MACHINE

    e_purse_policy  /* UAC policy for e-purse_func.mch */

SETS

    SUBJECT={pda, terminalBancaire, terminalAdministratif} ;
    OBJECT={beginSession, endSession, setBpc, setHpc, authBank, checkPin, getBalance, debit, credit} ;
    MODE={PERSO, INVALID, USE}
    
CONCRETE_CONSTANTS

    mode, isBankAuth, isHoldAuth, permission

PROPERTIES

    mode : MODE & 
    isBankAuth : BOOL & 
    isHoldAuth : BOOL & 
    permission : SUBJECT <-> OBJECT & 
    (terminalAdministratif |-> beginSession) : permission & 
    (
        mode = PERSO
         => 
        (terminalAdministratif |-> setBpc) : permission
    ) & 
    
    (    mode = PERSO 
         => 
        (terminalAdministratif |-> setHpc) : permission 
   
     ) &

    (terminalAdministratif |-> endSession) : permission & 

    (terminalBancaire |-> beginSession) : permission & 

    (
        (
            mode = INVALID
        )
         => 
        (terminalBancaire |-> authBank) : permission
    ) & 

    (
        (mode = USE)
         => 
        (terminalBancaire |-> checkPin) : permission
      ) & 

    (terminalBancaire |-> endSession) : permission & 

    (
        (
            mode = INVALID & 
            isBankAuth = TRUE
        )
         => 
        (terminalBancaire |-> setHpc) : permission
    ) & 
        
        
        (
            mode = USE & 
            isHoldAuth = TRUE
        )
         => 
        (terminalBancaire |-> credit) : permission
    ) & 
    (
        (
            mode = USE & 
	    isHoldHAuth = TRUE
        )
         => 
        (terminalBancaire |-> getBalance) : permission
    ) & 
    (
        
            mode = USE 
        
         => 
          (terminalBancaire |-> debit) : permission
                  
    ) & 

    (pda |-> beginSession) : permission & 
    (pda |-> endSession) : permission & 
    (
        (
            mode = USE
        )
         => 
        (pda |-> getBalance) : permission
    ) &
    (
        
            mode = USE 
        
         => 
        (pda |-> debit) : permission
    )

END