--------------------------------------------------------------------------------
--
--  Murphi Model of the Mobike protocol
--
--------------------------------------------------------------------------------
--
--  version:      1.0
--
--  written by:   Faisal Memon and Erik Weathers
--  date:         February 2006
--  affiliation:  Stanford University (students)
--
--------------------------------------------------------------------------------
--
--       Initiator                  Responder
--      -----------                -----------
--    1) (IP_I1:500 -> IP_R1:500)
--       HDR, SAi1, KEi, Ni,
--            N(NAT_DETECTION_SOURCE_IP),
--            N(NAT_DETECTION_DESTINATION_IP)  -->
-- 
--                             <--  (IP_R1:500 -> IP_I1:500)
--                                  HDR, SAr1, KEr, Nr,
--                                       N(NAT_DETECTION_SOURCE_IP),
--                                       N(NAT_DETECTION_DESTINATION_IP)
-- 
--    2) (IP_I1:4500 -> IP_R1:4500)
--       HDR, SK { IDi, CERT, AUTH,
--                 CP(CFG_REQUEST),
--                 SAi2, TSi, TSr,
--                 N(MOBIKE_SUPPORTED) }  -->
-- 
--                             <--  (IP_R1:4500 -> IP_I1:4500)
--                                  HDR, SK { IDr, CERT, AUTH,
--                                            CP(CFG_REPLY),
--                                            SAr2, TSi, TSr,
--                                            N(MOBIKE_SUPPORTED) }
-- 
--    (Initiator gets information from lower layers that its attachment
--    point and address have changed.)
-- 
--    3) (IP_I2:4500 -> IP_R1:4500)
--       HDR, SK { N(UPDATE_SA_ADDRESSES),
--                 N(NAT_DETECTION_SOURCE_IP),
--                 N(NAT_DETECTION_DESTINATION_IP) }  -->
-- 
--                             <-- (IP_R1:4500 -> IP_I2:4500)
--                                 HDR, SK { N(NAT_DETECTION_SOURCE_IP),
--                                      N(NAT_DETECTION_DESTINATION_IP) }
-- 
--    (Responder verifies that the initiator has given it
--    a correct IP address.)
-- 
--    4)                       <-- (IP_R1:4500 -> IP_I2:4500)
--                                 HDR, SK { N(COOKIE2) }
-- 
--       (IP_I2:4500 -> IP_R1:4500)
--       HDR, SK { N(COOKIE2) }  -->
-- 
--
--------------------------------------------------------------------------------

--
--


--------------------------------------------------------------------------------
-- constants, types and variables
--------------------------------------------------------------------------------


-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
const

  NO_NATS_ALLOWED: true;   -- are we allowing NATs in this test run?
  NumInitiators:   1;   -- number of initiators
  NumResponders:   1;   -- number of responders
  NumInitiators_p: 1;   -- number of initiator primes
  NumIntruders:    1;   -- number of intruders
  NetworkSize:     1;   -- max number of outstanding messages in network
  MaxKnowledge:   10;   -- max number of messages intruder can remember
  MaxRandom:      268435455; -- max value for random numbers
  MaxSpis:        10;   -- max number of spis
  SharedSecret:   12345;
  Generator:      2;
  Prime:          7919;


