byte sessionID_LINUX,username_LINUX,signature_LINUX,privatekey_LINUX;
bit result_LINUX;

#define Error               0
#define Success		    1

#define InvalidPWErr	    0
#define NoUserErr	    0
#define SameUserErr	    0
#define TooManySessionErr   0

#define InvalidPrivateKey   0
#define InvalidSignature    0
#define InvalidSession	    0
#define InvalidUserID	    0
#define InvalidPasswordHash 0

#define HashFunctionErr	    0
#define ReadPrivateKeyErr   0
#define ReadSigantureErr    0
#define AppendSignatureErr  0

#define MAX_num_of_users    2 /* = MAX_username-MIN_username+1 */

#define MIN_username	    1
#define MAX_username	    2

#define MIN_Good_Password   1
#define MAX_Good_Password   2
#define MIN_Bad_Password    3 /* = MAX_Good_Password+1 */
#define MAX_Bad_Password    3

#define MAX_num_of_sessions 2 /* = MAX_Good_SessionID-MIN_Good_SessionID+1 */

#define MIN_Good_SessionID  1
#define MAX_Good_SessionID  2
#define MIN_Bad_SessionID   3 /* = MAX_Good_SessionID+1 */
#define MAX_Bad_SessionID   3

#define MIN_Message_Hash    0
#define MAX_Message_Hash    1
#define MIN_Message	    0
#define MAX_Message	    1

mtype = { Logout, AuthUser, GenSig, CheckReadKey, CheckReadSigRec, CheckAppendSigRec};

#define Hash(x)			(x)   /* dummy hash function */
#define Sign(mes, key, sig)     (key) /* dummy sign function */

typedef ACL_entry {
    byte UserID;
    byte Username;
    byte Hpassword
}

typedef Session_entry {
    bool Flag;
    byte SessionID;
    byte UserID;
    bool PriKeyReadAccess;
    bool SigLogWriteAccess
}

typedef PrivateKeyList_entry {
    byte UserID;
    byte PrivateKey
}

typedef SignatureLog_entry {
    byte UserID;
    byte SignatureLog
}
/* NOTE: In this code, Signature Log has only the latest signature record for each user. */

/* dummy Init function for ACL */
#define Init_ACL(ent,i,j,k)    ent.UserID=i;ent.Username=j;ent.Hpassword=k

/* dummy Init function for PrivateKeyList */
#define Init_PrivateKeyList(ent,i,j) ent.UserID=i;ent.PrivateKey=j

/* dummy Init function for SignatureLog */
#define Init_SignatureLog(ent,i,j) ent.UserID=i;ent.SignatureLog=j

#define TRUE  1
#define FALSE 0

/* channel between Windows side module and Darma */

chan wd = [0] of { mtype, byte, byte }; /* funcID, arg1, arg2 */
chan dw  = [0] of { mtype, byte }; /* funcID, result */

/* channel between Darma and Linux side module */

chan dl_auth = [0] of { byte, byte };	/* username, password */
chan ld_auth  = [0] of { byte };	/* sessionID */
chan dl_gensig = [0] of { byte, bit }; /* sessionID, message_hash */
chan ld_gensig  = [0] of { byte };	/* signature */
chan dl_logout = [0] of { byte };	/* sessionID */
chan ld_logout  = [0] of { bit };	/* result (1:success) */

/* channel between Linux side module and Access Contoroller */
chan la_auth = [0] of { byte, byte };	/* username, password_hash */
chan al_auth  = [0] of { byte };	/* sessionID */
chan la_readkey = [0] of { byte };	/* sessionID */
chan al_readkey  = [0] of { byte };	/* private-key */
chan la_readsig = [0] of { byte };	/* sessionID */
chan al_readsig  = [0] of { byte };	/* lateset_signature_rec */
chan la_appendsig = [0] of { byte, byte }; /* sessionID, signature */
chan al_appendsig  = [0] of { bit };	/* result (1:success) */
chan la_logout = [0] of { byte };	/* sessionID */
chan al_logout  = [0] of { bit };	/* result (1:success) */

/* channel between Access Controller and Session Manager */

