---------------------------MODULE Authorization_PKMv35------------------------
(* The TLA+ specification of the Authorization process in IEEE 802.16 *)
(* EECS, Northwestern University *)

EXTENDS Integers, Sequences, Naturals, TLC, FiniteSets

CONSTANTS MScertificate, BScertificate, TEKkey, AuthKeySeq, MaxReal, NUM, CNTN

Real == 0 .. MaxReal

(* Certificate is used to prove the identity of the SS. It is used as an ID *)


(* Side = 1 for SSAuth, 2 for SATek, 3 for SSTek and 4 for BS *)

VARIABLES SS_state, SS_AuthPkmid, SS_AuthPend, SS_AuthGraceTimer, SS_cnt, SS_AuthWaitTimer, SS_retry

VARIABLES Tek_state, Tek_TekKeyTimeout, Tek_nonce

VARIABLES BS_state, BS_pkmid, BS_reqTimer

VARIABLES SA_state, SA_SATekPkmID, SA_challengeTimer, SA_responseTimer

VARIABLES AuthToTekmsg, AuthToSATekmsg, SSToBSmsg, SATekToAuthmsg, BStoSSmsg, Side, TekPkmid
          
VARIABLES AT_state, AT_knowledge, AT_MSGset, AT_cnt

varsSSAuth == <<SS_state, SS_AuthPkmid, SS_AuthPend, SS_AuthGraceTimer, SS_cnt, SS_AuthWaitTimer, SS_retry>>

varsSATek == <<SA_state, SA_SATekPkmID, SA_challengeTimer, SA_responseTimer>>

varsSSTek == <<Tek_state, Tek_TekKeyTimeout, Tek_nonce>>

varsBS == <<BS_state, BS_pkmid, BS_reqTimer>>

varsAT == <<AT_state, AT_knowledge, AT_MSGset, AT_cnt>>

gvars == <<SS_state, SS_AuthPkmid, SS_AuthPend, SS_AuthGraceTimer, SS_AuthWaitTimer, SS_retry,
         Tek_state, Tek_TekKeyTimeout, Tek_nonce,
         BS_state, BS_pkmid, BS_reqTimer,
         SA_state, SA_SATekPkmID, SA_challengeTimer, SA_responseTimer,
         AuthToTekmsg, AuthToSATekmsg, SSToBSmsg, SATekToAuthmsg, BStoSSmsg,
         Side, TekPkmid, SS_cnt, AT_state, AT_knowledge, AT_MSGset, AT_cnt>>
         

(* Messages: "PKM_REQ", "PKM_RSP" with different types *)

Message ==     [type:{" SA_ADD "}, pkmID: Real, HMAC: Real]

          \cup [type:{" RSA_REQ"}, pkmID: Real, MSrand: Real, MScert: MScertificate, SigSS: Real]

          \cup [type:{" RSA_REP"}, pkmID: Real, MSrand: Real, BSrand: Real, BScert: BScertificate,
                                   SigBS: Real]
          
          \cup [type:{" RSA_REJ"}, pkmID: Real, MSrand: Real, BSrand: Real, subtype:{"PERM", "NPERM"}, BScert: BScertificate,
                                   SigBS: Real]

          \cup [type:{" RSA_ACK"}, pkmID: Real, BSrand: Real, subtype:{"SUCCESS", "FAILURE"}, SigSS: Real]

          \cup [type:{"SATEK_CH"}, pkmID: Real, BSrand: Real, HMAC: Real]
          
          \cup [type:{"SATEK_RQ"}, pkmID: Real, MSrand: Real, BSrand: Real, HMAC: Real]
          
          \cup [type:{"SATEK_RP"}, pkmID: Real, MSrand: Real, BSrand: Real, SAdesc: Real, HMAC: Real]

          \cup [type:{" KEY_REQ"}, pkmID: Real, Nonce: Real, HMAC: Real]

          \cup [type:{" KEY_REP"}, pkmID: Real, TEKold: TEKkey, TEKnew: TEKkey, Nonce: Real, HMAC: Real]

          \cup [type:{" KEY_REJ"}, pkmID: Real, Nonce: Real, HMAC: Real]

          \cup [type:{"AUTH_INV"}, pkmID: Real]
          
          \cup [type:{" TEK_INV"}, pkmID: Real, HMAC: Real]
          
          \cup [type:{"AUTH_INF"}, pkmID: Real]

          \cup [type:{"SATEK_START"}]
          
          \cup [type:{"AUTHORIZED"}]

          \cup [type:{"ERROR"}]

          \cup [type:{"DONE"}]
          
          \cup [type:{"AUTH_COMP"}]

          \cup [type:{"AUTH_PEND"}]

          \cup [type:{"STOP"}]

          
---------------------------MODULE SSAuth-------------------------------

VARIABLES state, cnt2, AuthPkmid, AuthPend, AuthGraceTimer, AuthWaitTimer, retry
    
Init == /\ state = "SS_Start"        
        /\ AuthPend = 0
        /\ AuthPkmid = 1        
        /\ cnt2 = 1        
        /\ AuthGraceTimer = 0
        /\ AuthWaitTimer = 0
        /\ retry = 0
        
Trans0 == /\ state = "SS_Start"
          /\ Side = 1    
          /\ cnt2<=NUM               
          /\ retry<NUM*3
          /\ SSToBSmsg'= [type |-> " RSA_REQ", pkmID |-> AuthPkmid, MSrand |-> 1, 
                         MScert |-> MScertificate, SigSS |-> 1 ]
          /\ Side' = 2
          /\ state' = "SS_Auth_Wait"
          /\ UNCHANGED <<AuthToTekmsg, AuthToSATekmsg, SATekToAuthmsg, BStoSSmsg,
                         TekPkmid, AuthPkmid, AuthPend, AuthGraceTimer, cnt2, AuthWaitTimer, retry>>