-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
type
  InitiatorId:  scalarset (NumInitiators);     -- identifiers
  InitiatorIdP: scalarset (NumInitiators_p);   -- identifiers
  ResponderId:  scalarset (NumResponders);
  IntruderId:   scalarset (NumIntruders);
  SpiId:        0..MaxSpis;
  Random:       0..MaxRandom;
  Integer:      0..99999;
  
  AgentId:      union {InitiatorId, InitiatorIdP, ResponderId, IntruderId};

  MessageType : enum {           -- different types of messages
    PRE_MOBIKE_1,           -- state of initiator prior to start of protocol

    MOBIKE_1,               --          IKE_INIT -->
    MOBIKE_2,               --                      <-- IKE_INIT
    MOBIKE_3,               --          IKE_AUTH -->     
    MOBIKE_4,               --                      <-- IKE_AUTH
    MOBIKE_5,               --   IKE_UPDATE_ADDR -->
    MOBIKE_6,               --                      <-- IKE_UPDATE_ADDR
    MOBIKE_7,               --                      <-- IKE_RETURN_ROUTE
    MOBIKE_8,               --  IKE_RETURN_ROUTE -->

    MOBIKE_ADDR_CHANGE,     -- only used as state for session when transitioning
                            --  from initiator to initiator-prime, not as a real
                            --  msg type.
    MOBIKE_DONE         
  };

  Ke: record
    random:	Random;
  end;

  SessionKey: record
    random:	Random;
  end;

  Spi: record
    ke:          Ke;
    peer_ke:     Ke;
    peer:        AgentId;
    peer_spi_id: SpiId;
    spi_id:      SpiId;
    nonce:       Random;
    peer_nonce:  Random;
    msgid:       Integer;
    peer_msgid:  Integer;
    cookie:      Random;
    exponent:    Random;        -- a or b, depending on who we are       
    session_key: SessionKey;
    state:       MessageType;
    in_use:      boolean;
  end;

  Auth: record
    msgid: Integer;
    ke:    Ke;
    nonce: Random;
    spi:   SpiId;
    peer_nonce: Random;
    id_p:       AgentId;
    shared_secret: Integer;
  end;

  Message : record
    source:   AgentId;           -- source of message
    dest:     AgentId;           -- intended destination of message
    msgid:    Integer;
    init_spi: SpiId;
    resp_spi: SpiId;
    mType:    MessageType;       -- type of message
    ke_i:     Ke;               -- Ke used for encryption
    ke_r:     Ke;               -- dh partial Ke OR ID
    nonce_i:  Random;
    nonce_r:  Random;
    id_i:     AgentId;
    id_r:     AgentId;
    auth:     Auth;
    mobike_s: boolean;
    upd_addr: AgentId;
    cookie:   Random;            -- cookie used for return routability check
    no_nats_allowed_source: AgentId;
    no_nats_allowed_dest:   AgentId;
    session_key: SessionKey;
    from_intruder:  boolean;
  end;

  Intruder : record
    nonces:   array[AgentId] of boolean;           -- known nonces
    messages: multiset[MaxKnowledge] of Message;   -- known messages
  end;


-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
var                                                      -- state variables for
  net:               multiset[NetworkSize] of Message;    --  network
  initiator_spi:     array[SpiId] of Spi;
  responder_spi:     array[SpiId] of Spi;
  next_random:       Random;
  initiator_num_spis: SpiId;
  int: array[IntruderId] of Intruder;       --  intruders



--------------------------------------------------------------------------------
-- utility functions
--------------------------------------------------------------------------------

-- Generate a fresh random number

function new_random(): Random;
var tmp: Random;
begin
   tmp := next_random;
   next_random := next_random + 1;
   return tmp;
end;
         
function make_ke(exponent: Random): Ke;
var tmp_ke: Ke;
var tmp_exp: Random;
begin
    tmp_exp := exponent;
    if (tmp_exp = 0) then 
        error "make_ke: exponent not allowed to be 0\n";
    else
        tmp_ke.random := Generator;
        while tmp_exp > 1 do
            tmp_ke.random := tmp_ke.random * Generator;
            tmp_exp := tmp_exp - 1;
        end;
        tmp_ke.random := (tmp_ke.random % Prime);
    end;
    return tmp_ke;
end;