chan as_regist = [0] of { byte, bool, bool };
     /* userID, AccessRight of PrivateKey, Access Right of Signature log */
chan sa_regist  = [0] of { byte };	/* sessionID */
chan as_check = [0] of { byte, mtype }; /* sessionID, funcID(AccessType)  */
chan sa_check  = [0] of { mtype, byte };/* funcID(AccessType), userID */
chan as_free = [0] of { byte };		/* sessionID */
chan sa_free  = [0] of { bit };		/* result (1:success) */

/* Random Number Generator (we do not use the proccess for RNG any more.) */

#define setrandom(var, lower, upper) 	atomic{ \
	  var = (lower);			\
	  do					\
	  :: break				\
	  :: (var <  (upper)) -> var = var + 1	\
	  :: (var == (upper)) -> break		\
	  od;					\
	  skip;					\
	}

/*******/

proctype WindowsSideModule_Attacker()
{
  byte username, password, sessionID, signature, dummy, result;
  bit message_hash;

  /* 
  [Attacker Model]  
  1. Attacker can call AuthenticateUserW, GenerateSignatureW, and LogoutW 
     in any order.
  2. Attacker is also a legitimate user with a user name and a password.
  3. Attacker knows the names of all users, and can guess messages and 
     message hashs.
  4. Attacker can only give his (good) password or a bad guessed password.
  5. Attacker cannot guess a good sessionID.
  6. Generated sessionIDs are always good.
  */

  atomic{  
  setrandom(username, MIN_username, MAX_username);
  setrandom(password, MAX_Good_Password, MAX_Bad_Password);
  setrandom(sessionID, MIN_Bad_SessionID, MAX_Bad_SessionID);
  setrandom(message_hash, MIN_Message_Hash, MAX_Message_Hash);
  };

  do
  /* Attacker calls these three functions in any order */
  :: wd!AuthUser,username,password
     -> dw?AuthUser,sessionID  /* sessionID (0:failed) */

  :: wd!GenSig,sessionID,message_hash
     -> dw?GenSig,signature  /* signature (0:failed) */

  :: wd!Logout,sessionID,dummy
     -> dw?Logout,result  /* result: Seccess or Error */

  /* Or, Attacker guesses following values */
  :: setrandom(username, MIN_username, MAX_username)
  :: setrandom(password, MAX_Good_Password, MAX_Bad_Password)
  :: setrandom(sessionID, MIN_Bad_SessionID, MAX_Bad_SessionID)
  :: setrandom(message_hash, MIN_Message_Hash, MAX_Message_Hash)
  od
}


proctype WindowsSideModule_Normal()
{
  byte username;
  byte password;
  byte sessionID;
  bit  message;
  bit  message_hash;
  byte signature;
  byte result;

  atomic{
  username = 1; /* legitimate username */
  password = 1;	/* good password for above user */
  }

  do
  :: wd!AuthUser,username,password;
     dw?AuthUser,sessionID;

     atomic{
     setrandom(message, MIN_Message, MAX_Message);
     message_hash = Hash(message);
     };

     wd!GenSig,sessionID,message_hash;
     dw?GenSig,signature;

     wd!Logout,sessionID,0; /* second argument '0' is dummy */
     dw?Logout,result

  od
}


proctype Darma()
{
  byte username, password, sessionID, signature, dummy;
  bit result, message_hash;
	
  do
    :: wd?AuthUser,username,password
       -> 
	  dl_auth!username,password;
	  ld_auth?sessionID;
	  dw!AuthUser,sessionID

    :: wd?GenSig,sessionID,message_hash
       -> 
	  dl_gensig!sessionID,message_hash;
	  ld_gensig?signature;
	  dw!GenSig,signature

    :: wd?Logout,sessionID,dummy
       -> 
	  dl_logout!sessionID;
	  ld_logout?result;
	  dw!Logout,result
  od
}

