--
--

-- IEEE 802.16e 3-way TEK Handshake Protocol

-- Vijay Chauhan & Srinivas Inguva
--

--
-- Parameters
--

const

  BS_SEND_M1:            6;
  MS_RECV_M1:            5;
  MS_SEND_M2:            6;
  BS_RECV_M2:            5;
  BS_SEND_M3:            8;
  MS_RECV_M3:            8;

  INT_INTERCEPT:         4; 
  INT_COMPOSE:           4;
  INT_SEND:              4;

  MS_WAIT_RES_COST:      11;
  INT_RES_THRESHOLD:     8;

  INT_THRESHOLD:         16;
  MS_DONE_COST:          19;
  BS_DONE_COST:          19;


  
  DOS_ENABLED:           true;
  PN_ENABLED:            true;
--PN_ENABLED:            false;
  -- If PN_ENABLED is set to "false", we expect an invariant violation
  -- representing a DoS


  NumMS:                   1;
  NumBS:                   1;
  NumIntruders:            1;

  NetworkSize:             10;


  MaxSessions:             1;
  MaxIntruderActions:      5;

  MaxIntruderCosts:        200;
  MaxCost:                 200;

  MaxNonce:                30;

  MaxPN:                   100;


  -- What intruder can remember
 
  MaxKnowledge:            10;    


type
  MSId:          scalarset(NumMS);
  BSId:          scalarset(NumBS);
  IntruderId:    scalarset(NumIntruders);
  AgentId:       union{MSId, BSId, IntruderId};


  Nonce:           0..MaxNonce;
  PN:              -1..MaxPN;
  SessionId:       0..MaxSessions;


-- Key modeling

AK: record
  peer1:           AgentId;   --MS
  peer2:           AgentId;   --BS
end;


--
-- Message Modeling
--

MessageType: enum {
  M_1,
  M_2,
  M_3

};

MAC: record
  ak:	            AK;		
  MSnonce:          Nonce;
  BSnonce:          Nonce;
  TEKnonce:         Nonce;
  mtype:            MessageType;
end;

Message: record
  source:           AgentId;
  dest:             AgentId;
  mtype:            MessageType;
  BSnonce:          Nonce;
  MSnonce:          Nonce;
  TEKnonce:         Nonce;
  address:          AgentId; 
  pn:               PN;
  mac:              MAC;
end;

-- MS
MSStates: enum {
  MS_WAIT_CLG,
  MS_WAIT_RES,
  MS_DONE
};

MSSessions: record
  state:            MSStates;
  ak:               AK;
  costs:            0..MaxCost;
  intCosts:         0..MaxIntruderCosts;
end;


MSAssociations: record
  session:          MSSessions;
  sid:              SessionId;
  peer:             AgentId;
  MSnonce:          Nonce;
  BSnonce:          Nonce;
  TEKnonce:         Nonce;
lastKnownPN:        PN;
end;

MS: record
  associations:     array[AgentId] of MSAssociations;
end;

-- BS
BSStates: enum {
  BS_START,
  BS_WAIT_REQ,
  BS_DONE
};
 
BSSessions: record
  state:            BSStates;
  ak:               AK;
  costs:            0..MaxCost;
  intCosts:         0..MaxIntruderCosts;
end;


BSAssociations: record
  session:          BSSessions;
  sid:              SessionId;
  peer:             AgentId;
  BSnonce:          Nonce;
  MSnonce:          Nonce;
  TEKnonce:         Nonce;
end;

BS: record
  associations:     array[AgentId] of BSAssociations;
end;

-- Intruder

Intruder: record

  nonces:           multiset[MaxKnowledge] of Nonce; 
  TEKnonces:        multiset[MaxKnowledge] of Nonce; 
  macs:             multiset[MaxKnowledge] of MAC;
  messages:         multiset[MaxKnowledge] of Message;

end;

-- Other variables

