--
--

-- IEEE 802.11i 4-way handshake Protocols

-- Feb.18, Changhua He
--

--
-- Parameters
--

const
  
  NONCE_ENABLED:           true;
  SEQUENCE_ENABLED:        true;
  MTYPE_ENABLED:           true;
  ADDRESS_ENABLED:         true;

  NumSupplicants:          1;
  NumAuthenticators:       1;
  NumIntruders:            1;

  NetworkSize:             2;


  MaxSessions:             3;

  MaxNonce:                20;
  MaxSequence:             20;


  -- What intruder can remember
 
  MaxKnowledge:            30;    


type
  SupplicantId:          scalarset(NumSupplicants);
  AuthenticatorId:       scalarset(NumAuthenticators);
  IntruderId:            scalarset(NumIntruders);
  AgentId:               union{SupplicantId, AuthenticatorId, IntruderId};


  Nonce:           0..MaxNonce;
  Sequence:        0..MaxSequence;
  SessionId:       0..MaxSessions;

-- Key modeling

PMK: record
  peer1:           AgentId;   --supplicant
  peer2:           AgentId;   --authenticator
end;


PTK: record
  pmk:              PMK;
  nonce1:           Nonce;    --supplicant nonce
  nonce2:           Nonce;    --authenticator nonce
  address1:         AgentId;  --supplicant
  address2:         AgentId;  --authenticator
end;


--
-- Message Modeling
--

MessageType: enum {
  M_1,
  M_2,
  M_3,
  M_4

};

MIC: record
  ptk:	            PTK;		
  nonce:            Nonce;
  sequence:         Sequence;
  mtype:            MessageType;
end;

Message: record
  source:           AgentId;
  dest:             AgentId;
  mtype:            MessageType;
  nonce:            Nonce;
  sequence:         Sequence;
  address:          AgentId;
  mic:              MIC;
end;

--
-- Player modeling
--

-- Supplicant
SupplicantStates: enum {
  S_START,
  S_PTKSA,
  S_DONE
};

SSessions: record
  state:            SupplicantStates;
  ptk:              PTK;
end;


SAssociations: record
  session:          SSessions;
  sid:              SessionId;
  pmk:              PMK;
  peer:             AgentId;
  nonce:            Nonce;
  preanonce:          Nonce;
precomp:       boolean;
  sequence:         Sequence;
end;

Supplicant: record
  associations:     array[AgentId] of SAssociations;
end;


-- Authenticator
AuthenticatorStates: enum {
  A_PMKSA,
  A_WAITFORNS,
  A_PTKSA,
  A_DONE
};

ASessions: record
  state:            AuthenticatorStates;
  ptk:              PTK;
end;


AAssociations: record
  session:          ASessions;
  sid:              SessionId;
  pmk:              PMK;
  peer:             AgentId;
  nonce:            Nonce;
  sequence:         Sequence;
end;

Authenticator: record
  associations:     array[AgentId] of AAssociations;
end;


-- Intruder

Intruder: record
  -- We assume Intruder can impersonate both supplicant and authenticator except that no PMK in Intruder

  nonces:           multiset[MaxKnowledge] of Nonce; 
  mics:             multiset[MaxKnowledge] of MIC;
  messages:         multiset[MaxKnowledge] of Message;
end;

-- Other variables

var
  net:              multiset[NetworkSize] of Message;
  sup:              array[SupplicantId] of Supplicant;
  aut:              array[AuthenticatorId] of Authenticator;
  int:              array[IntruderId] of Intruder;

  nextNonce:        Nonce;
  nextSequence:     Sequence;

-- Generate a fresh nonce

function freshNonce(): Nonce;
var tmp: Nonce;
begin
   if (nextNonce = MaxNonce) then
      error "Run out of nonces!"
   end;
   tmp := nextNonce;
   nextNonce := nextNonce + 1;
   return tmp;
end;

-- Generate a fresh sequence

function freshSequence(): Sequence;
var tmp: Sequence;
begin
   if (nextSequence = MaxSequence) then
      error "Run out of sequences!"
   end;
   tmp := nextSequence;
   nextSequence := nextSequence + 1;
   return tmp;