proctype LinuxSideModule()
{

  byte password,password_hash,sigrec;
  bit message_hash;

  do

  /* AuthenticateUserL */
  :: dl_auth?username_LINUX,password
     -> 

	/* (1) caluculate hash value of password */	
	password_hash = Hash(password);
	if
	:: (password_hash <= 0) -> sessionID_LINUX = HashFunctionErr;
				   goto DONE_AuthL
	:: else
	fi;

	/* (2) authenticate user by the function AuthenticateUser
	       of AccessContoroller */
	la_auth!username_LINUX,password_hash;
	al_auth?sessionID_LINUX;

	/* (3) Output SessionID */

      DONE_AuthL:
	ld_auth!sessionID_LINUX

  /* GenerateSignatureL */
  :: dl_gensig?sessionID_LINUX,message_hash
     -> 
	

	/* (1) read private-key by the ReadPrivateKey
	       of AccessContoroller */

	la_readkey!sessionID_LINUX;
	al_readkey?privatekey_LINUX;
	if
	:: (privatekey_LINUX <= 0) -> signature_LINUX = ReadPrivateKeyErr;
				goto DONE_GensigL
	:: else
	fi;

	/* (2) read the latest signature record by ReadSignatureRecord
	       of AccessContoroller */

	la_readsig!sessionID_LINUX;
	al_readsig?sigrec;
	if
	:: (sigrec <= 0) -> signature_LINUX = ReadSigantureErr;
			    goto DONE_GensigL
	:: else
	fi;

	/* (3) generate signature from message hash, private-key, 
	       and the latest signature record */

        signature_LINUX = Sign(message_hash, privatekey_LINUX, sigrec);
	if
	:: (signature_LINUX <= 0) -> signature_LINUX = InvalidSignature;
			       goto DONE_GensigL
	:: else
	fi;

	/* (4) Append signature to signature log by AppendSignatureRecord
	       of AccessContoroller */

	la_appendsig!sessionID_LINUX,signature_LINUX;
	al_appendsig?result_LINUX;
	if
	:: (result_LINUX <= 0) -> signature_LINUX = AppendSignatureErr;
			    goto DONE_GensigL
	:: else
	fi;

	/* (5) Output the signature */
   DONE_GensigL:
        ld_gensig!signature_LINUX

  /* LogoutL */
  :: dl_logout?sessionID_LINUX
     -> 
	
	/* (1) Free session by Logout of AccessContoroller */
	la_logout!sessionID_LINUX;
	al_logout?result_LINUX;
	/* (2) Output result_LINUX */
    DONE_LogoutL:    /* Added for fixed property spec */
	ld_logout!result_LINUX

	/* NOTE: According to the specification document, 
		 result_LINUX=0 means Success, 
		 but in this promela code, result_LINUX=0 means Error */

  od

}