var
  net:              multiset[NetworkSize] of Message;
  ms:               array[MSId] of MS;
  bs:               array[BSId] of BS;
  int:              array[IntruderId] of Intruder;
  actionCount:      0..MaxIntruderActions;       

  nextNonce:        Nonce;
  nextPN:           PN;

-- 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 PN

function freshPN(): PN;
var tmp: PN;
begin
   if (nextPN = MaxPN) then
      error "Run out of PNs!"
   end;
   tmp := nextPN;
   nextPN := nextPN + 1;
   return tmp;
end;

-- Use AK for peers.

function useAK(peer1: AgentId; peer2: AgentId) : AK;
var tmp: AK;
begin
        tmp.peer1 := peer1;
        tmp.peer2 := peer2;
        return tmp;
end;

-- Compute MAC

function computeMAC(msg: Message; ak: AK) : MAC;
var tmp: MAC;
begin
        tmp.ak          := ak;
        tmp.BSnonce     := msg.BSnonce;
        
        if (msg.mtype = M_2 | msg.mtype = M_3) then
          tmp.MSnonce     := msg.MSnonce; 
        end;
        
        if (msg.mtype = M_3) then
          tmp.TEKnonce     := msg.TEKnonce; 
        end;
        
        tmp.mtype       := msg.mtype;
        return tmp;
end;

--
-- Comparison functions
--

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

function macEqual(mac1: MAC; mac2: MAC): boolean;
begin
  if (!akEqual(mac1.ak, mac2.ak)) then 
    return false;
  end;

  if (!(mac1.mtype = mac2.mtype)) then 
    return false;
  end;
 
  if (!(mac1.BSnonce = mac2.BSnonce)) then
    return false;
  end;

  if ((mac1.mtype = M_2 | mac1.mtype = M_3) & !(mac1.MSnonce = mac2.MSnonce)) then
    return false;
  end; 

  if ((mac1.mtype = M_3) & !(mac1.TEKnonce = mac2.TEKnonce)) then
    return false;
  end; 

  return true;

end;


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

--
-- BS
--

-- BS sends message 1

ruleset i: BSId do
  ruleset j: AgentId do
    rule 20 "BS sends Message 1 to associated agents"

      !ismember(j, BSId) &  -- no message to BSs
      !ismember(j, IntruderId) &  -- no message to Intruders
      bs[i].associations[j].sid < MaxSessions &
      multisetcount(l:net, true) < NetworkSize &
      (bs[i].associations[j].session.state = BS_START | bs[i].associations[j].session.state = BS_DONE)
      --(bs[i].associations[j].session.state = BS_START)

      ==>


      var
        outM: Message;       -- outgoing message
        outAK: AK;

      begin
        undefine outM;
        outM.source       :=      i;
        outM.dest         :=      j;
        outM.mtype        :=      M_1;
        outM.BSnonce      :=      freshNonce();
        outM.address      :=      i;
        outM.pn           :=      freshPN();
 
        outAK := useAK(i, j);
         
        outM.mac          :=      computeMAC(outM, outAK);

        multisetadd(outM, net);

        -- store the states
        bs[i].associations[j].peer               :=     j;
        bs[i].associations[j].session.ak         :=     useAK(i, j);
        bs[i].associations[j].BSnonce            :=     outM.BSnonce;
        bs[i].associations[j].session.state      :=     BS_WAIT_REQ;

        bs[i].associations[j].sid :=  bs[i].associations[j].sid + 1; 
        bs[i].associations[j].session.costs      :=     BS_SEND_M1;      

      end;

  end;
end;


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