end;

-- Use PMK for peers.

function usePMK(peer1: AgentId; peer2: AgentId) : PMK;
var tmp: PMK;
begin
        tmp.peer1 := peer1;
        tmp.peer2 := peer2;
        return tmp;
end;

-- Derive a PTK from PMK

function derivePTK(pmkey: PMK; nonce1: Nonce; nonce2: Nonce; address1: AgentId; address2: AgentId): PTK;
var tmp: PTK;
begin
        tmp.pmk       := pmkey;
        tmp.nonce1    := nonce1;
        tmp.nonce2    := nonce2;
        tmp.address1  := address1;
        tmp.address2  := address2;
        return tmp;
end;

-- Compute MIC

function computeMIC(ptk: PTK; nonce: Nonce; sequence: Sequence; mtype: MessageType): MIC;
var tmp: MIC;
begin
        tmp.ptk       := ptk;
        tmp.nonce     := nonce;
        tmp.sequence  := sequence;
        tmp.mtype     := mtype;
        return tmp;
end;

--
-- Comparison functions
--

function pmkEqual(key1: PMK; key2: PMK): boolean;
begin
   return ((key1.peer1  = key2.peer1) & (key1.peer2  = key2.peer2)) |
          ((key1.peer2  = key2.peer1) & (key1.peer1  = key2.peer2)) ;
end;

function ptkEqual(key1: PTK; key2: PTK): boolean;
begin
   return pmkEqual(key1.pmk, key2.pmk) &
          (!NONCE_ENABLED | (key1.nonce1 = key2.nonce1 & key1.nonce2 = key2.nonce2) | (key1.nonce1 = key2.nonce2 & key1.nonce2 = key2.nonce1))  &
          (!ADDRESS_ENABLED | (key1.address1 = key2.address1 & key1.address2 = key2.address2) | (key1.address1 = key2.address2 & key1.address2 = key2.address1)) ;
end;

function micEqual(mic1: MIC; mic2: MIC): boolean;
begin
   return ptkEqual(mic1.ptk, mic2.ptk)    &
          (!NONCE_ENABLED | mic1.mtype = M_4 | mic1.nonce    = mic2.nonce)    &
          (!SEQUENCE_ENABLED | mic1.sequence = mic2.sequence) &
          (!MTYPE_ENABLED | mic1.mtype    = mic2.mtype) ;
end;

-----------
-- Rules --
-----------

--
-- Authenticator
--

-- Authenticator sends message 1

ruleset i: AuthenticatorId do
  ruleset j: AgentId do
    rule 20 "Authenticator sends Message 1 to associated agents"

      -- j != i & --no message to itself
      !ismember(j, AuthenticatorId) &  -- no message to Authenticators
      !ismember(j, IntruderId) &  -- no message to Intruders
      aut[i].associations[j].sid < MaxSessions &
      multisetcount(l:net, true) < NetworkSize &
      (aut[i].associations[j].session.state = A_PMKSA | aut[i].associations[j].session.state = A_DONE)


      ==>


      var
        outM: Message;       -- outgoing message

      begin
        undefine outM;
        outM.source       :=      i;
        outM.dest         :=      j;
        outM.mtype        :=      M_1;
        outM.nonce        :=      freshNonce();
        outM.sequence     :=      freshSequence();
        outM.address      :=      i;
        -- outM.mic          :=      computeMIC();


        multisetadd(outM, net);


        -- store the states
        aut[i].associations[j].peer               :=     j;
        aut[i].associations[j].pmk                :=     usePMK(i, j);
        aut[i].associations[j].sequence           :=     outM.sequence;
        aut[i].associations[j].nonce              :=     outM.nonce;
        aut[i].associations[j].session.state      :=     A_WAITFORNS;
        undefine aut[i].associations[j].session.ptk;
      end;

  end;
end;


-- For a Supplicant.
-- Receive message 1. Send message 2.
--