Trans1 == /\ state = "SS_Auth_Wait"
          /\ Side = 1 
          /\ IF /\ BStoSSmsg # << >> 
                /\ BStoSSmsg.type = " RSA_REP" \/ BStoSSmsg.type = " RSA_REJ" 
                /\ BStoSSmsg.pkmID = AuthPkmid 
                /\ BStoSSmsg.MSrand = 1
                /\ BStoSSmsg.BScert = BScertificate
                /\ BStoSSmsg.SigBS = 2
             THEN
                /\ IF BStoSSmsg.type = " RSA_REP" THEN                      
                      /\ AuthToSATekmsg' = [type |-> "SATEK_START"]                      
                      /\ SSToBSmsg' = [type |-> " RSA_ACK", pkmID |-> BStoSSmsg.pkmID, BSrand |-> BStoSSmsg.BSrand, 
                                         subtype |-> "SUCCESS", SigSS |-> 1]
                      /\ state' = "SS_SATek_Wait"
                      /\ UNCHANGED <<AuthWaitTimer>>
                   ELSE IF BStoSSmsg.type = " RSA_REJ" THEN
                           /\ IF BStoSSmsg.subtype = "PERM" THEN
                                 /\ state' = "SS_Silent"
                                 /\ UNCHANGED <<AuthToSATekmsg, AuthWaitTimer>>
                              ELSE
                                 /\ state' = "SS_Auth_Reject_Wait"
                                 /\ UNCHANGED <<AuthToSATekmsg, AuthWaitTimer>>                           
                           /\ SSToBSmsg' = [type |-> " RSA_ACK", pkmID |-> BStoSSmsg.pkmID, BSrand |-> BStoSSmsg.BSrand, 
                                              subtype |-> "FAILURE", SigSS |-> 1]
                        ELSE                            
                           /\ UNCHANGED <<SSToBSmsg, state, AuthToSATekmsg, AuthWaitTimer>>
                /\ UNCHANGED AuthPkmid
                   (* IF AuthPkmid = MaxReal THEN
                       /\ AuthPkmid' = 1
                   ELSE 
                       /\ AuthPkmid' = AuthPkmid+1 *)
             ELSE
                IF AuthWaitTimer = 2 THEN                   
                   /\ SSToBSmsg'= [type |-> " RSA_REQ", pkmID |-> AuthPkmid, MSrand |-> 1, MScert |-> MScertificate, 
                                     SigSS |-> 1 ]
                   /\ AuthWaitTimer' = 0
                   /\ UNCHANGED <<AuthToSATekmsg, state, AuthPkmid>>
                ELSE
                   /\ AuthWaitTimer' = AuthWaitTimer + 1
                   /\ UNCHANGED <<AuthToSATekmsg,  state,  SSToBSmsg, AuthPkmid>>
          /\ Side' = 2    
          /\ BStoSSmsg' = << >>
          /\ UNCHANGED <<AuthToTekmsg, SATekToAuthmsg, TekPkmid,
                         AuthPend, AuthGraceTimer, cnt2, retry>>

Trans2 == /\ state = "SS_SATek_Wait"
          /\ Side = 1
          /\ IF SATekToAuthmsg # << >> THEN
                /\ IF SATekToAuthmsg.type = "ERROR" THEN
                      /\ state' = "SS_Start"
                      /\ UNCHANGED <<cnt2, AuthToTekmsg>>
                   ELSE 
                      IF SATekToAuthmsg.type = "DONE" THEN
                         /\ state' = "SS_Authorized"
                         /\ cnt2' = cnt2+1 
                         /\ AuthToTekmsg' = [type |-> "AUTHORIZED"]
                      ELSE UNCHANGED <<state, cnt2, AuthToTekmsg>> 
             ELSE UNCHANGED <<state, cnt2, AuthToTekmsg>> 
          /\ Side' = 2
          /\ SATekToAuthmsg' = << >>
          /\ UNCHANGED <<AuthToSATekmsg, SSToBSmsg, BStoSSmsg, TekPkmid,
                         AuthPkmid, AuthPend, AuthGraceTimer, AuthWaitTimer, retry>>