proctype AccessController()
{
  byte userID,hpassword;
  byte privatekey, signature, latest_signature, sessionID;
  byte username, password_hash;
  byte counter;
  bit result;

  ACL_entry ACL[MAX_num_of_users]; /* username, userID, password_hash */
  PrivateKeyList_entry PrivateKeyList[MAX_num_of_users]; /* userID, priv_key */
  SignatureLog_entry SignatureLog[MAX_num_of_users]; /* userID, sig_log */

  d_step{
  Init_ACL(ACL[0],1,1,1); /* for Username (= UserID) = 1 */
  Init_ACL(ACL[1],2,2,2); /* for Username (= UserID) = 2 */

  Init_PrivateKeyList(PrivateKeyList[0],1,1); /* for UserID = 1 */
  Init_PrivateKeyList(PrivateKeyList[1],2,2); /* for UserID = 2 */

  Init_SignatureLog(SignatureLog[0],1,1); /* for UserID = 1 */
  Init_SignatureLog(SignatureLog[1],2,2); /* for UserID = 2 */
  }
  
  do

  /* AuthenticateUser */
  :: la_auth?username,password_hash
     -> 

	/* (1) search username from access control list */
	/* (2) Get UserID and Hpassword for username */
	atomic{
	counter = 0;
	do
	:: (  (counter < MAX_num_of_users) 
	    &&(ACL[counter].Username == username))
	   -> userID = ACL[counter].UserID;
	      hpassword = ACL[counter].Hpassword;
	      break
	:: (  (counter < MAX_num_of_users) 
	    &&(ACL[counter].Username != username))
	   -> counter = counter + 1
	:: (counter >= MAX_num_of_users)
	   -> userID = InvalidUserID;
	      hpassword = InvalidPasswordHash;
	      sessionID = NoUserErr;
	      goto DONE_Auth
	od;
	};

	/* (3) Check hpassword == password_hash ? */
	atomic{
	if
	:: (hpassword != password_hash) -> sessionID = InvalidPWErr;
					   goto DONE_Auth
	:: else
	fi;
	};

	/* (4) Set PriKeyReadAccess = TRUE, SigLogWriteAccess = TRUE */
	/* (5) Call RegistSessionInformation of SessionManager */
	as_regist!userID,TRUE,TRUE;
	sa_regist?sessionID;

      DONE_Auth:
        al_auth!sessionID
	
  /* ReadPrivateKey */
  :: la_readkey?sessionID
     -> 

	/* (1) Call CheckValidofSession an AccessType=READ_PRIKEY */
	as_check!sessionID,CheckReadKey;
	sa_check?CheckReadKey,userID;
	
	atomic{
	if
	::(userID <= 0) -> privatekey = InvalidPrivateKey;
			   goto DONE_ReadPrivateKey
	:: else
	fi;
	};

	/* (2) Read private-key corresponding to userID */
	d_step{
	counter = 0;
	do
	:: (  (counter < MAX_num_of_users)
	    &&(PrivateKeyList[counter].UserID==userID))
	   -> privatekey = PrivateKeyList[counter].PrivateKey;
	      break
	:: (  (counter < MAX_num_of_users)
	    &&(PrivateKeyList[counter].UserID!=userID))
	   -> counter = counter + 1
	:: (counter >= MAX_num_of_users)
	   -> privatekey = InvalidPrivateKey;
	      break
	od;
	skip;
	};

	/* (3) Output private-key */

      DONE_ReadPrivateKey:
	al_readkey!privatekey

  /* ReadSignatureRecord */
  :: la_readsig?sessionID
     -> 
	
	/* (1) Call CheckValidofSession an AccessType=READ_SIGLOG */
	as_check!sessionID,CheckReadSigRec;
	sa_check?CheckReadSigRec,userID;

	atomic{
	if
	::(userID <= 0) -> latest_signature = ReadSigantureErr;
			   goto DONE_ReadSignatureRecord
	:: else
	fi;
	};

	/* (2) Read the latest signature corresponding to userID */
	d_step{
	counter = 0;
	do
	:: (  (counter < MAX_num_of_users)
	    &&(SignatureLog[counter].UserID==userID))
	   -> latest_signature = SignatureLog[counter].SignatureLog;
	      break
	:: (  (counter < MAX_num_of_users)
	    &&(SignatureLog[counter].UserID!=userID))
	   -> counter = counter + 1
	:: (counter >= MAX_num_of_users)
	   -> latest_signature = InvalidSignature;
	   break
	od;
	skip;
	};

	/* (3) Output the latest signature */

      DONE_ReadSignatureRecord:
	al_readsig!latest_signature

  /* AppendSignatureRecord */
  :: la_appendsig?sessionID,signature
     -> 

	/* (1) Call CheckValidofSession an AccessType=WRITE_SIGLOG */
	as_check!sessionID,CheckAppendSigRec;
	sa_check?CheckAppendSigRec,userID;

	atomic{
	if
	::(userID <= 0) -> result = Error; goto DONE_AppendSignatureRecord
	::(userID >  0) -> result = Success
	fi;
	};

	/* (2) Append the latest signature corresponding to userID */
	d_step{
	counter = 0;
	do
	:: (  (counter < MAX_num_of_users) 
	    &&(SignatureLog[counter].UserID==userID))
	   -> SignatureLog[counter].SignatureLog = signature;
	      break
	:: (  (counter < MAX_num_of_users) 
	    &&(SignatureLog[counter].UserID!=userID))
	   -> counter = counter + 1
	:: (counter >= MAX_num_of_users)
	   -> result = Error;
	      break
	od;
	skip;
	};

	/* (3) Output the latest signature */

      DONE_AppendSignatureRecord:
	al_appendsig!result

	/* NOTE: According to the specification document, 
		 result=0 means Sucssess, 
		 but in this promela code, result=0 means Error */

  /* Logout */
  :: la_logout?sessionID
     -> 

	/* (1) Call FreeSessionInformation of SessionManager */
	as_free!sessionID;
	sa_free?result;
	/* (2) Output result */
	al_logout!result

  od

}