ruleset i: SupplicantId do
  choose j: net do
    rule 20 "Supplicant processes message 1"

       net[j].dest = i &
       net[j].mtype = M_1 & 
       sup[i].associations[net[j].address].sid < MaxSessions &
(isundefined(sup[i].associations[net[j].address].preanonce) | !(sup[i].associations[net[j].address].preanonce = net[j].nonce & net[j].mtype = M_1))
       -- (sup[i].associations[net[j].address].session.state = S_START | sup[i].associations[net[j].address].session.state = S_DONE)

       ==>

       var
          outM: Message;       -- outgoing message
          inM:  Message;

       begin
          inM   := net[j];
          
          -- Remove processed message
          multisetremove (j, net);

          if (sup[i].associations[inM.address].sequence <= inM.sequence) then
             -- Derive PTK.
             sup[i].associations[inM.address].peer       := inM.source;
             sup[i].associations[inM.address].pmk        := usePMK(i, inM.address);
             -- sup[i].associations[inM.address].sequence
             sup[i].associations[inM.address].nonce      := freshNonce();
sup[i].associations[inM.address].preanonce      := inM.nonce;
             sup[i].associations[inM.address].session.ptk := derivePTK(
                                                          sup[i].associations[inM.address].pmk,
                                                          sup[i].associations[inM.address].nonce,
                                                          inM.nonce,
                                                          i,
                                                          inM.address);


             -- Send message M_2.
             undefine outM;
   
             outM.source       := i;
             outM.dest         := inM.address;
             outM.mtype        := M_2;
             outM.nonce        := sup[i].associations[inM.address].nonce;
             outM.sequence     := inM.sequence;
             outM.address      := i;
             outM.mic          := computeMIC(
                               sup[i].associations[inM.address].session.ptk,
                               outM.nonce,
                               outM.sequence,
                               outM.mtype);


             multisetadd(outM, net);

             -- Change state to S_PTKSA.
             sup[i].associations[inM.address].session.state := S_PTKSA;

          end;
         
       end;

  endchoose;
end;



-- For Authenticator.
-- Receive message 2. Send message 3.


ruleset i: AuthenticatorId do
  choose j: net do
    rule 20 "Authenticator processes message 2"

       net[j].dest = i &
       net[j].mtype = M_2 & 
       aut[i].associations[net[j].address].session.state = A_WAITFORNS

       ==>

       var
          outM: Message;       -- outgoing message
          inM:  Message; 
          ptk:  PTK;
          mic:  MIC;

        begin
	  inM := net[j];

          -- Remove processed message
          multisetremove(j, net);

        
             -- Check correctness of message

             if (inM.sequence = aut[i].associations[inM.address].sequence) then
               -- Derive PTK.
               ptk := derivePTK(aut[i].associations[inM.address].pmk,
                                inM.nonce,
                                aut[i].associations[inM.address].nonce,
                                inM.address,
                                i);
               mic := computeMIC(
                                 ptk,
                                 inM.nonce,
                                 inM.sequence,
                                 inM.mtype);
               if (micEqual(mic, inM.mic)) then

                  -- Send message M_3
                  undefine outM;
                  outM.source       := i;
                  outM.dest         := inM.address;
                  outM.mtype        := M_3;
                  outM.nonce        := aut[i].associations[inM.address].nonce;
                  outM.sequence     := freshSequence();
                  outM.address      := i;
                  outM.mic          := computeMIC(
                                       ptk,
                                       outM.nonce,
                                       outM.sequence,
                                       outM.mtype);


                  multisetadd(outM, net);

                  -- update states.
                  aut[i].associations[inM.address].sequence      := outM.sequence;
                  aut[i].associations[inM.address].peer          := inM.source;

                  aut[i].associations[inM.address].session.ptk   := ptk;
                  aut[i].associations[inM.address].session.state := A_PTKSA;

                end;
              end;

        
        end;

  endchoose;
end;


-- For Supplicant.
-- Receive message 3. Send message 4.
--