Trans3 == /\ state = "SS_Authorized"
          /\ Side = 1 
          /\ IF BStoSSmsg # << >> /\ BStoSSmsg.type = "AUTH_INV" THEN
                      /\ IF \/ BStoSSmsg.pkmID > 0 /\ BStoSSmsg.pkmID = TekPkmid 
                            \/ BStoSSmsg.pkmID = 0 THEN                            
                            /\ SSToBSmsg'= [type |-> " RSA_REQ", pkmID |-> AuthPkmid, MSrand |->1,  MScert |-> MScertificate, 
                                              SigSS |-> 1 ]
                            /\ IF BStoSSmsg.pkmID = TekPkmid THEN
                                  /\ AuthToTekmsg' = [type |-> "AUTH_PEND"]
                                  /\ IF TekPkmid = MaxReal THEN
                                        /\ TekPkmid' = 1
                                     ELSE 
                                        /\ TekPkmid' = TekPkmid+1
                                  /\ AuthPend' = 1
                               ELSE
                                  /\ UNCHANGED <<AuthToTekmsg, AuthPend, TekPkmid>>
                            /\ state' = "SS_Reauth_Wait"
                            /\ UNCHANGED <<AuthGraceTimer, retry>>
                         ELSE UNCHANGED <<state, AuthPend, TekPkmid, AuthToTekmsg, AuthGraceTimer, SSToBSmsg, retry>>                   
             ELSE
                IF AuthGraceTimer = 4 THEN                   
                   /\ SSToBSmsg'= [type |-> " RSA_REQ", pkmID |-> AuthPkmid, MSrand |->1,  MScert |-> MScertificate, 
                                     SigSS |-> 1 ]
                   (* /\ retry' = retry+1 *)
                   /\ state' = "SS_Reauth_Wait"
                   /\ AuthGraceTimer' = 0
                   /\ UNCHANGED <<AuthPend, TekPkmid, AuthToTekmsg, retry>>
                ELSE
                   /\ AuthGraceTimer' = AuthGraceTimer + 1
                   /\ UNCHANGED <<state, SSToBSmsg,  TekPkmid, AuthPend, AuthToTekmsg, retry>>
          /\ Side' = 2
          /\ BStoSSmsg' = << >>
          /\ UNCHANGED <<AuthToSATekmsg, SATekToAuthmsg, AuthPkmid,  
                         cnt2, AuthWaitTimer>> 

Trans4 == /\ state = "SS_Reauth_Wait"
          /\ Side = 1
          /\ IF /\ BStoSSmsg # << >>
                /\ BStoSSmsg.type = " RSA_REP"
                /\ BStoSSmsg.pkmID = AuthPkmid
                /\ BStoSSmsg.MSrand = 1
                /\ BStoSSmsg.BScert = BScertificate                      
             THEN                      
                      /\ AuthToSATekmsg' = [type |-> "SATEK_START"]                      
                      /\ SSToBSmsg' = [type |-> " RSA_ACK", pkmID |-> BStoSSmsg.pkmID, BSrand |-> BStoSSmsg.BSrand, 
                                         subtype |-> "SUCCESS", SigSS |-> 1]
                      /\ state' = "SS_Reauth_SATek_Wait"
                      /\ UNCHANGED AuthPkmid                         
                      /\ UNCHANGED <<AuthToTekmsg, AuthPend, TekPkmid, AuthToTekmsg, AuthWaitTimer, retry>>
             ELSE
                IF BStoSSmsg # << >> /\ BStoSSmsg.type = "AUTH_INV" /\ BStoSSmsg.pkmID = TekPkmid THEN
                               /\ AuthToTekmsg' = [type |-> "AUTH_PEND"]
                               /\ IF TekPkmid = MaxReal THEN
                                     /\ TekPkmid' = 1
                                  ELSE 
                                     /\ TekPkmid' = TekPkmid+1
                               /\ AuthPend' = 1
                               /\ IF AuthWaitTimer = 2 THEN                                      
                                    /\ SSToBSmsg'= [type |-> " RSA_REQ", pkmID |-> AuthPkmid, MSrand |-> 1, MScert |-> MScertificate, 
                                               SigSS |-> 1 ]
                                    (* /\ retry' = retry+1 *)
                                    /\ AuthWaitTimer' = 0
                                    /\ UNCHANGED <<AuthPkmid, state, AuthToSATekmsg, 
                                              retry>>
                                  ELSE
                                     /\ AuthWaitTimer' = AuthWaitTimer + 1	
                                     /\ UNCHANGED <<AuthPkmid, SSToBSmsg,  state, AuthToSATekmsg, 
                                                retry>>
                               /\ UNCHANGED <<AuthPkmid, state, AuthToSATekmsg, retry>>
                ELSE  /\ UNCHANGED <<AuthPend, TekPkmid>> 
                      /\ IF /\ BStoSSmsg # << >>
                            /\ BStoSSmsg.type = " RSA_REJ"
                            /\ BStoSSmsg.pkmID = AuthPkmid
                            /\ BStoSSmsg.MSrand = 1
                            /\ BStoSSmsg.BScert = BScertificate
                            /\ BStoSSmsg.SigBS = 2
                         THEN
                            /\ IF BStoSSmsg.subtype = "PERM" THEN                      
                                  /\ state' = "SS_Silent"
                               ELSE
                                  /\ state' = "SS_Auth_Reject_Wait"
                            /\ AuthToTekmsg' = [type |-> "STOP"]                            
                            /\ SSToBSmsg' = [type |-> " RSA_ACK", pkmID |-> BStoSSmsg.pkmID, BSrand |-> BStoSSmsg.BSrand, 
                                               subtype |-> "FAILURE", SigSS |-> 1]
                            /\ UNCHANGED AuthPkmid
                               (* IF AuthPkmid = MaxReal THEN
                                  /\ AuthPkmid' = 1
                               ELSE 
                                  /\ AuthPkmid' = AuthPkmid+1 *)
                            /\ UNCHANGED <<AuthToSATekmsg, AuthPend, TekPkmid, AuthWaitTimer, retry>>
                         ELSE 
                           IF AuthWaitTimer = 2 THEN                                      
                              /\ SSToBSmsg'= [type |-> " RSA_REQ", pkmID |-> AuthPkmid, MSrand |-> 1, MScert |-> MScertificate, 
                                               SigSS |-> 1 ]
                              (* /\ retry' = retry+1 *)
                              /\ AuthWaitTimer' = 0
                              /\ UNCHANGED <<AuthPkmid, AuthToTekmsg, state, AuthToSATekmsg, 
                                              AuthPend, TekPkmid, AuthToTekmsg, retry>>
                           ELSE
                              /\ AuthWaitTimer' = AuthWaitTimer + 1	
                              /\ UNCHANGED <<AuthPkmid, SSToBSmsg,  AuthToTekmsg, state, AuthToSATekmsg, 
                                          AuthPend, TekPkmid, AuthToTekmsg, retry>>                         
          /\ Side' = 2
          /\ BStoSSmsg' = << >>
          /\ UNCHANGED <<SATekToAuthmsg, cnt2, AuthGraceTimer>>

Trans5 == /\ state = "SS_Reauth_SATek_Wait"
          /\ Side = 1
          /\ IF SATekToAuthmsg # << >> THEN
                /\ IF SATekToAuthmsg.type = "ERROR" THEN
                      /\ state' = "SS_Start"
                      /\ AuthToTekmsg' = [type |-> "STOP"]
                      /\ UNCHANGED <<cnt2, AuthPend>>
                   ELSE IF SATekToAuthmsg.type = "DONE" THEN
                           /\ IF AuthPend = 1 THEN
                                 /\ AuthToTekmsg' = [type |-> "AUTH_COMP"]
                                 /\ AuthPend' = 0
                              ELSE
                                 /\ UNCHANGED <<AuthToTekmsg, AuthPend>>
                           /\ cnt2' = cnt2+1 
                           /\ state' = "SS_Authorized"
                        ELSE UNCHANGED <<state, AuthPend, AuthToTekmsg, cnt2>>
             ELSE UNCHANGED <<state, AuthToTekmsg, AuthPend, cnt2>>
          /\ Side' = 2
          /\ SATekToAuthmsg' = << >>
          /\ UNCHANGED <<AuthToSATekmsg, SSToBSmsg, BStoSSmsg, TekPkmid,
                         AuthPkmid, AuthGraceTimer, AuthWaitTimer, retry>>

Trans6 == /\ state = "SS_Auth_Reject_Wait"
          /\ Side = 1
          /\ state' = "SS_Start"
          /\ Side' = 2
          /\ UNCHANGED <<AuthToTekmsg, AuthToSATekmsg, SSToBSmsg, SATekToAuthmsg, BStoSSmsg, 
                         TekPkmid, AuthPkmid, AuthPend, AuthGraceTimer, cnt2, AuthWaitTimer, retry>> 

(*
Trans7 == /\ Side = 1 
          /\ cnt2<=NUM 
          /\ retry>NUM*3
          /\ Print("Stop", TRUE)
          /\ state' = "Stop"
          /\ UNCHANGED <<AuthToTekmsg, AuthToSATekmsg, SATekToAuthmsg, BStoSSmsg,  
                          SSToBSmsg, Side, TekPkmid, AuthPkmid, AuthPend, AuthGraceTimer, cnt2, AuthWaitTimer, retry>>         
                          
Trans8 == /\ cnt2>NUM
          /\ Side = 1
          /\ state # "Over"
          /\ Print("Over", TRUE)
          /\ state' = "Over"    
          /\ UNCHANGED <<AuthToTekmsg, AuthToSATekmsg, SATekToAuthmsg, BStoSSmsg, 
                          SSToBSmsg, Side, TekPkmid, AuthPkmid, AuthPend, AuthGraceTimer, cnt2, AuthWaitTimer, retry>>         
*)

vars == <<state, cnt2, AuthPkmid, AuthPend, AuthGraceTimer, AuthWaitTimer, retry, AuthToTekmsg, AuthToSATekmsg, SSToBSmsg, SATekToAuthmsg, BStoSSmsg, Side, TekPkmid>>


Liveness == /\ WF_vars(Trans0) /\ WF_vars(Trans1) /\ WF_vars(Trans2) /\ WF_vars(Trans3) /\ WF_vars(Trans4) 
            /\ SF_vars(Trans5) /\ WF_vars(Trans6) (* /\ WF_vars(Trans7) /\ WF_vars(Trans8) *)
           
Next == /\ \/ Trans0 
           \/ Trans1 
           \/ Trans2 
           \/ Trans3 
           \/ Trans4 
           \/ Trans5 
           \/ Trans6           
           (*
           \/ Trans7 
           \/ Trans8 *)
        /\ UNCHANGED <<varsSSTek, varsSATek, varsBS, varsAT>>
      
SSSpec == Init /\ [][Next]_vars /\ Liveness

=======================================================================

---------------------------MODULE SATek--------------------------------

VARIABLES state, SATekPkmID, challengeTimer, responseTimer

Init == /\ state = "SATek_Start"                
        /\ SATekPkmID = 1        
        /\ challengeTimer = 0
        /\ responseTimer = 0
        
Trans0 == /\ state = "SATek_Start"
          /\ Side = 2   
          /\ IF AuthToSATekmsg # << >> 
                /\ AuthToSATekmsg.type = "SATEK_START"
             THEN
               /\ state' = "SATek_Challenge_Wait"                                 
               /\ AuthToSATekmsg' = << >>
             ELSE UNCHANGED <<state,  AuthToSATekmsg>>            
          /\ Side' = 3
          /\ UNCHANGED <<AuthToTekmsg, SATekToAuthmsg, BStoSSmsg, SSToBSmsg, 
                         TekPkmid, SATekPkmID, challengeTimer, responseTimer>>

Trans1 == /\ state = "SATek_Challenge_Wait"
          /\ Side = 2                     
          /\ IF /\ BStoSSmsg # << >>          
                /\ BStoSSmsg.type = "SATEK_CH"          
                /\ BStoSSmsg.HMAC = 2
             THEN                
                /\ SSToBSmsg' = [type |-> "SATEK_RQ", pkmID |-> BStoSSmsg.pkmID, MSrand |->1,  BSrand |-> BStoSSmsg.BSrand, 
                                    HMAC |-> 1]
                /\ state' = "SATek_Response_Wait"
                /\ SATekPkmID' = BStoSSmsg.pkmID
                /\ UNCHANGED <<challengeTimer, SATekToAuthmsg>>
             ELSE
                /\ IF challengeTimer = 3 THEN
                     /\ state' = "SATek_Start"
                     /\ SATekToAuthmsg' = [type |-> "ERROR"]
                     /\ challengeTimer' = 0
                   ELSE
                     /\ challengeTimer' = challengeTimer + 1
                     /\ UNCHANGED <<state, SATekToAuthmsg>>
                /\ UNCHANGED <<SSToBSmsg, SATekPkmID>>
          /\ BStoSSmsg' = << >>
          /\ Side' = 3          
          /\ UNCHANGED <<AuthToTekmsg, AuthToSATekmsg, TekPkmid,  
                         responseTimer>>