ruleset i: MSId do
  choose j: net do
    rule 20 "MS processes message 1"

       net[j].dest = i &
       net[j].mtype = M_1 & 
       ms[i].associations[net[j].address].sid < MaxSessions &
       -- (ms[i].associations[net[j].address].session.state = MS_WAIT_CLG | ms[i].associations[net[j].address].session.state = MS_DONE)
       (ms[i].associations[net[j].address].session.state = MS_WAIT_CLG)

       ==>


       var
          outM: Message;       -- outgoing message
          inM:  Message;
          mac: MAC;
          outAK: AK;

       begin
          inM   := net[j];
          
          -- Remove processed message
          multisetremove (j, net);
  
          outAK := useAK(i, inM.address);
          mac := computeMAC(inM, outAK);
                              
          --MAC CHECK
          if (macEqual(mac, inM.mac) & (!PN_ENABLED | (inM.pn > ms[i].associations[inM.address].lastKnownPN))) then

             -- Store MSNonce
             ms[i].associations[inM.address].peer       := inM.source;
             ms[i].associations[inM.address].session.ak := useAK(i, inM.address);
             ms[i].associations[inM.address].BSnonce      := inM.BSnonce;
             ms[i].associations[inM.address].MSnonce      := freshNonce();


             -- Send message M_2
             undefine outM;
   
             outM.source       := i;
             outM.dest         := inM.address;
             outM.mtype        := M_2;
             outM.BSnonce      := ms[i].associations[inM.address].BSnonce;
             outM.MSnonce      := ms[i].associations[inM.address].MSnonce;
             outM.address      := i;
             outM.mac          := computeMAC(outM, outAK);

             multisetadd(outM, net);

             -- Change state to MS_WAIT_RES
             ms[i].associations[inM.address].session.state := MS_WAIT_RES;

             if (!DOS_ENABLED) then 
               ms[i].associations[inM.address].sid :=  ms[i].associations[inM.address].sid + 1;
             end;

             ms[i].associations[inM.address].session.costs := ms[i].associations[inM.address].session.costs + MS_RECV_M1 + MS_SEND_M2;

             if (!PN_ENABLED) then 
               ms[i].associations[inM.address].lastKnownPN := inM.pn;
             end;
 
          end;
       end;

  endchoose;
end;

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


ruleset i: BSId do
  choose j: net do
    rule 20 "BS processes message 2"

       net[j].dest = i &
       net[j].mtype = M_2 &
       -- Allow the BS to accept rekey messages
       (DOS_ENABLED | bs[i].associations[net[j].address].session.state = BS_WAIT_REQ)

       ==>

       var
          outM: Message;       -- outgoing message
          inM:  Message; 
          mac:  MAC;
          outAK: AK;

        begin
	  inM := net[j];

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

          outAK := useAK(i, inM.address);
          mac := computeMAC(inM, outAK);
                              
          --MAC CHECK
          if (macEqual(mac, inM.mac)) then

                  -- Send message M_3
                  undefine outM;
                  outM.source       := i;
                  outM.dest         := inM.address;
                  outM.mtype        := M_3;

                  outM.BSnonce      := inM.BSnonce;
                  outM.MSnonce      := inM.MSnonce;
                  outM.TEKnonce     := freshNonce();

                  outM.address      := i;
                  outM.mac          := computeMAC(outM,outAK);


                  multisetadd(outM, net);

                  -- update states.
                  bs[i].associations[inM.address].peer          := inM.source;
                  bs[i].associations[inM.address].MSnonce       := inM.MSnonce;
                  bs[i].associations[inM.address].TEKnonce      := outM.TEKnonce;

                  bs[i].associations[inM.address].session.state := BS_DONE;

                  --bs[i].associations[inM.address].sid :=  bs[i].associations[inM.address].sid + 1; 

                  if (!DOS_ENABLED) then
                    bs[i].associations[inM.address].session.costs := bs[i].associations[inM.address].session.costs + BS_RECV_M2 + BS_SEND_M3; 
                  end;

          end;
           --MAC CHECK end;

        
        end;

  endchoose;
end;

-- For MS
-- Receive message 3, done..
--