ruleset i: SupplicantId do
  choose j: net do
    rule 20 "supplicant processes message 3"

       net[j].dest = i &
       net[j].mtype = M_3 &
       sup[i].associations[net[j].address].sid < MaxSessions
       -- sup[i].associations[net[j].address].session.state = S_PTKSA

       ==>

       var
          outM: Message;       -- outgoing message
          inM:  Message;
          mic:  MIC;

       begin
          inM := net[j];

          -- Remove processed message
          multisetremove (j, net);

      

               -- Check correctness of message

               if (sup[i].associations[inM.address].sequence < inM.sequence) then

                 mic := computeMIC(
                        sup[i].associations[inM.address].session.ptk,
                        inM.nonce,
                        inM.sequence,
                        inM.mtype);
                 if (micEqual(mic, inM.mic)) then
                   -- Send message M_4.
                   undefine outM;

                   outM.source       := i;
                   outM.dest         := inM.address;
                   outM.mtype        := M_4;
                   outM.nonce        := sup[i].associations[inM.address].nonce;
                   outM.sequence     := inM.sequence;
                   outM.address      := i;
                   outM.mic          := computeMIC(
                                        sup[i].associations[inM.address].session.ptk,
                                        outM.nonce,
                                        outM.sequence,
                                        outM.mtype);


                   multisetadd(outM, net);

                   -- Update states.
                   sup[i].associations[inM.address].peer       := inM.source;
                   sup[i].associations[inM.address].sequence   := inM.sequence;

                   sup[i].associations[inM.address].session.state := S_DONE;
                   sup[i].associations[inM.address].sid :=  sup[i].associations[inM.address].sid + 1;

                 end;
               end;


     
       end;

  endchoose;
end;

-- For Authenticator.
-- Receive message 4.

ruleset i: AuthenticatorId do
  choose j: net do
    rule 20 "Authenticator processes message 4"

       net[j].dest = i &
       net[j].mtype = M_4  & 
       aut[i].associations[net[j].address].sid < MaxSessions &
       aut[i].associations[net[j].address].session.state = A_PTKSA 

       ==>

       var
         inM: Message;
         mic:  MIC;

       begin
	 inM := net[j];
              -- Remove processed message
              multisetremove (j, net);

                -- Check correctness of message

                if (inM.sequence = aut[i].associations[inM.address].sequence) then

                  mic := computeMIC(
                         aut[i].associations[inM.address].session.ptk,
                         inM.nonce,
                         inM.sequence,
                         inM.mtype);
                  if (micEqual(mic, inM.mic)) then

                    -- update states.
                    aut[i].associations[inM.address].peer          := inM.source;  
                    aut[i].associations[inM.address].session.state := A_DONE;
                    aut[i].associations[inM.address].sid       := aut[i].associations[inM.address].sid + 1;
                  end;
                end;

        
       end;

  endchoose;
end;


-- Intruder

-- Intercept a message

ruleset i: IntruderId do
  choose j: net do
    rule 10 "Intruders intercept a message"

       multisetcount(l:net, true) > 0 &
       !ismember(net[j].source, IntruderId) -- not intercept messages from Intruders

       ==>

       var
         inM: Message;

       begin
         alias msg: int[i].messages;
               nc:  int[i].nonces;
               mc:  int[i].mics;  do
      
           inM := net[j];

           -- Remove processed message.
           multisetremove (j, net);

           -- store the whole message for replay
           if (multisetcount(l:msg,
                             msg[l].mtype = inM.mtype &
                             (msg[l].mtype = M_4 | msg[l].nonce = inM.nonce) &
                             msg[l].sequence = inM.sequence &
                             msg[l].address = inM.address &
                             (msg[l].mtype = M_1 | micEqual(msg[l].mic, inM.mic))) = 0) then

               undefine inM.source;
               undefine inM.dest;
               multisetadd(inM, int[i].messages);
           end;

           -- store nonces
           if (multisetcount(n:nc, inM.mtype != M_4 & nc[n] = inM.nonce) = 0) then
	      multisetadd(inM.nonce, int[i].nonces);
           end;
    
           -- store mics
           if (multisetcount(m:mc, inM.mtype != M_1 & micEqual(mc[m], inM.mic)) = 0) then
	      multisetadd(inM.mic, int[i].mics);
	   end;


         endalias;
       end;
