Re: Confusion in TLA+ model for access control

[Leslie Lamport <tlapl...@xxxxxxxxx>]

The specification you have written seems to be assuming that UserId is
a set of strings, apparently containing the elements "u1" and "u2" and
perhaps other elements.  My guess is that you are telling TLC to set
UserId to a set whose elements are not strings.  Since you don't
report an error message, I presume that set is a set of model values.

It is helpful to readers of a spec to say what the "types" of the
spec's constants are.  The best way to do that is with an assumption
such as

 

   ASSUME UserId \subseteq STRING

 

TLC checks that assumptions are satisfied by a model.  If you had

done that, I expect that TLC would have reported an error
that would have told you exactly what your problem was.

 

Leslie Lamport

 

On Saturday, January 11, 2014 1:23:17 PM UTC-8, Reena Singh wrote:

Hi,

I am writing a model to check access of users on documents. If the user satisfies certain conditions document should be accessible. For example, say we have users with UserId u1, u2 and documents with DocId d1, d2. I initialize them with default values (in Init). Then I call a function, say Assign with UserId which assigns different values for the different fields depending on the value of UserId i.e. u1 or u2. Similarly, we assign values to Document d1, d2. Then we will specify other actions where states of u1, u2, d1, d2 will be changed.

Here is what I have written.

---------------MODULE acm0 ------------------
EXTENDS Naturals, TLC
CONSTANTS UserId, DocId
VARIABLES user, doc
-------------------------------------------------
User == [st:{"idle", "requesting", "accessing", "ended"}, role:{"na","pm", "operator"}, op: {"na","sp", "agg", "r", "w", "a"}]
Doc ==  [st:{"idle", "active", "ended"}, access: {"na","pm"}, op : {"na", "sp", "agg"}]

-----------------------------------------------------
TypeOK == /\ user \in [UserId -> User]
          /\ doc  \in [DocId -> Doc]
           
Init ==
      /\  user =  [u \in UserId |-> [st |-> "idle", role |-> "na", op |-> "na"]]
      /\ doc = [D \in DocId |-> [st |-> "idle", access |-> "na", op |-> "na"]]
       
 Assign(uid)  ==
  /\ PrintT(uid)
  /\ IF (uid = "u1")
    THEN ( PrintT(uid) \/ user' = [uid |-> [st |-> "idle", role |-> "pm", op |-> "sp"]])
    ELSE IF (uid = "u2")
     THEN (PrintT(uid) /\ user' = [uid |-> [st |-> "idle", role |-> "pm", op |-> "agg"]] )
    ELSE (PrintT("Nothing")/\ UNCHANGED <<user>>)
 /\ PrintT(user')

## Comment-- The comparison in the If condition in above function fails always as I am comparing value to string.
 
 AssignD(oid) ==
 IF (oid = "D1")
 THEN doc = [oid |-> [st |-> "idle", access |-> "pm", op |-> "sp"]]
 ELSE IF (oid = "D2")
 THEN doc = [oid |->  [st |-> "idle", access |-> "pm", op |-> "agg"]]
 ELSE UNCHANGED <<doc>>
 
 
---------------------------------------------------------
Tryaccess(uid, oid) ==
  IF (user[uid].st = "idle" /\ doc[oid].st = "idle")
    THEN   (user' = [user EXCEPT ![uid].st = "requesting"]
             /\ doc' = [doc EXCEPT ![oid].st = "active"])
             
     ELSE UNCHANGED <<user, doc>>
     

Allowaccess(uid, oid) ==
 IF (user[uid].st = "requesting" /\ doc[oid].st = "active" /\ user[uid].role = doc[oid].access /\ user[uid].op = doc[oid].op)  
   THEN (/\ user' = [user EXCEPT ![uid].st = "accessing"]
        /\ doc' = [doc EXCEPT ![oid].st = "accessing"])
       
    ELSE UNCHANGED <<user, doc>>

Next ==
   \E uid \in UserId, oid \in DocId :
   /\ Assign(uid)
   /\ AssignD(oid)
   
   /\ \/ Tryaccess(uid, oid)
     
      \/ Allowaccess(uid,oid)

--------------------------------------------------------------------------
Spec == Init /\ [][Next]_<<user,doc>>

THEOREM Spec => []TypeOK        
========================================================================        
Only Init action happens. In Assign(), the If condition always evaluates to false. What is the alternative way to do this?

Thank you so much in advance