Trans2 == /\ state = "SATek_Response_Wait"
          /\ Side = 2
          /\ IF              
               /\ BStoSSmsg # << >>
               /\ BStoSSmsg.type = "SATEK_RP"                    
               /\ BStoSSmsg.pkmID = SATekPkmID          
               /\ BStoSSmsg.MSrand = 1          
               /\ BStoSSmsg.HMAC = 2
             THEN
               /\ SATekToAuthmsg' = [type |-> "DONE"]               
               /\ BStoSSmsg' = << >>
               /\ state' = "SATek_Start"
               /\ UNCHANGED <<responseTimer, SSToBSmsg>>    
             ELSE
               IF responseTimer = 3 THEN
                  /\ state' = "SATek_Start"
                  /\ SATekToAuthmsg' = [type |-> "ERROR"]
                  /\ responseTimer' = 0
                  /\ UNCHANGED << BStoSSmsg, SSToBSmsg>>
               ELSE
                  /\ responseTimer' = responseTimer + 1
                  /\ SSToBSmsg' = [type |-> "SATEK_RQ", pkmID |-> SATekPkmID, MSrand |-> 1, BSrand |->2, 
                                      HMAC |-> 1]
                  /\ UNCHANGED << BStoSSmsg, state, SATekToAuthmsg>>
          /\ Side' = 3
          /\ UNCHANGED <<AuthToTekmsg, AuthToSATekmsg, TekPkmid, 
                         challengeTimer, SATekPkmID>>

vars == <<state, SATekPkmID, challengeTimer, responseTimer, AuthToTekmsg, AuthToSATekmsg, SSToBSmsg, SATekToAuthmsg, BStoSSmsg, Side, TekPkmid>>

Liveness == /\ WF_vars(Trans0) /\ WF_vars(Trans1) /\ WF_vars(Trans2) 

Next == /\ \/ Trans0
           \/ Trans1           
           \/ Trans2
        /\ UNCHANGED <<varsSSAuth, varsBS, varsSSTek, varsAT>>
        
      
SATekSpec == Init /\ [][Next]_vars /\ Liveness

======================================================================= 

---------------------------MODULE SSTek--------------------------------

VARIABLES state, TekKeyTimeout, nonce

Init ==   /\ state = "Tek_Start"          
          /\ TekKeyTimeout = 1
          /\ nonce = 3          
          
Trans0 == /\ state = "Tek_Start"          
          /\ Side = 3 
          /\ IF AuthToTekmsg # << >> 
                /\ AuthToTekmsg.type = "AUTHORIZED" 
             THEN                
                /\ state' = "Tek_Wait"                
                /\ SSToBSmsg' = [type |-> " KEY_REQ", pkmID |-> TekPkmid, KeySequence |-> AuthKeySeq, Nonce |-> nonce, HMAC |-> 1]
                /\ AuthToTekmsg' = << >>              
             ELSE
                UNCHANGED <<state, SSToBSmsg, AuthToTekmsg>>
          /\ Side' = 5
          /\ UNCHANGED <<AuthToSATekmsg, SATekToAuthmsg, BStoSSmsg, 
                         TekPkmid, TekKeyTimeout, nonce>>

Trans1 == /\ state = "Tek_Wait"
          /\ Side = 3 
          /\ IF /\ BStoSSmsg # << >>
                /\ BStoSSmsg.type = " KEY_REP"
                /\ BStoSSmsg.Nonce = nonce
                /\ BStoSSmsg.pkmID = TekPkmid
                /\ BStoSSmsg.HMAC = 2 
             THEN
                   /\ state' = "Tek_Operational"
                   /\ IF TekPkmid = MaxReal THEN
                        /\ TekPkmid' = 1
                      ELSE 
                        /\ TekPkmid' = TekPkmid+1                      
             ELSE
                      IF /\ BStoSSmsg # << >>
                         /\ BStoSSmsg.type = " KEY_REJ"
                         /\ BStoSSmsg.Nonce = nonce
                         /\ BStoSSmsg.pkmID = TekPkmid
                         /\ BStoSSmsg.HMAC = 2 
                      THEN
                           /\ state' = "Tek_Start"
                           /\ IF TekPkmid = MaxReal THEN
                                /\ TekPkmid' = 1
                              ELSE 
                                /\ TekPkmid' = TekPkmid+1                                                 
                      ELSE
                         IF AuthToTekmsg # << >> THEN
	                          IF AuthToTekmsg.type = "STOP" THEN
                              /\ state' = "Tek_Start"
                              /\ IF TekPkmid = MaxReal THEN
                                    /\ TekPkmid' = 1
                                 ELSE 
                                    /\ TekPkmid' = TekPkmid+1                      
	                          ELSE
	                            IF AuthToTekmsg.type = "AUTH_PEND" THEN
                                 /\ state' = "Tek_OP_Reauth_Wait"
                                 /\ UNCHANGED <<TekPkmid>>
                              ELSE UNCHANGED <<state, TekPkmid>>             
                         ELSE UNCHANGED<<state, TekPkmid>>
          /\ Side' = 5
          /\ BStoSSmsg' = << >>
          /\ AuthToTekmsg' = << >>
          /\ UNCHANGED <<AuthToSATekmsg, SATekToAuthmsg, SSToBSmsg, 
                         TekKeyTimeout, nonce>>