endchoose;
end;


-- Replay a complete message

ruleset i: IntruderId do
  choose j: int[i].messages do
    ruleset k: AgentId do
      rule 30 "Messages Replayed to every agent"

      i != k &
      multisetcount(l:net, true) < NetworkSize 

      ==>

      var
        outM: Message;  -- outgoing message

      begin
        undefine outM;
        outM              := int[i].messages[j];
        outM.source       := i;
        outM.dest         := k;

        multisetadd (outM, net);
        -- multisetremove (j, int[i].messages); 

      end;
      
    end;

  endchoose;
end;

/*
-- Intruder compose message 1 from known nonces and send to agents

ruleset i: IntruderId do
  ruleset j: SupplicantId do
    ruleset k: AuthenticatorId do
    choose n: int[i].nonces do

      rule 30 "Intruders compose message 1 and send to agents"

      -- i != j &
      -- j != k &
      -- i != k &
      multisetcount(l:net, true) < NetworkSize 


      ==>


      var
        outM: Message;       -- outgoing message

      begin
        undefine outM;

        outM.source       :=      i;
        outM.dest         :=      j;
        outM.mtype        :=      M_1;
        outM.nonce        :=      int[i].nonces[n];
        outM.sequence     :=      nextSequence; 
        outM.address      :=      k;
        -- outM.mic          :=      computeMIC();


        multisetadd(outM, net);


        -- store the states
        -- aut[i].associations[j].peer               :=     j;
        -- aut[i].associations[j].pmk                :=     usePMK(i, j);
        -- aut[i].associations[j].sequence           :=     outM.sequence;
        -- aut[i].associations[j].nonce              :=     outM.nonce;
        -- aut[i].associations[j].session.state      :=     A_WAITFORNS;
        -- aut[i].associations[j].session.ptk

      end;
endchoose;
    end;
  end;
end;

*/

-- Intruder compose message 1 for some specific nonces

ruleset i: IntruderId do
  ruleset j: SupplicantId do
    ruleset k: AuthenticatorId do
    --choose n: int[i].nonces do

      rule 10 "Intruders compose message 1 and send to agents"

      -- i != j &
      -- j != k &
      -- i != k &
      sup[j].associations[k].precomp = true &
      multisetcount(l:net, true) < NetworkSize 


      ==>


      var
        outM: Message;       -- outgoing message

      begin
        undefine outM;

        outM.source       :=      i;
        outM.dest         :=      j;
        outM.mtype        :=      M_1;
        outM.nonce        :=      2;
        outM.sequence     :=      nextSequence; 
        outM.address      :=      k;
        -- outM.mic          :=      computeMIC();


        multisetadd(outM, net);

sup[j].associations[k].precomp := false;
        -- store the states
        -- aut[i].associations[j].peer               :=     j;
        -- aut[i].associations[j].pmk                :=     usePMK(i, j);
        -- aut[i].associations[j].sequence           :=     outM.sequence;
        -- aut[i].associations[j].nonce              :=     outM.nonce;
        -- aut[i].associations[j].session.state      :=     A_WAITFORNS;
        -- aut[i].associations[j].session.ptk

      end;
--endchoose;
    end;
  end;
end;


-- Intruder response with forged messages

ruleset i: IntruderId do
  choose j: net do
    choose n: int[i].nonces do
    choose m: int[i].mics do
    rule 30 "Intruder response with forged messages"

       multisetcount(l:net, true) > 0 &
       !ismember(net[j].source, IntruderId) &
       net[j].mtype != M_4

       ==>

       var
          outM: Message;       -- outgoing message
          inM:  Message;

       begin
          inM   := net[j];
          
          -- Remove processed message
          multisetremove (j, net);
	       undefine outM;

	 
          switch inM.mtype

	       case M_1:
	       outM.mtype := M_2;
               outM.sequence := inM.sequence;
	       case M_2:
	       outM.mtype := M_3;
	       outM.sequence := inM.sequence + 1;
	       case M_3:
	       outM.mtype := M_4;
	       outM.sequence := inM.sequence;

	       case M_4:

	  endswitch;

          outM.source       := i;
             outM.dest         := inM.source;
             outM.nonce        := int[i].nonces[n];
            
             outM.address      := inM.dest;
             outM.mic          := int[i].mics[m];


             multisetadd(outM, net);

        end;  
       endchoose;
      endchoose;