ruleset i: MSId do
  choose j: net do
    rule 20 "MS processes message 3"

       net[j].dest = i &
       net[j].mtype = M_3 &
       ms[i].associations[net[j].address].sid < MaxSessions &
       ms[i].associations[net[j].address].session.state = MS_WAIT_RES

       ==>

       var
          inM:  Message;
          mac:  MAC;
          outAK: AK;

       begin
          inM := net[j];

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

          outAK := useAK(i, inM.address);
          mac := computeMAC(inM, outAK);
                              
          --MAC CHECK
          if (macEqual(mac, inM.mac)) then

      
                   -- Update states.
                   ms[i].associations[inM.address].peer       := inM.source;
                   ms[i].associations[inM.address].TEKnonce   := inM.TEKnonce;                   

                   ms[i].associations[inM.address].session.state := MS_DONE;

                  ms[i].associations[inM.address].session.costs := ms[i].associations[inM.address].session.costs + MS_RECV_M3;

          end;
          --MAC CHECK end;


     
       end;

  endchoose;
end;

--

ruleset i: MSId do
  ruleset j: AgentId do
    rule 291 "MS transitions from MS_DONE->MS_WAIT_CLG"

    ms[i].associations[j].session.state = MS_DONE

    ==>
  
    begin

       ms[i].associations[j].session.state := MS_WAIT_CLG;
       if (!DOS_ENABLED) then
         ms[i].associations[j].session.costs := 0;
         ms[i].associations[j].session.intCosts := 0;
       end;
       
    end;
  
  end;
end;

/*
ruleset i: BSId do
  ruleset j: AgentId do
    rule 291 "BS transitions from BS_DONE->BS_START"

    bs[i].associations[j].session.state = BS_DONE

    ==>
  
    begin

       bs[i].associations[j].session.state := BS_START;
       bs[i].associations[j].session.costs := 0;
    end;
  
  end;
end;
*/ 

    


-- Intruder

-- Intercept a message

ruleset i: IntruderId do
  choose j: net do
    rule 10 "Intruders intercept a message"
       
       actionCount < MaxIntruderActions &
       multisetcount(l:net, true) > 0 &
       !ismember(net[j].source, IntruderId) -- do not intercept messages from Intruders

       ==>

       var
         inM: Message;

       begin
         alias msg: int[i].messages;
               nc:  int[i].nonces;
               teknc: int[i].TEKnonces;
               mc:  int[i].macs; 
 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].BSnonce = inM.BSnonce) &
                             (msg[l].mtype = M_1 | msg[l].MSnonce = inM.MSnonce) &
                             (msg[l].mtype = M_1 | msg[l].mtype = M_2 | msg[l].TEKnonce = inM.TEKnonce) &
                             (msg[l].address = inM.address)  &
                             (macEqual(msg[l].mac, inM.mac))) = 0) then
                            

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

           -- store BSnonces
           if (multisetcount(n:nc, nc[n] = inM.BSnonce) = 0) then
	      multisetadd(inM.BSnonce, int[i].nonces);
           end;
    
           -- store MSnonces
           if (multisetcount(n:nc, (inM.mtype = M_1 | nc[n] = inM.MSnonce)) = 0) then
	      multisetadd(inM.MSnonce, int[i].nonces);
           end;
 
--            put "#####################DEBUG 1\n";                       
--            put inM.mtype;                       

           -- store TEKnonces
           if (multisetcount(n:teknc, (inM.mtype = M_1 | inM.mtype = M_2 | teknc[n] = inM.TEKnonce)) = 0) then
	      if (inM.mtype = M_3) then   
                 multisetadd(inM.TEKnonce, int[i].TEKnonces);
              end;
           end;

--          put "#####################DEBUG 2\n";

           -- store macs
           if (multisetcount(m:mc, macEqual(mc[m], inM.mac)) = 0) then
	      multisetadd(inM.mac, int[i].macs);
	   end;

--          put "#####################DEBUG 3\n";

            actionCount:= actionCount+1;

         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"

      actionCount < MaxIntruderActions & 
      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); 

         actionCount:= actionCount+1;
 
       if (isMember(k, MSId) & isMember(outM.address, BSId)) then
          ms[k].associations[outM.address].session.intCosts :=ms[k].associations[outM.address].session.intCosts + INT_INTERCEPT + INT_SEND;
       end;

      end;
      
    end;

  endchoose;