Trans2 == /\ state = "Tek_Operational"          
          /\ Side = 3          
          /\ IF AuthToTekmsg # << >> THEN
                /\ IF AuthToTekmsg.type = "STOP" THEN
                      /\ state' = "Tek_Start"
                   ELSE UNCHANGED <<state>>
                /\ UNCHANGED <<TekPkmid, SSToBSmsg, TekKeyTimeout>>
             ELSE 
                IF /\ BStoSSmsg # << >>
                   /\ BStoSSmsg.type = " TEK_INV" 
                   /\ BStoSSmsg.pkmID = TekPkmid
                   /\ BStoSSmsg.HMAC = 2
                THEN
                   /\ IF TekPkmid = MaxReal THEN
                         /\ TekPkmid' = 1
                      ELSE 
                         /\ TekPkmid' = TekPkmid+1                  
                   /\ SSToBSmsg' = [type |-> " KEY_REQ", pkmID |-> TekPkmid, KeySequence |-> AuthKeySeq, Nonce |-> nonce, 
                                     HMAC |-> 1]
                   /\ state' = "Tek_Wait"
                   /\ UNCHANGED <<TekKeyTimeout>>
                ELSE
                   /\ IF TekKeyTimeout = 2 THEN
                         /\ state' = "Tek_Rekey_Wait"
                         /\ TekKeyTimeout' = 1                         
                         /\ SSToBSmsg' = [type |-> " KEY_REQ", pkmID |-> TekPkmid, KeySequence |-> AuthKeySeq, Nonce |-> nonce, 
                                           HMAC |-> 1]
                      ELSE
                         /\ TekKeyTimeout' = TekKeyTimeout+1
                         /\ UNCHANGED <<state, SSToBSmsg>>
                   /\ UNCHANGED <<TekPkmid>>
          /\ Side' = 5
          /\ AuthToTekmsg' = << >>
          /\ BStoSSmsg' = << >>
          /\ UNCHANGED <<AuthToSATekmsg, SATekToAuthmsg, nonce>>

Trans3 == /\ state = "Tek_Rekey_Wait"
          /\ Side = 3               
          /\ IF AuthToTekmsg # << >> THEN
                 /\ IF AuthToTekmsg.type = "STOP" THEN
                      /\ state' = "Tek_Start"
                      /\ IF TekPkmid = MaxReal THEN
                            /\ TekPkmid' = 1
                         ELSE 
                            /\ TekPkmid' = TekPkmid+1
                      /\ UNCHANGED <<SSToBSmsg, nonce>>
                    ELSE
                      IF AuthToTekmsg.type = "AUTH_PEND" THEN
                         /\ state' = "Tek_Rekey_Reauth_Wait"
                         /\ UNCHANGED <<TekPkmid, TekPkmid, SSToBSmsg>>
                      ELSE UNCHANGED <<TekPkmid, state, TekPkmid, SSToBSmsg>>
             ELSE                
               /\ IF  /\ BStoSSmsg # << >>
                      /\ BStoSSmsg.type = " KEY_REP"
                      /\ BStoSSmsg.pkmID = TekPkmid
                      /\ BStoSSmsg.Nonce = nonce
                      /\ BStoSSmsg.HMAC = 2
                  THEN
                      /\ state' = "Tek_Operational"
                      /\ IF TekPkmid = MaxReal THEN
                            /\ TekPkmid' = 1
                         ELSE 
                            /\ TekPkmid' = TekPkmid+1                      
                      /\ UNCHANGED <<SSToBSmsg>>
                  ELSE
                      IF /\ BStoSSmsg # << >> 
                         /\ BStoSSmsg.type = " KEY_REJ"
                         /\ BStoSSmsg.Nonce = nonce
                         /\ BStoSSmsg.pkmID = TekPkmid
	                       /\ BStoSSmsg.HMAC = 2
	                    THEN
                         /\ state' = "Tek_Start"
                         /\ IF TekPkmid = MaxReal THEN
                               /\ TekPkmid' = 1
                            ELSE 
                               /\ TekPkmid' = TekPkmid+1
                         /\ UNCHANGED <<SSToBSmsg, nonce>>
                      ELSE 
                         IF /\ BStoSSmsg # << >>
                            /\ BStoSSmsg.type = " TEK_INV" 
                            /\ BStoSSmsg.pkmID = TekPkmid
                            /\ BStoSSmsg.HMAC = 2
                         THEN
                            /\ IF TekPkmid = MaxReal THEN
                                  /\ TekPkmid' = 1
                               ELSE 
                                  /\ TekPkmid' = TekPkmid+1                            
                            /\ SSToBSmsg' = [type |-> " KEY_REQ", pkmID |-> TekPkmid, Nonce |-> nonce, 
                                              HMAC |-> 1]
                            /\ state' = "Tek_Wait"                            
                         ELSE UNCHANGED <<TekPkmid, state, SSToBSmsg>>
          /\ Side' = 5
          /\ AuthToTekmsg' = << >>
          /\ BStoSSmsg' = << >>
          /\ UNCHANGED <<AuthToSATekmsg, SATekToAuthmsg, TekKeyTimeout, nonce>>

Trans4 == /\ state = "Tek_Rekey_Reauth_Wait"
          /\ Side = 3
          /\ IF AuthToTekmsg # << >> THEN
                /\ IF AuthToTekmsg.type = "AUTH_COMP" THEN
                      /\ state' = "Tek_Rekey_Wait"
                      /\ SSToBSmsg' = [type |-> " KEY_REQ", pkmID |-> TekPkmid, Nonce |-> nonce, 
                                        HMAC |-> 1]
                   ELSE
                      IF AuthToTekmsg.type = "STOP" THEN
                         /\ state' = "Tek_Start"
                         /\ UNCHANGED <<SSToBSmsg>>
                      ELSE UNCHANGED <<state, SSToBSmsg>>
                /\ UNCHANGED <<TekPkmid>>
             ELSE
                /\ IF BStoSSmsg # << >>
                     /\ BStoSSmsg.type = " TEK_INV"
                     /\ BStoSSmsg.pkmID = TekPkmid
                     /\ BStoSSmsg.HMAC = 2
                   THEN
                     /\ state' = "Tek_OP_Reauth_Wait"          
                     /\ IF TekPkmid = MaxReal THEN
                           /\ TekPkmid' = 1
                        ELSE 
                           /\ TekPkmid' = TekPkmid+1
                   ELSE UNCHANGED <<state, TekPkmid>>
                /\ UNCHANGED <<SSToBSmsg>>
          /\ Side' = 5
          /\ BStoSSmsg' = << >>
          /\ AuthToTekmsg' = << >>
          /\ UNCHANGED <<AuthToSATekmsg, SATekToAuthmsg, TekKeyTimeout, nonce>>