/* NOTE: I modeled SessionManager based on the document "darma-hs.pdf". */

proctype SessionManager()
{
  bit result;
  byte userID,sessionID;
  bool priKeyReadAccess,sigLogWriteAccess;
  byte counter;
  Session_entry session_entry;

  /* Session table (NOTE: This table is initilized as all values = 0) */
  Session_entry Session[MAX_num_of_sessions];

  do

  /* RegistSessionInformation */
  :: as_regist?userID,priKeyReadAccess,sigLogWriteAccess
     -> 

	/* (1) Check whether the same UserID does not exist on the table */
	atomic{
	counter = 0;
	do
	:: (  (counter < MAX_num_of_sessions)
	    &&(  (Session[counter].UserID == userID) 
	       &&(Session[counter].Flag == TRUE)))
	   -> sessionID = SameUserErr;
	      goto DONE_RegistSession
	:: (  (counter < MAX_num_of_sessions)
	    &&(  (Session[counter].UserID != userID)
	       ||(Session[counter].Flag == FALSE)))
	   -> counter = counter + 1
	:: (counter >= MAX_num_of_sessions)
	   -> break
	od;
	};

	/* (2) Generate SessionID */

      GENERATE_SESSION_ID:
	atomic{
	setrandom(sessionID,MIN_Good_SessionID,MAX_Good_SessionID); 
	/* choose a random number between MIN_Good_SessionID 
	   and MAX_Good_SessionID */
	counter = 0;
	do
	:: (counter < MAX_num_of_sessions)
	   -> if    /* Check the sessionID is fresh or not */
	      :: ((Session[counter].SessionID == sessionID)
		 && (Session[counter].Flag == TRUE))
		 -> goto GENERATE_SESSION_ID
	      :: ((Session[counter].SessionID != sessionID)
		 || (Session[counter].Flag == FALSE))
		 -> counter = counter + 1
              fi
	:: (counter >= MAX_num_of_sessions)
	   -> break
	od;
	};

	/* (3) Register session information */

	d_step{
	counter = 0;
	do
	:: (  (counter < MAX_num_of_sessions)
	    &&(Session[counter].Flag == FALSE))
	   -> Session[counter].UserID = userID;
	      Session[counter].SessionID = sessionID;
	      Session[counter].PriKeyReadAccess = priKeyReadAccess;
	      Session[counter].SigLogWriteAccess = sigLogWriteAccess;
	      Session[counter].Flag = TRUE;
	      break
	:: (  (counter < MAX_num_of_sessions)
	    &&(Session[counter].Flag != FALSE))
	   -> counter = counter + 1
	:: (counter >= MAX_num_of_sessions)
	   -> sessionID = TooManySessionErr;
	      break
	od;
	skip;
	};

	/* (4) Output sessionID */
      DONE_RegistSession:
	sa_regist!sessionID
  
  /* CheakValidOfSession (READ_PRIKEY) */
  :: as_check?sessionID,CheckReadKey
     -> 

	/* (1) Search the pointer to SessionID in the session table */
	atomic{
	counter = 0;
	do
	:: (  (counter < MAX_num_of_sessions) 
	    &&(Session[counter].SessionID == sessionID))
	   -> break
	:: (  (counter < MAX_num_of_sessions) 
	    &&(Session[counter].SessionID != sessionID))
	   -> counter = counter + 1
	:: (counter >= MAX_num_of_sessions)
	   -> userID = Error;
	      goto DONE_CHECK_READ_KEY
	od;
	};

	/* (2-1) Check PriKeyReadAccess == TRUE && Flag == TRUE */
	   
	d_step{
	if
	:: ((Session[counter].PriKeyReadAccess == TRUE) &&
	    (Session[counter].Flag == TRUE))
	   -> Session[counter].PriKeyReadAccess = FALSE; 
			/* (2-2) set PriKeyReadAccess = FALSE */
	      userID = Session[counter].UserID
	:: ((Session[counter].PriKeyReadAccess == FALSE) ||
	    (Session[counter].Flag == FALSE )) 	   
	   -> userID = Error
	fi;
	};
	
      DONE_CHECK_READ_KEY:
	sa_check!CheckReadKey,userID

  /* CheakValidOfSession (READ_SIGLOG) */
  :: as_check?sessionID,CheckReadSigRec
     -> 

	/* (1) Search the pointer to SessionID in the session table */

	atomic{
	counter = 0;
	do
	:: (  (counter < MAX_num_of_sessions) 
	    &&(Session[counter].SessionID == sessionID))
	    -> break
	:: (  (counter < MAX_num_of_sessions) 
	    &&(Session[counter].SessionID != sessionID))
	    -> counter = counter + 1
	:: (counter >= MAX_num_of_sessions)
	   -> userID = Error;
	      goto DONE_CHECK_READ_SIG_REC
	od;
	};

	/* (2-1) Check Flag == TRUE */

	d_step{
	if
	:: (Session[counter].Flag == TRUE )
	   -> userID = Session[counter].UserID
	:: (Session[counter].Flag == FALSE )
	   -> userID = Error
	fi;
	};

      DONE_CHECK_READ_SIG_REC:
	sa_check!CheckReadSigRec,userID

  /* CheakValidOfSession (WRITE_SIGLOG) */
  :: as_check?sessionID,CheckAppendSigRec
     -> 

	/* (1) Search the pointer to SessionID in the session table */
	atomic{
	counter = 0;
	do
	:: (  (counter < MAX_num_of_sessions) 
	    &&(Session[counter].SessionID == sessionID))
	   -> break
	:: (  (counter < MAX_num_of_sessions) 
	    &&(Session[counter].SessionID != sessionID))
	   -> counter = counter + 1
	:: (counter >= MAX_num_of_sessions)
	   -> userID = Error;
	      goto DONE_CHECK_APPEND_SIG_REC
	od;
	};

	/* (2-1) Check SigLogWriteAccess == TRUE && Flag == TRUE */

	d_step{
	if
	:: ((Session[counter].SigLogWriteAccess == TRUE) &&
	    (Session[counter].Flag == TRUE ))
	   -> Session[counter].SigLogWriteAccess = FALSE;
			/* (2-2) set SigLogWriteAccess = FALSE */
	      userID = Session[counter].UserID
	:: ((Session[counter].SigLogWriteAccess == FALSE) ||
	    (Session[counter].Flag == FALSE )) 	   
	   -> userID = Error
	fi;
	};
	
       DONE_CHECK_APPEND_SIG_REC:
	sa_check!CheckAppendSigRec,userID

  /* FreeSessionInformation */
  :: as_free?sessionID
     -> 

	/* Free session */

	/* (1) Search the pointer to SessionID in the session table */
	atomic{
	counter = 0;
	do
	:: (  (counter < MAX_num_of_sessions) 
	    &&(Session[counter].SessionID == sessionID))
	   -> break
	:: (  (counter < MAX_num_of_sessions) 
	    &&(Session[counter].SessionID != sessionID))
	   -> counter = counter + 1
	:: (counter >= MAX_num_of_sessions)
	   -> result = Error;
	      goto DONE_FREE_SESSION
	od;
	};

	d_step{
	if
	:: (Session[counter].Flag == TRUE)
	   -> Session[counter].Flag = FALSE;
	      Session[counter].SigLogWriteAccess = FALSE;
	      Session[counter].PriKeyReadAccess = FALSE;
	      Session[counter].UserID = 0;
	      Session[counter].SessionID = 0;
	      result = Success
	:: (Session[counter].Flag == FALSE)
	   -> result = Error
	fi;  
	};

      DONE_FREE_SESSION:
	sa_free!result

	/* NOTE: According to the specification document, 
		 result=0 means Sucssess, 
		 but in this promela code, result=0 means Error */

  od
}