-- Using "DH group 0", our made up group that uses a pitifully small 
-- prime number
-- raise g to the exponent, and 
function make_session_key (ke_peer: Ke; exponent: Random): SessionKey;
var tmp_sk: SessionKey;
var tmp_exp: Random;
begin
    tmp_exp := exponent;
    if (tmp_exp = 0) then 
        error "make_session_key: exponent not allowed to be 0\n";
    else
        tmp_sk.random := ke_peer.random;
        while tmp_exp > 1 do
            tmp_sk.random := tmp_sk.random * Generator;
            tmp_exp := tmp_exp - 1;
        end;
        tmp_sk.random := (tmp_sk.random % Prime);
    end;
    return tmp_sk;
end;

function initiator_new_spi(): Spi;
begin
    for i: SpiId do
        if i != 0 & initiator_spi[i].in_use = false then
            initiator_spi[i].in_use := true;
            initiator_num_spis := initiator_num_spis + 1;
            return initiator_spi[i];
        end;
    end;
    error "initiator: no more spis available";
end;

function responder_new_spi(): Spi;
begin
    for i: SpiId do
        if i != 0 & responder_spi[i].in_use = false then
            responder_spi[i].in_use := true;
            return responder_spi[i];
        end;
    end;
    error "responder: no more spis available";
end;

--------------------------------------------------------------------------------
-- rules
--------------------------------------------------------------------------------


--------------------------------------------------------------------------------
-- behavior of initiators

-- initiator i starts protocol with responder or intruder j (step 1)
ruleset i: InitiatorId do
    ruleset j: ResponderId do
        rule 20 "initiator starts protocol (step 1)"
            initiator_num_spis = 0 &
            multisetcount (l:net, true) < NetworkSize

    ==>
    
    var
      outM: Message;   -- outgoing message
      spi:  Spi;

    begin
      -- Create the SPI for this session
      undefine spi;
      spi := initiator_new_spi();
      put "pas initiator_new_spi stuff\n";
      spi.peer := j;
      spi.exponent       := new_random();

      -- Form the first message and send it out
      undefine outM;
      outM.source        := i;
      outM.dest          := j;
      outM.init_spi      := spi.spi_id;
      outM.resp_spi      := 0;
      outM.mType         := MOBIKE_1;
      outM.ke_i          := make_ke(spi.exponent);
      outM.nonce_i       := new_random();
      outM.from_intruder := false;
      outM.msgid         := 0;
      outM.session_key   := spi.session_key;
      multisetadd (outM,net);

      -- add SPI to multiset
      spi.state := MOBIKE_2;
      spi.peer_spi_id := 0;
      spi.nonce := outM.nonce_i;
      spi.ke := outM.ke_i;
      spi.msgid := outM.msgid;
      initiator_spi[spi.spi_id] := spi;
    end;
  end;
end;