Trans5 == /\ state = "Tek_OP_Reauth_Wait"
          /\ Side = 3
          /\ IF AuthToTekmsg # << >> THEN
                /\ IF AuthToTekmsg.type = "AUTH_COMP" THEN
                      /\ SSToBSmsg' = [type |-> " KEY_REQ", pkmID |-> TekPkmid, KeySequence |-> AuthKeySeq, Nonce |-> nonce, 
                                        HMAC |-> 1]
                      /\ state' = "Tek_Wait"         
                   ELSE
                      IF AuthToTekmsg.type = "STOP" THEN
                         /\ state' = "Tek_Start"
                         /\ UNCHANGED <<SSToBSmsg>>
                      ELSE UNCHANGED <<state, SSToBSmsg>>
             ELSE UNCHANGED <<SSToBSmsg, state>>
          /\ Side' = 5
          /\ AuthToTekmsg' = << >>
          /\ UNCHANGED <<AuthToSATekmsg, SATekToAuthmsg, BStoSSmsg, TekPkmid, 
                         TekKeyTimeout, nonce>>

vars == <<state, TekKeyTimeout, nonce, AuthToTekmsg, AuthToSATekmsg, SSToBSmsg, SATekToAuthmsg, BStoSSmsg, Side, TekPkmid>>

Liveness == /\ WF_vars(Trans0) /\ WF_vars(Trans1) /\ WF_vars(Trans2) /\ WF_vars(Trans3) /\ WF_vars(Trans4) 
            /\ WF_vars(Trans5) 


Next == /\ \/ Trans0
           \/ Trans1
           \/ Trans2
           \/ Trans3
           \/ Trans4           
           \/ Trans5
        /\ UNCHANGED <<varsSSAuth, varsSATek, varsBS, varsAT>>
        
TekSpec == Init /\ [][Next]_vars /\ Liveness

=======================================================================

---------------------------MODULE BS-----------------------------------

VARIABLES state, pkmid, reqTimer

Init == /\ state = "BS_Start"                
        /\ pkmid = 1
        /\ reqTimer = 0
        
Trans0 == /\ state = "BS_Start"
          /\ Side = 4            
          /\ IF SSToBSmsg # << >> /\ SSToBSmsg.type = " RSA_REQ" THEN
                /\ IF SSToBSmsg.MScert = MScertificate THEN
                      /\ IF SSToBSmsg.SigSS = 1 THEN
                            /\ BStoSSmsg' = [type |-> " RSA_REP", pkmID |-> SSToBSmsg.pkmID, MSrand |-> SSToBSmsg.MSrand,
                                               BSrand |->2, BScert |-> BScertificate, SigBS |-> 2]
                            /\ state' = "BS_RSA_REP_Sent"
                         ELSE (* Send NPERM reject message *)                                                  
                            /\ BStoSSmsg' = [type |-> " RSA_REJ", pkmID |-> SSToBSmsg.pkmID, MSrand |-> SSToBSmsg.MSrand,
                                               BSrand |->2,  subtype |-> "NPERM", BScert |-> BScertificate, SigBS |-> 2]
                            /\ state' = "BS_RSA_REJ_Sent"                            
                   ELSE (* Send PERM reject message *)                  
                      /\ BStoSSmsg' = [type |-> " RSA_REJ", pkmID |-> SSToBSmsg.pkmID, MSrand |-> SSToBSmsg.MSrand,
                                         BSrand |->2,  subtype |-> "PERM", BScert |-> BScertificate, SigBS |-> 2]
                      /\ state' = "BS_RSA_REJ_Sent"                                      
             ELSE
                /\ IF SSToBSmsg # << >> /\ SSToBSmsg.type = " KEY_REQ" THEN                   
                     /\ IF SSToBSmsg.HMAC = 1 THEN
                           /\ IF SSToBSmsg.KeySequence = AuthKeySeq THEN
                                 /\ BStoSSmsg' = [type |-> " KEY_REP", pkmID |-> SSToBSmsg.pkmID, TEKold |-> TEKkey, TEKnew |-> TEKkey,
                                                   Nonce |-> SSToBSmsg.Nonce, HMAC |-> 2]                                 
                              ELSE
                                 /\ BStoSSmsg' = [type |-> " KEY_REJ", pkmID |-> SSToBSmsg.pkmID,
                                                  Nonce |-> SSToBSmsg.Nonce, HMAC |-> 2]                                 
                        ELSE                            
                            /\ BStoSSmsg' = [type |-> "AUTH_INV", pkmID |-> SSToBSmsg.pkmID]                            
                     /\ UNCHANGED <<state>>
                  ELSE
                     BStoSSmsg' = << >>
                /\ UNCHANGED <<state>>
          /\ Side' = 6
          /\ SSToBSmsg' = << >>          
          /\ UNCHANGED <<AuthToTekmsg, AuthToSATekmsg, SATekToAuthmsg, TekPkmid,  pkmid, reqTimer>>

Trans3 == /\ state = "BS_RSA_REP_Sent"
          /\ Side = 4
          /\ IF SSToBSmsg # << >> /\ SSToBSmsg.type = " RSA_ACK" THEN
                /\ IF SSToBSmsg.subtype = "SUCCESS" /\ SSToBSmsg.BSrand = 2 /\ SSToBSmsg.SigSS = 1 THEN
                      /\ state' = "BS_SATek_Start"                      
                   ELSE
                      /\ state' = "BS_Start"
             ELSE 
                /\ state' = "BS_Start"                
          /\ Side' = 6
          /\ SSToBSmsg' = << >>          
          /\ UNCHANGED <<AuthToTekmsg, AuthToSATekmsg, SATekToAuthmsg, BStoSSmsg, 
                         TekPkmid,  pkmid, reqTimer>>

Trans4 == /\ state = "BS_RSA_REJ_Sent"
          /\ Side = 4
          /\ IF /\ SSToBSmsg # << >> 
                /\ SSToBSmsg.type = " RSA_ACK"
                /\ SSToBSmsg.BSrand = 2
             THEN
                /\ state' = "BS_Start"
             ELSE                 
                /\ state' = "BS_Start"                
          /\ Side' = 6
          /\ SSToBSmsg' = << >>
          /\ UNCHANGED <<AuthToTekmsg, AuthToSATekmsg, SATekToAuthmsg, BStoSSmsg, 
                         TekPkmid, pkmid, reqTimer>>


Trans5 == /\ state = "BS_SATek_Start"
          /\ Side = 4
          /\ BStoSSmsg' = [type |-> "SATEK_CH", pkmID |-> pkmid, BSrand |-> 2, HMAC |-> 2 ]
          /\ Side' = 6
          /\ state' = "BS_SATek_Req_Wait"
          /\ UNCHANGED <<AuthToTekmsg, AuthToSATekmsg, SSToBSmsg, SATekToAuthmsg,  
                         TekPkmid, pkmid, reqTimer>>