byte lsm;

init {

     atomic{
     run WindowsSideModule_Normal();
     run WindowsSideModule_Attacker();
     run Darma();
     lsm = run LinuxSideModule();
     run AccessController();
     run SessionManager()
     }
}


/* UAS stands for "User Authenticate with Session" 
   uname:username, sID:sessioID */

#define UAS(uname,sID)    ((LinuxSideModule[lsm]@DONE_AuthL)  \
			&& (username_LINUX == (uname))	    \
			&& (sessionID_LINUX == (sID)))

/* GHSS stands for "Generate Hysteresis Signature with Session"
   sID: sessionID		*/

#define GHSS(sID)     ((LinuxSideModule[lsm]@DONE_GensigL)    \
		    && (signature_LINUX > 0)		    \
		    && (sessionID_LINUX == (sID)))

/* added for modeling logout */
#define OUT(sID)    ((LinuxSideModule[lsm]@DONE_LogoutL)    \
		    && (result_LINUX > 0)		    \
		    && (sessionID_LINUX == (sID)))


/* GHSSP stands for "Generate Hysteresis Signature with Session(sID)
   by using the Privatekey(privkey)"
   sID: sessionID  privkey: private-key */

#define GHSSP(privkey,sID)   ((LinuxSideModule[lsm]@DONE_GensigL)    \
			    && (signature_LINUX > 0)		   \
			    && (sessionID_LINUX == (sID))	   \
			    && (privatekey_LINUX == (privkey)))