-- initiator i main process
ruleset i: InitiatorId do
    choose j: net do
        rule 20 "initiator main process"
            net[j].dest = i

    ==>

    var
        outM: Message;   -- outgoing message
        inM:  Message;   -- incoming message
        spi_id:  SpiId;
        spi:     Spi;
        auth:    Auth;
        continue_MOBIKE: boolean;

    begin
        inM := net[j];
        multisetremove (j,net);
        spi_id := inM.init_spi;
        spi := initiator_spi[spi_id];
        continue_MOBIKE := true;

        switch inM.mType
        case MOBIKE_2:
            if (spi.in_use = true &
                spi.peer = inM.source &
                spi.state = MOBIKE_2) then

                if spi.peer_msgid != inM.msgid then
                    put "initiator: mismatch of msgid\n";
                else

                    -- Update the SPI
                    spi.state := MOBIKE_4;
                    spi.peer_spi_id := inM.resp_spi;
                    spi.peer_nonce := inM.nonce_r;
                    spi.peer_ke := inM.ke_r;
                    spi.peer_msgid := inM.msgid + 1;
                    spi.session_key := make_session_key(inM.ke_r, spi.exponent);
                    put "Initiator: session_key: ";
                    put spi.session_key;

                    -- Create the Auth payload
                    undefine auth;
                    auth.msgid := spi.msgid;
                    auth.ke := spi.ke;
                    auth.nonce := spi.nonce;
                    auth.spi := spi.spi_id;
                    auth.peer_nonce := spi.peer_nonce;
                    auth.id_p := i;
                    auth.shared_secret := SharedSecret;

                    undefine outM;
                    outM.source   := i;
                    outM.dest     := spi.peer;
                    outM.mType    := MOBIKE_3;
                    outM.msgid    := spi.msgid + 1;
                    outM.init_spi := spi_id;
                    outM.resp_spi := spi.peer_spi_id;
                    outM.id_i     := i;
                    outM.auth     := auth;
                    if NO_NATS_ALLOWED then
                        outM.no_nats_allowed_source := outM.source;
                        outM.no_nats_allowed_dest := outM.dest;
                    endif;
                    outM.mobike_s := true;
                    outM.from_intruder := false;
                    outM.session_key   := spi.session_key;

                    multisetadd (outM,net);

                    spi.msgid := outM.msgid;
                    initiator_spi[spi_id] := spi;
                end;

            else
                put "initiator received unsolicited MOBIKE_2 message\n"; 
            end;

        case MOBIKE_4:
            if (spi.in_use = true &
                spi.peer = inM.source &
                spi.peer_spi_id = inM.resp_spi &
                spi.state = MOBIKE_4) then

                -- First check correctness of received message
                if inM.id_r != spi.peer then
                    put "initiator: incorrect id_r\n";
                    continue_MOBIKE := false;
                end;

                if spi.peer_msgid != inM.msgid then
                    put "initiator: mismatch of msgid\n";
                    continue_MOBIKE := false;
                end;

                -- Check the auth payload
                undefine auth;
                auth := inM.auth;
                if auth.ke.random != spi.peer_ke.random |
                   auth.nonce != spi.peer_nonce |
                   auth.spi != spi.peer_spi_id |
                   auth.peer_nonce != spi.nonce |
                   auth.id_p != spi.peer |
                   auth.shared_secret != SharedSecret |
                   auth.msgid != spi.peer_msgid - 1 then
                   put "initiator: invalid auth payload\n";
                   continue_MOBIKE := false;
                end;

                if continue_MOBIKE = true then
                    spi.peer_msgid := inM.msgid + 1;
                    spi.state := MOBIKE_ADDR_CHANGE;
                    initiator_spi[spi_id] := spi;
                end;
            else
                put "initiator received unsolicited MOBIKE_4 message\n"; 
            end;
        endswitch;
        end;
    end;
end;

ruleset i: InitiatorIdP do
    ruleset spi_id: SpiId do
        rule 20 "initiator address change (step 6)"
            initiator_spi[spi_id].in_use = true &
            initiator_spi[spi_id].state = MOBIKE_ADDR_CHANGE
     
     ==>

     var
        outM: Message;   -- outgoing message
        spi: Spi;

    begin
        undefine outM;
        undefine spi;
        spi := initiator_spi[spi_id];

        put "received addr change message\n";
        outM.source := i;
        outM.dest := spi.peer;
        outM.init_spi := spi.spi_id;
        outM.resp_spi := spi.peer_spi_id;
        outM.mType := MOBIKE_5;
        outM.from_intruder := false;
        if NO_NATS_ALLOWED then
            outM.no_nats_allowed_source := outM.source;
            outM.no_nats_allowed_dest := outM.dest;
        end;
        outM.msgid := spi.msgid + 1;
        outM.session_key := spi.session_key;

        multisetadd (outM,net);

        initiator_spi[spi_id].msgid := outM.msgid;
        initiator_spi[spi_id].state := MOBIKE_6;
    end;
    end;
end;