end;


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

ruleset i: IntruderId do
  ruleset j: MSId do
    ruleset k: BSId do
    choose n: int[i].nonces do
    choose m: int[i].macs do

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

      actionCount < MaxIntruderActions & 
      multisetcount(l:net, true) < NetworkSize 


      ==>


      var
        outM: Message;       -- outgoing message

      begin
        undefine outM;

        outM.source       :=      i;
        outM.dest         :=      j;
        outM.mtype        :=      M_1;
        outM.BSnonce      :=      int[i].nonces[n];
        outM.address      :=      k;
        outM.mac          :=      int[i].macs[m];
        outM.pn           :=      -1;


        multisetadd(outM, net);

        actionCount:= actionCount+1;

        ms[j].associations[k].session.intCosts := ms[j].associations[k].session.intCosts + INT_INTERCEPT + INT_COMPOSE;



      end;
endchoose;
endchoose;
    end;
  end;
end;


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

ruleset i: IntruderId do
  ruleset j: MSId do
    ruleset k: BSId do
    choose n: int[i].nonces do
    choose p: int[i].nonces do
    choose m: int[i].macs do

      rule 31 "Intruders compose message 2 and send to agents"

      actionCount < MaxIntruderActions & 
      multisetcount(l:net, true) < NetworkSize 


      ==>


      var
        outM: Message;       -- outgoing message

      begin
        undefine outM;

        outM.source       :=      i;
        outM.dest         :=      k;
        outM.mtype        :=      M_2;
        outM.BSnonce      :=      int[i].nonces[n];
        outM.MSnonce      :=      int[i].nonces[p];
        outM.address      :=      j;
        outM.mac          :=      int[i].macs[m];


        multisetadd(outM, net);

        actionCount:= actionCount+1;

      end;
endchoose;
endchoose;
endchoose;
    end;
  end;
end;




-- Intruder compose message 3 from known nonces and send to agents

ruleset i: IntruderId do
  ruleset j: MSId do
    ruleset k: BSId do
    choose n: int[i].nonces do
    choose p: int[i].nonces do
    choose q: int[i].TEKnonces do
    choose m: int[i].macs do

      rule 31 "Intruders compose message 2 and send to agents"

      actionCount < MaxIntruderActions & 
      multisetcount(l:net, true) < NetworkSize 


      ==>


      var
        outM: Message;       -- outgoing message

      begin
        undefine outM;

        outM.source       :=      i;
        outM.dest         :=      j;
        outM.mtype        :=      M_2;
        outM.BSnonce      :=      int[i].nonces[n];
        outM.MSnonce      :=      int[i].nonces[p];
        outM.TEKnonce     :=      int[i].TEKnonces[q];
        outM.address      :=      k;
        outM.mac          :=      int[i].macs[m];


        multisetadd(outM, net);

        actionCount:= actionCount+1;

      end;
endchoose;
endchoose;
endchoose;
endchoose;
    end;
  end;
end;

*/

--
-- Start state
--

startstate

var

begin


  -- Initialize variables
       nextNonce              := 0;
       nextPN                 := 0;
       actionCount            := 0; 

  -- Initialize network
     undefine net;

  -- Initialize MSs
     undefine ms;
     for i:MSId do
         for j:AgentId do
           ms[i].associations[j].session.state  := MS_WAIT_CLG;
           ms[i].associations[j].sid        := 0;
           ms[i].associations[j].session.ak            := useAK(i, j);
           ms[i].associations[j].peer           := j;
           ms[i].associations[j].session.costs := 0;
           ms[i].associations[j].session.intCosts := 0;
           ms[i].associations[j].lastKnownPN := 0;
         end;
     end;

  -- Initalize BS
     undefine bs;
     for i:BSId do
         for j:AgentId do
           bs[i].associations[j].session.state  := BS_START;
           bs[i].associations[j].sid        := 0;
           bs[i].associations[j].session.ak            := useAK(i, j);
           bs[i].associations[j].peer           := j;
           bs[i].associations[j].session.costs := 0;
         end;
      end;

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