/*********** Requrement 1 ************/

/*
    Requirement (1)

GOOD1:   HSD shall authenticate a user before the user generates 
    a hysteresis siganture.

BAD1: The signature architecture generates a signature
             for an unauthenticated user
 
    \exist s:session (GHSS(s) without (\exist u:user UAS(u,s)))
 => \exist s:session ( !(\exist u:user UAS(u,s)) U GHSS(s) )
 =>    ( !(UAS(1,1)||UAS(2,1)) U GHSS(1) ) 
    || ( !(UAS(1,2)||UAS(2,2)) U GHSS(2) )   
    || ( !(UAS(1,3)||UAS(2,3)) U GHSS(3) )   


For following formalizations we use weak until.  (use BASH)
   p W q = ([]p) \/ (p U q)
         = <>(!p) -> (p U q)
         = p U (q \/ []p)


Good2:  For each signature generation, the user is authenticated
and has not logged out.
   ((~s) W i) & G( o -> ((~s) W i) )
 The 1st conjunct says 
   "there is no $s$ (weak) until there is an $i$."
or  i proceeds s
 
 The 2nd conjunts says 
   "everytime there is an $o$, there is no $s$ (weak) until there is an $i$."
or after each o, i proceeds s

TRANSLATION IN SPIN:
   ((~s) W i) & G( o -> ((~s) W i) )
or !(((!s) U (i || []!s)) && []( o -> ((!s) U (i || []!s))))

GENERALIZE for 2 users, 3 session ids
Here replace s with gi, i with ui, and o with oi
  (((!gi) U (ui || []!gi)) && []( oi -> ((!gi) U (ui || []!gi))))

Now conjoin (good thing) 3 copies appropriately indexed and negate
  !( (((!g1) U (u1 || []!g1)) && []( o1 -> ((!g1) U (u1 || []!g1)))) && 
     (((!g2) U (u2 || []!g2)) && []( o2 -> ((!g2) U (u2 || []!g2)))) && 
     (((!g3) U (u3 || []!g3)) && []( o3 -> ((!g3) U (u3 || []!g3))))  )  */

#define u1	(UAS(1,1) || UAS(2,1))
#define u2	(UAS(1,2) || UAS(2,2))
#define u3	(UAS(1,3) || UAS(2,3))
#define g1	GHSS(1)
#define g2	GHSS(2)
#define g3	GHSS(3)
#define o1      OUT(1)
#define o2      OUT(2)
#define o3      OUT(3)

/* compile options: gcc -O3 -DCOLLAPSE -o pan pan.c
   pan options: pan -m1400000 -w24 -a -n -c1 */