-- initiator prime main process
ruleset i: InitiatorIdP do
    choose j: net do
        rule 20 "initiator_p main process"
            net[j].dest = i

    ==>

    var
        outM: Message;   -- outgoing message
        inM:  Message;   -- incoming message
        spi_id:  SpiId;
        spi:     Spi;

    begin
        inM := net[j];
        multisetremove (j,net);
        spi_id := inM.init_spi;
        spi := initiator_spi[spi_id];

        if spi.peer_msgid != inM.msgid then
            put "initiator: mismatch of msgid\n";
        else

            switch inM.mType
            case MOBIKE_6:
                if (spi.in_use = true &
                    spi.peer = inM.source &
                    spi.peer_spi_id = inM.resp_spi &
                    spi.state = MOBIKE_6) then

                    put "initiator received expected MOBIKE_6 message\n"; 
                    spi.peer_msgid := inM.msgid + 1;
                    spi.state := MOBIKE_7;
                    initiator_spi[spi_id] := spi;
                else
                    put "initiator received unsolicited MOBIKE_6 message\n"; 
                end;

            case MOBIKE_7:
                if (spi.in_use = true &
                    spi.peer = inM.source &
                    spi.peer_spi_id = inM.resp_spi &
                    spi.state = MOBIKE_7) then

                    put "initiator received MOBIKE_7 message\n"; 
                    undefine outM;
                    outM.source   := i;
                    outM.dest     := inM.source;
                    outM.init_spi := spi.spi_id;
                    outM.resp_spi := spi.peer_spi_id;
                    outM.mType    := MOBIKE_8;
                    outM.cookie   := inM.cookie;
                    outM.from_intruder := false;
                    outM.msgid    := spi.msgid + 1;
                    outM.session_key := spi.session_key;

                    multisetadd(outM,net);

                    spi.msgid := outM.msgid;
                    spi.peer_msgid := inM.msgid + 1;
                    spi.state := MOBIKE_DONE;
                    initiator_spi[spi_id] := spi;
                else
                    put "initiator received unsolicited MOBIKE_7 message\n"; 
                end;
            endswitch;
        end; -- if/else
        end;
    end;
end;

--------------------------------------------------------------------------------
-- behavior of responders