Trans6 == /\ state = "BS_SATek_Req_Wait"
          /\ Side = 4                    
          /\ IF 
               /\ SSToBSmsg # << >>
               /\ SSToBSmsg.type = "SATEK_RQ"
               /\ SSToBSmsg.pkmID = pkmid
               /\ SSToBSmsg.BSrand = 2
               /\ SSToBSmsg.HMAC = 1                                
             THEN               
               /\ BStoSSmsg' = [type |-> "SATEK_RP", pkmID |-> SSToBSmsg.pkmID, MSrand |-> SSToBSmsg.MSrand, 
                              BSrand |-> 2, SAdesc |-> 1222, HMAC |-> 2]                              
               /\ state' = "BS_Start"
               /\ SSToBSmsg' = << >>
               /\ UNCHANGED <<reqTimer, pkmid>>
             ELSE
               IF reqTimer = 3 THEN
                 /\ state' = "BS_Start"
                 /\ reqTimer' = 0
                 /\ UNCHANGED <<BStoSSmsg, SSToBSmsg, pkmid>>
               ELSE
                 /\ reqTimer' = reqTimer + 1
                 /\ IF pkmid = MaxReal THEN
                       /\ pkmid'=1
                    ELSE
                       /\ pkmid' = pkmid+1
                 /\ BStoSSmsg' = [type |-> "SATEK_CH", pkmID |-> pkmid', BSrand |->2, HMAC |-> 2]
                 /\ SSToBSmsg' = << >>
                 /\ UNCHANGED <<state>>
          /\ Side' = 6
          /\ UNCHANGED <<AuthToTekmsg, AuthToSATekmsg, SATekToAuthmsg, TekPkmid>>           

vars == <<state, pkmid, reqTimer, AuthToTekmsg, AuthToSATekmsg, SSToBSmsg, SATekToAuthmsg, BStoSSmsg, Side, TekPkmid>>

Liveness == /\ WF_vars(Trans0) /\ WF_vars(Trans3) /\ WF_vars(Trans4) /\ WF_vars(Trans5) /\ WF_vars(Trans6)             
          
Next == /\ \/ Trans0
           \/ Trans3
           \/ Trans4
           \/ Trans5
           \/ Trans6           
        /\ UNCHANGED <<varsSSAuth, varsSATek, varsSSTek, varsAT>>        
      
BSSpec == Init /\ [][Next]_varsBS /\ Liveness
=======================================================================

---------------------------MODULE Attacker-------------------------------

VARIABLES state, knowledge, MSGset, cnt

Init == /\ state = "AT_init"           
        /\ cnt = 1    
        /\ knowledge = [mesTypes |-> 
            {" RSA_REQ", " RSA_REP", " RSA_REJ", " RSA_ACK", "SATEK_CH", "SATEK_RQ", "SATEK_RP", " KEY_REQ", " KEY_REP", " KEY_REJ", "AUTH_INV", 
            " TEK_INV", "AUTH_INF", "ERROR", "DONE", "AUTH_COMP", "AUTH_PEND", "STOP"}, pkmID |-> {1}, messages|-> {}]
        /\ MSGset = {}        

Read == /\ Side = 5 \/ Side = 6
        /\ state = "AT_init"
        /\ state' = "AT_Read"
        /\ MSGset' = {SSToBSmsg, BStoSSmsg}\{<< >>}           
        /\ UNCHANGED <<AuthToTekmsg, AuthToSATekmsg, SSToBSmsg, SATekToAuthmsg, BStoSSmsg,
              Side, TekPkmid, knowledge, cnt>>

ReadMessages == /\ state = "AT_Read"                
                /\ IF MSGset # {} /\ \E msg \in MSGset : msg.type \in {" RSA_REQ", " RSA_REP", " RSA_REJ", " RSA_ACK", "SATEK_CH", "SATEK_RQ", "SATEK_RP", " KEY_REQ", " KEY_REP", " KEY_REJ", "AUTH_INV", 
                     " TEK_INV", "AUTH_INF"} THEN
                     LET
                       msg == CHOOSE ps \in MSGset: TRUE
                     IN
                       /\ IF "pkmID" \in DOMAIN msg THEN
                            /\ knowledge' = [knowledge EXCEPT !.messages=@\cup{msg}, !.pkmID =@\cup{msg.pkmID}]
                          ELSE
                            /\ knowledge' = [knowledge EXCEPT !.messages=@\cup{msg}]
                       /\ MSGset' = MSGset\{msg}
                       /\ UNCHANGED <<state>>           
                   ELSE /\ state' = "AT_Write"             
                        /\ UNCHANGED <<knowledge, MSGset>>                
                /\ UNCHANGED <<AuthToTekmsg, AuthToSATekmsg, SSToBSmsg, SATekToAuthmsg, BStoSSmsg,
                     Side, TekPkmid, cnt>>
                       
SWrite       == /\ Side = 5
                /\ state = "AT_Write"                
                /\ \E sel \in {"Op", "Noop"}:                     
                     /\ IF sel="Op" THEN
                          \E msg \in knowledge.messages:
                             /\ IF msg.type = " KEY_REQ" THEN
                                     /\ IF SSToBSmsg # << >> /\ cnt<CNTN THEN 
                                          /\ SSToBSmsg' = << >>  (* erase *)
                                          /\ cnt' = cnt+1
                                        ELSE 
                                          /\ IF SSToBSmsg = << >> THEN
                                                 SSToBSmsg' = [msg EXCEPT !.Nonce= 10]
                                             ELSE
                                                 UNCHANGED SSToBSmsg
                                          /\ UNCHANGED cnt
                                ELSE
                                  IF msg.type \in {"SATEK_RQ"}  THEN
                                     /\ IF SSToBSmsg # << >> /\ cnt<CNTN THEN                      
                                          /\ SSToBSmsg' = << >> (* erase *)
                                          /\ cnt' = cnt+1
                                        ELSE    
                                          /\ IF SSToBSmsg = << >> THEN                                                        
                                                SSToBSmsg' = [msg EXCEPT !.MSrand = 11, !.BSrand = 12]
                                             ELSE
                                                UNCHANGED SSToBSmsg
                                          /\ UNCHANGED cnt
                                  ELSE
                                    IF msg.type \in {" RSA_REQ", " RSA_ACK"}  THEN
                                      IF SSToBSmsg # << >> /\ cnt<CNTN THEN                      
                                         /\ SSToBSmsg' = << >> (* erase *)
                                         /\ cnt' = cnt+1
                                      ELSE
                                          /\ IF SSToBSmsg = << >> THEN                                                        
                                                IF msg.type = " RSA_REQ" THEN
                                                   SSToBSmsg' = [msg EXCEPT !.MSrand = 11]
                                                ELSE
                                                   SSToBSmsg' = [msg EXCEPT !.BSrand = 12]    
                                             ELSE
                                                UNCHANGED SSToBSmsg
                                          /\ UNCHANGED cnt
                                    ELSE UNCHANGED <<SSToBSmsg, cnt>>
                        ELSE UNCHANGED <<SSToBSmsg, cnt>>
                 /\ state' = "AT_init"
                 /\ Side' = 4
                 /\ UNCHANGED <<AuthToTekmsg, AuthToSATekmsg, SATekToAuthmsg, BStoSSmsg, TekPkmid, knowledge, MSGset>>