endchoose;
end;




--
-- Start state
--

startstate

var

begin


  -- Initialize variables
       nextNonce              := 0;
       nextSequence           := 0;

  -- Initialize network
     undefine net;

  -- Initialize supplicants
     undefine sup;
     for i:SupplicantId do
         for j:AgentId do
           -- undefine sup[i].associations[j];

           sup[i].associations[j].session.state  := S_START;
           -- sup[i].associations[j].session.ptk :=
           sup[i].associations[j].sid        := 0;
           sup[i].associations[j].pmk            := usePMK(i, j);
           sup[i].associations[j].peer           := j;
           sup[i].associations[j].sequence       := 0;
           -- sup[i].associations[j].nonce          := freshNonce();
sup[i].associations[j].precomp := true;
         end;
     end;

  -- Initalize Authenticators
     undefine aut;
     for i:AuthenticatorId do
         for j:AgentId do
           -- undefine aut[i].associations[j];
           aut[i].associations[j].session.state  := A_PMKSA;
           -- aut[i].associations[j].session.ptk :=
           aut[i].associations[j].sid        := 0;
           aut[i].associations[j].pmk            := usePMK(i, j);
           aut[i].associations[j].peer           := j;
           aut[i].associations[j].sequence       := 0;
           -- aut[i].associations[j].nonce          := freshNonce();
         end;
      end;

  -- Initialize intruders
     undefine int;
     for i:IntruderId do
       undefine int[i].messages;
     end;

end;

--
-- invariants
--

/*
invariant "authenticator knows the supplicant is live due to valid msg2"
  forall i: AuthenticatorId do
    forall j: SupplicantId do
 
      aut[i].associations[j].session.state = A_PTKSA 
      
      ->

      ptkEqual(aut[i].associations[j].session.ptk, sup[j].associations[i].session.ptk)
  
     end
  end;


--
invariant "supplicant knows authenticator is live due to valid msg3"
  forall i: SupplicantId do
    forall j: AuthenticatorId do
 
      sup[i].associations[j].session.state = S_DONE 
      
      ->

      -- (aut[j].associations[i].session.state = A_PTKSA |
      -- aut[j].associations[i].session.state = A_DONE) &
      ptkEqual(aut[j].associations[i].session.ptk, sup[i].associations[j].session.ptk)
  
     end
  end;
*/


--
invariant "The shared PTKs are consistent and fresh"

  forall i: AuthenticatorId do
    forall j: SupplicantId do
 
     
      aut[i].associations[j].session.state = A_DONE

      ->

      (sup[j].associations[i].session.state = S_DONE &
      ptkEqual(aut[i].associations[j].session.ptk, sup[j].associations[i].session.ptk) &
      aut[i].associations[j].sid = sup[j].associations[i].sid) 
      -- (sup[j].associations[i].session.state = S_PTKSA & aut[i].associations[j].sid <= sup[j].associations[i].sid)  
      -- aut[i].associations[j].sid <= sup[j].associations[i].sid

     end
  end;

/*
--
invariant "The shared key are achieved"

  forall i: AuthenticatorId do
    forall j: SupplicantId do
 
     
      !aut[i].associations[j].session.state = A_DONE & !sup[j].associations[i].session.state = S_DONE 

     end
  end;



--
invariant "The protocol can finish under attacking"

  forall i: AuthenticatorId do
    forall j: SupplicantId do

      !(aut[i].associations[j].session.state = A_DONE &
      sup[j].associations[i].session.state = S_DONE &
      aut[i].associations[j].sid = sup[j].associations[i].sid &
	ptkEqual(aut[i].associations[j].session.ptk, sup[j].associations[i].session.ptk))

    end
  end
*/