-- responder i reacts to MOBIKE_1
ruleset i: ResponderId do
    choose j: net do
        rule 20 "responder main process"
            net[j].dest = i
    ==>

    var
        outM: Message;   -- outgoing message
        inM:  Message;   -- incoming message
        spi:  Spi;
        spi_id:  SpiId;
        auth:    Auth;
        continue_MOBIKE : boolean;

    begin
        undefine inM;
        undefine spi;
        inM := net[j];
        multisetremove (j,net);
        continue_MOBIKE := true;
        spi_id := inM.resp_spi;
        spi := responder_spi[spi_id];

        switch inM.mType
        case MOBIKE_1:
                -- Create a new SPI based on this message
                spi := responder_new_spi();
                spi.peer := inM.source;
                spi.peer_spi_id := inM.init_spi;
                spi.peer_ke := inM.ke_i;
                spi.peer_nonce := inM.nonce_i;
                spi.peer_msgid := 0;
                spi.exponent := new_random();

                if spi.peer_msgid != inM.msgid then
                    put "responder: mismatch of msgid\n";
                else
                    -- respond to the message
                    undefine outM;
                    outM.source  := i;
                    outM.dest    := spi.peer;   -- identifier of initiator
                    outM.mType   := MOBIKE_2;
                    outM.ke_r    := make_ke(spi.exponent);
                    outM.nonce_r := new_random();
                    outM.init_spi := spi.peer_spi_id;
                    outM.resp_spi := spi.spi_id;
                    outM.from_intruder := false;
                    outM.msgid := 0;
                    outM.session_key := spi.session_key;

                    multisetadd (outM,net);

                    -- Update the Spi
                    spi.session_key := make_session_key(inM.ke_i, spi.exponent);
                    put "Responder: session_key: ";
                    put spi.session_key;
                    spi.msgid := outM.msgid;
                    spi.peer_msgid := inM.msgid + 1;
                    spi.nonce := outM.nonce_r;
                    spi.ke := outM.ke_r;
                    spi.state := MOBIKE_3;
                    responder_spi[spi.spi_id] := spi;
                end;

        case MOBIKE_3:
            if (spi.in_use = true &
                spi.peer = inM.source &
                spi.peer_spi_id = inM.init_spi &
                spi.state = MOBIKE_3) then

                if NO_NATS_ALLOWED then
                    if inM.no_nats_allowed_source != inM.source then
                        put "NO_NATS_ALLOWED, but the MOBIKE_3's ";
                        put "source address changed\n";
                        continue_MOBIKE := false;
                    end;
                    if inM.no_nats_allowed_dest != inM.dest then
                        put "NO_NATS_ALLOWED, but the MOBIKE_3's ";
                        put "dest address changed\n";
                        continue_MOBIKE := false;
                    end;
                end;

                if inM.id_i != spi.peer then
                    put "responder: incorrect id_i\n";
                    continue_MOBIKE := false;
                end;

                if spi.peer_msgid != inM.msgid then
                    put "responder: mismatch of msgid\n";
                    continue_MOBIKE := false;
                end;
                
                -- Check the auth payload
                undefine auth;
                auth := inM.auth;
                if auth.ke.random != spi.peer_ke.random |
                   auth.nonce != spi.peer_nonce |
                   auth.spi != spi.peer_spi_id |
                   auth.peer_nonce != spi.nonce |
                   auth.id_p != spi.peer |
                   auth.msgid != spi.peer_msgid - 1 |
                   auth.shared_secret != SharedSecret then
                   put "responder: invalid auth payload\n";
                   continue_MOBIKE := false;
                end;

                if continue_MOBIKE then
                    -- Create the Auth payload
                    undefine auth;
                    auth.ke := spi.ke;
                    auth.nonce := spi.nonce;
                    auth.peer_nonce := spi.peer_nonce;
                    auth.spi := spi.spi_id;
                    auth.id_p := i;
                    auth.shared_secret := SharedSecret;
                    auth.msgid := spi.msgid;

                    undefine outM;
                    outM.source  := i;
                    outM.dest    := spi.peer;   -- identifier of initiator
                    outM.mType   := MOBIKE_4;
                    outM.init_spi := spi.peer_spi_id;
                    outM.resp_spi := spi.spi_id;
                    outM.id_r    := i;
                    outM.auth    := auth;
                    outM.mobike_s := true; 
                    outM.from_intruder := false;
                    outM.msgid    := spi.msgid + 1;
                    outM.session_key := spi.session_key;

                    multisetadd (outM,net);

                    spi.msgid := outM.msgid;
                    spi.peer_msgid := inM.msgid + 1;
                    spi.state := MOBIKE_5;
                    responder_spi[spi.spi_id] := spi;
                end;
            else
                put "responder received unsolicited MOBIKE_3 message\n"; 
            end;
            
        case MOBIKE_5:
            if (spi.in_use = true &
                spi.peer_spi_id = inM.init_spi &
                spi.state = MOBIKE_5) then

                if NO_NATS_ALLOWED then
                    if inM.no_nats_allowed_source != inM.source then
                        put "NO_NATS_ALLOWED, but the MOBIKE_5's ";
                        put "source address changed\n";
                        continue_MOBIKE := false;
                    end;
                    if inM.no_nats_allowed_dest != inM.dest then
                        put "NO_NATS_ALLOWED, but the MOBIKE_5's ";
                        put "dest address changed\n";
                        continue_MOBIKE := false;
                    end;
                end;

                if spi.peer_msgid != inM.msgid then
                    put "responder: mismatch of msgid\n";
                    continue_MOBIKE := false;
                end;
 
                if continue_MOBIKE then
                    -- Update the spi
                    spi.peer := inM.source;

                    -- And acknowledge the address change
                    undefine outM;
                    outM.source  := i;
                    outM.dest    := spi.peer;   -- identifier of initiator
                    outM.mType   := MOBIKE_6;
                    outM.init_spi := spi.peer_spi_id;
                    outM.resp_spi := spi.spi_id;
                    outM.from_intruder := false;
                    outM.msgid    := spi.msgid + 1;
                    outM.session_key := spi.session_key;

                    multisetadd (outM,net);

                    spi.msgid := outM.msgid;
                    spi.peer_msgid := inM.msgid + 1;
                    spi.state := MOBIKE_7;
                    responder_spi[spi.spi_id] := spi;
                end;
            else
                put "responder received unsolicited MOBIKE_5 message\n"; 
            end;

        case MOBIKE_8:
            if (spi.in_use = true &
                spi.peer = inM.source &
                spi.peer_spi_id = inM.init_spi &
                spi.state = MOBIKE_8) then
                assert(inM.cookie = spi.cookie);
                if spi.peer_msgid != inM.msgid then
                    put "responder: mismatch of msgid\n";
                else
                    put "Cookie received, we're done\n";
                    spi.peer_msgid := inM.msgid + 1;
                    responder_spi[spi.spi_id].state := MOBIKE_DONE;
                end;
            else
                put "responder received unsolicited MOBIKE_8 message\n"; 
            end;
        endswitch;
        end;
    end;