BWrite       == /\ Side = 6
                /\ state = "AT_Write"
                /\ \E sel \in {"Op", "Noop", "New"}:
                      /\ IF sel="Op" THEN
                          \E msg \in knowledge.messages:
                             /\ IF msg.type \in {" RSA_REP", "AUTH_INV", " RSA_REJ"}  THEN
                                     /\ IF BStoSSmsg # << >> /\ cnt<CNTN THEN                      
                                          /\ BStoSSmsg' = << >> (* erase *)
                                          /\ cnt' = cnt+1
                                        ELSE 
                                          /\ IF BStoSSmsg # << >> THEN
                                                UNCHANGED <<BStoSSmsg>>
                                             ELSE 
                                                IF msg.type = "AUTH_INV" THEN
                                                   BStoSSmsg' = msg
                                                ELSE                                                
                                                  BStoSSmsg' = [msg EXCEPT !.MSrand = 11, !.BSrand = 12]
                                          /\ UNCHANGED cnt
                                ELSE 
                                  IF msg.type \in {"SATEK_CH", "SATEK_RP"}  THEN
                                     /\ IF BStoSSmsg # << >> /\ cnt<CNTN THEN                      
                                          /\ BStoSSmsg' = << >> (* erase *)
                                          /\ cnt' = cnt+1
                                        ELSE
                                           /\ IF BStoSSmsg # << >> THEN
                                                 UNCHANGED <<BStoSSmsg>>
                                              ELSE                                            
                                                 IF msg.type = "SATEK_CH" THEN
                                                    BStoSSmsg' = [msg EXCEPT !.BSrand = 11]
                                                 ELSE
                                                    BStoSSmsg' = [msg EXCEPT !.MSrand = 11, !.BSrand=12]
                                           /\ UNCHANGED cnt
                                  ELSE
                                    IF msg.type \in {" KEY_REP", " KEY_REJ", " TEK_INV"}  THEN
                                      IF BStoSSmsg # << >> /\ cnt<CNTN THEN   
                                         /\ BStoSSmsg' = << >> (* erase *)
                                         /\ cnt' = cnt+1
                                      ELSE
                                        /\ IF BStoSSmsg # << >> THEN
                                              UNCHANGED <<BStoSSmsg>>
                                           ELSE   
                                              IF msg.type # " TEK_INV" THEN                                       
                                                 BStoSSmsg' = [msg EXCEPT !.Nonce = 10]
                                              ELSE
                                                 BStoSSmsg' = msg
                                        /\ UNCHANGED cnt
                                    ELSE UNCHANGED <<BStoSSmsg, cnt>>
                         ELSE IF sel="New" THEN
                                /\ IF BStoSSmsg # << >> /\ cnt<CNTN THEN 
                                     /\ BStoSSmsg' = << >> (* erase *)
                                     /\ cnt' = cnt+1
                                   ELSE
                                     /\ IF BStoSSmsg # << >> THEN
                                          UNCHANGED BStoSSmsg
                                        ELSE
                                          \E id \in knowledge.pkmID:
                                             BStoSSmsg' = [type |-> "AUTH_INV", pkmID |-> id]
                                     /\ UNCHANGED cnt
                                     /\ Print("ABCD", TRUE)
                              ELSE UNCHANGED <<BStoSSmsg, cnt>>
                 /\ state' = "AT_init"
                 /\ Side' = 1
                 /\ UNCHANGED <<AuthToTekmsg, AuthToSATekmsg, SATekToAuthmsg, TekPkmid, SSToBSmsg, knowledge, MSGset>>

(*                 
Next == /\ \/ /\ Side = 6
              /\ Side' = 1
           \/ /\ Side = 5
              /\ Side' = 4
        /\ UNCHANGED <<varsSSAuth, varsSATek, varsSSTek, varsBS, AuthToTekmsg, AuthToSATekmsg, SATekToAuthmsg, TekPkmid, SSToBSmsg, SSToBSmsg, SSToBSmsg, knowledge, MSGset, BStoSSmsg, BStoSSmsg, BStoSSmsg, state, cnt>>
*)

vars == <<state, knowledge, MSGset, cnt, AuthToTekmsg, AuthToSATekmsg, SSToBSmsg, SATekToAuthmsg, BStoSSmsg, Side, TekPkmid>>

Next == /\ \/ Read
           \/ ReadMessages          
           \/ BWrite
           \/ SWrite    
        /\ UNCHANGED <<varsSSAuth, varsSATek, varsSSTek, varsBS>>                          


Liveness == WF_vars(Next)
      
BSSpec == Init /\ [][Next]_varsAT /\ WF_varsAT(Next)
=======================================================================


SSLayer == INSTANCE SSAuth WITH state<- SS_state, AuthPkmid<- SS_AuthPkmid, AuthPend<- SS_AuthPend,
             AuthGraceTimer<- SS_AuthGraceTimer, cnt2<- SS_cnt, AuthWaitTimer<- SS_AuthWaitTimer, retry <- SS_retry

Tek == INSTANCE SSTek WITH state<- Tek_state, TekKeyTimeout<- Tek_TekKeyTimeout, nonce<- Tek_nonce

Base == INSTANCE BS WITH state<- BS_state, pkmid<- BS_pkmid, reqTimer<- BS_reqTimer

SATek == INSTANCE SATek WITH state<- SA_state,  
                  SATekPkmID<- SA_SATekPkmID, challengeTimer<- SA_challengeTimer, 
                  responseTimer<- SA_responseTimer

Terrorist == INSTANCE Attacker WITH state<- AT_state, knowledge<- AT_knowledge, MSGset<- AT_MSGset, cnt <- AT_cnt

(*
TypeInvariant == /\ IF SS_msg # << >> THEN SS_msg \in Message
                    ELSE TRUE
                 /\ IF BS_msg # << >> THEN BS_msg \in Message
                    ELSE TRUE                 
                 /\ Side \in (0 .. Num+2)
*)                

Init == /\ Side = 1        
        /\ AuthToTekmsg = << >>
        /\ AuthToSATekmsg = << >>
        /\ SATekToAuthmsg = << >>
        /\ SSToBSmsg = << >>
        /\ BStoSSmsg = << >>        
        /\ TekPkmid = 1
        /\ SSLayer!Init
        /\ Tek!Init
        /\ Base!Init        
        /\ SATek!Init
        /\ Terrorist!Init

Next == [][SSLayer!Next\/Tek!Next\/Base!Next\/SATek!Next\/Terrorist!Next]_gvars

AuthSpec == Init /\ Next /\ Tek!Liveness /\ SSLayer!Liveness /\ Base!Liveness /\ SATek!Liveness /\ Terrorist!Liveness 

SizeConstraint == /\ SS_cnt<=NUM /\ SS_retry<=NUM*3

Correctness == []<>(SS_state="SS_Authorized")
=======================================================================