end;


--
-- If MS is done, so is BS
invariant "If MS is DONE => BS is DONE" 

  forall i: BSId do
    forall j: MSId do

   (ms[j].associations[i].session.state = MS_DONE &
   (ms[j].associations[i].sid = bs[i].associations[j].sid))

   ->

   (bs[i].associations[j].session.state = BS_DONE)

     end
  end;

--

-- If MS is waiting for CLG, BS can't have finished the handshake
invariant "If MS is WAIT_CLG => BS is in START/WAIT_REQ" 

  forall i: BSId do
    forall j: MSId do

   (ms[j].associations[i].session.state = MS_WAIT_CLG &
   (ms[j].associations[i].sid = bs[i].associations[j].sid))

   ->

   (!bs[i].associations[j].session.state = BS_DONE)

     end
  end;

--

-- If MS is waiting for RES then BS must have sent a CLG
invariant "If MS is WAIT_RES => BS is in WAIT_REQ/DONE" 

  forall i: BSId do
    forall j: MSId do

   (ms[j].associations[i].session.state = MS_WAIT_RES &
   (ms[j].associations[i].sid = bs[i].associations[j].sid))

   ->

   (!bs[i].associations[j].session.state = BS_START)

     end
  end;

--

invariant "When MS/BS complete handshake they share a TEK"

  forall i: BSId do
    forall j: MSId do

   (ms[j].associations[i].session.state = MS_DONE &
   (ms[j].associations[i].sid = bs[i].associations[j].sid) &      
   (bs[i].associations[j].session.state = BS_DONE)) 

   ->
 
   (bs[i].associations[j].TEKnonce = ms[j].associations[i].TEKnonce)

    end
   end;


/*
-- If MS is waiting for RES then costs ==  MS_WAIT_RES_COST
invariant "If MS is WAIT_RES => costs =  MS_WAIT_RES_COST" 

  forall i: BSId do
    forall j: MSId do

   (ms[j].associations[i].session.state = MS_WAIT_RES)

   ->

   (ms[j].associations[i].session.costs <= MS_WAIT_RES_COST)

     end
  end;
*/

/*
-- If MS is waiting for RES then costs == MS_WAIT_RES_COST and intCosts > threshold
invariant "If MS is WAIT_RES => costs = MS_WAIT_RES_COST and intCosts > threshold" 

  forall i: BSId do
    forall j: MSId do

   (ms[j].associations[i].session.state = MS_WAIT_RES)

   ->

   (ms[j].associations[i].session.costs <= MS_WAIT_RES_COST | ms[j].associations[i].session.intCosts > INT_RES_THRESHOLD)

     end
  end;
*/
/*
-- If MS is waiting done then costs == MS_DONE_COST
invariant "If MS is DONE => costs = MS_DONE_COST" 

  forall i: BSId do
    forall j: MSId do

   (ms[j].associations[i].session.state = MS_DONE)

   ->

   (ms[j].associations[i].session.costs <= MS_DONE_COST)

     end
   end;
*/

-- If MS is waiting done then costs == MS_DONE_COST
invariant "If MS is DONE => costs = MS_DONE_COST and intCosts > threshold" 

  forall i: BSId do
    forall j: MSId do

   (ms[j].associations[i].session.state = MS_DONE)

   ->

   (ms[j].associations[i].session.costs <= MS_DONE_COST | ms[j].associations[i].session.intCosts > INT_THRESHOLD)

     end
   end;


/*
-- If BS is waiting for REQ then costs == BS_DONE_COST
invariant "If BS is WAIT_REQ => costs = BS_DONE_COST" 

  forall i: BSId do
    forall j: MSId do

   (bs[i].associations[j].session.state = BS_WAIT_REQ)

   ->

   (bs[i].associations[j].session.costs <= BS_DONE_COST)

     end
  end;
*/