end;

ruleset i: ResponderId do
    ruleset j: SpiId do
        rule 20 "responder sub process"
            responder_spi[j].in_use = true &
            responder_spi[j].state = MOBIKE_7 &
            multisetcount(l:net, true) < NetworkSize
    
    ==>

    var
        outM: Message;   -- outgoing message
        spi:  Spi;

    begin
        undefine spi;
        undefine outM;

        spi := responder_spi[j];
        outM.source  := i;
        outM.dest    := spi.peer;   -- identifier of initiator
        outM.mType   := MOBIKE_7;
        outM.init_spi := spi.peer_spi_id;
        outM.resp_spi := spi.spi_id;
        outM.cookie  := new_random(); -- random cookie for
        outM.from_intruder := false;
        -- res[i].cookie := outM.cookie;
        outM.msgid := spi.msgid + 1;
        outM.session_key := spi.session_key;

        multisetadd (outM,net);

        spi.cookie := outM.cookie;
        spi.msgid := outM.msgid;
        spi.state := MOBIKE_8;
        responder_spi[j] := spi;
    end;
    end;
end;

--------------------------------------------------------------------------------
-- behavior of intruders

-- intruder i intercepts messages
ruleset i: IntruderId do
    choose j: net do
        rule 10 "intruder intercepts"
            !ismember (net[j].source, IntruderId) &
            !net[j].from_intruder

    ==>

    var
        temp: Message;

    begin
        alias msg: net[j] do   -- message to intercept
            if msg.dest = i then   -- message is to intruder i
                -- do nothing for now
            else                   -- learn message
                alias messages: int[i].messages do
                    temp := msg;
                    if multisetcount (l:messages,   -- add only if not there
                           messages[l].source = temp.source &
                           messages[l].dest = temp.dest &
                           messages[l].mType = temp.mType &
                           ( messages[l].mType = MOBIKE_1 ->
                             messages[l].nonce_i = temp.nonce_i ) &
                           ( messages[l].mType = MOBIKE_2 ->
                             messages[l].nonce_r = temp.nonce_r )) = 0 then
                        multisetadd (temp, int[i].messages);
                        put "Intruder picking up message ";
                        put temp.mType;
                     end;
                end; -- alias
            end; -- if/else
            multisetremove (j,net);
        end; -- alias
    end; -- begin
    end; -- choose
end; -- ruleset

-- intruder i sends recorded message
ruleset i: IntruderId do         -- arbitrary choice of
    ruleset j: AgentId do
        ruleset k: AgentId do
            choose msg_index: int[i].messages do   --  recorded message
                rule 90 "intruder sends recorded message"
                    j != k &
                    multisetcount (l:net, true) < NetworkSize

    ==>

    var
        outM: Message;

    begin
        alias outM: int[i].messages[msg_index] do
            outM.from_intruder := true;
            outM.source := j;
            outM.dest   := k;
           -- outM.id_r   := j;
            multisetadd (outM,net);
           -- multisetremove(l, int[i].messages);
           -- put "Intruder sending message ";
           -- put outM.mType;
        end;
        multisetremove(msg_index, int[i].messages);
    end;
            end;
        end;
    end;
end;

--------------------------------------------------------------------------------
-- startstate
--------------------------------------------------------------------------------

startstate

  -- initialize variables
  next_random := 7;

  -- initialize initiators
  initiator_num_spis := 0;
  undefine initiator_spi;
  for i: SpiId do
    initiator_spi[i].ke.random := 0;
    initiator_spi[i].peer_ke.random := 0;
    initiator_spi[i].session_key.random := 0;
    initiator_spi[i].msgid := 0;
    initiator_spi[i].peer_msgid := 0;
    initiator_spi[i].nonce := 0;
    initiator_spi[i].peer_nonce := 0;
    initiator_spi[i].cookie := 0;
    initiator_spi[i].exponent := 0;
    initiator_spi[i].spi_id := i;
    initiator_spi[i].in_use := false;
  end;
    
  -- initialize responders
  undefine responder_spi;
  for i: SpiId do
    responder_spi[i].ke.random := 0;
    responder_spi[i].peer_ke.random := 0;
    responder_spi[i].session_key.random := 0;
    responder_spi[i].msgid := 0;
    responder_spi[i].peer_msgid := 0;
    responder_spi[i].nonce := 0;
    responder_spi[i].peer_nonce := 0;
    responder_spi[i].cookie := 0;
    responder_spi[i].exponent := 0;

    responder_spi[i].spi_id := i;
    responder_spi[i].in_use := false;
  end;

  -- initialize network 
  undefine net;
end;

--------------------------------------------------------------------------------
-- invariants
--------------------------------------------------------------------------------

invariant "responder correctly authenticated"
  forall i: InitiatorIdP do
    forall j: SpiId do
      initiator_spi[j].in_use = true &
      initiator_spi[j].state = MOBIKE_DONE &
      ismember(initiator_spi[j].peer, ResponderId)
    ->
    responder_spi[initiator_spi[j].peer_spi_id].in_use = true &
    responder_spi[initiator_spi[j].peer_spi_id].peer = i &
    ( responder_spi[initiator_spi[j].peer_spi_id].state = MOBIKE_DONE |
      responder_spi[initiator_spi[j].peer_spi_id].state = MOBIKE_8 )
    end
  end;

invariant "initiator correctly authenticated"
  forall i: ResponderId do
    forall j: SpiId do
      responder_spi[j].in_use = true &
      responder_spi[j].state = MOBIKE_DONE &
      ismember(responder_spi[j].peer, InitiatorIdP)
    ->
    initiator_spi[responder_spi[j].peer_spi_id].in_use = true &
    initiator_spi[responder_spi[j].peer_spi_id].peer = i &
    initiator_spi[responder_spi[j].peer_spi_id].state = MOBIKE_DONE
    end
  end;

invariant "responder and initiator have same session key"
  forall i: ResponderId do
    forall j: SpiId do
      responder_spi[j].in_use = true &
      responder_spi[j].state = MOBIKE_DONE &
      ismember(responder_spi[j].peer, InitiatorIdP)
    ->
    initiator_spi[responder_spi[j].peer_spi_id].in_use = true &
    initiator_spi[responder_spi[j].peer_spi_id].session_key.random = 
        responder_spi[j].session_key.random
    end
  end;
