-------------------------------------------------------------------------------- -- -- Murphi Model of the Needham-Schroeder protocol (with bug) -- -------------------------------------------------------------------------------- -- -- version: 1.0 -- -- written by: Ulrich Stern -- date: Sep 1996 -- affiliation: Stanford University (visiting scholar), -- Technical University of Munich (PhD student) -- -------------------------------------------------------------------------------- -- -- only the following three steps of the protocol are modeled: -- -- 3. A->B: {Na,A}Kb -- 6. B->A: {Na,Nb}Ka -- A assumes it is talking to B -- 7. A->B: {Nb}Kb -- B assumes it is talking to A -- -- A: initiator, B: reponder -- -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- -- constants, types and variables -------------------------------------------------------------------------------- -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - const NumInitiators: 1; -- number of initiators NumResponders: 1; -- number of responders NumIntruders: 1; -- number of intruders NetworkSize: 1; -- max. number of outstanding messages in network MaxKnowledge: 10; -- max. number of messages intruder can remember -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - type InitiatorId: scalarset (NumInitiators); -- identifiers ResponderId: scalarset (NumResponders); IntruderId: scalarset (NumIntruders); AgentId: union {InitiatorId, ResponderId, IntruderId}; MessageType : enum { -- different types of messages M_NonceAddress, -- {Na, A}Kb: nonce and address M_NonceNonce, -- {Na,Nb}Ka: two nonces M_Nonce -- {Nb}Kb: one nonce }; Message : record source: AgentId; -- source of message dest: AgentId; -- intended destination of message key: AgentId; -- key used for encryption mType: MessageType; -- type of message nonce1: AgentId; -- nonce1 nonce2: AgentId; -- nonce2 OR sender identifier OR empty end; -- remark: keys, nonces and addresses are encoded in the message by their -- agent's identifier only. They can be distinguished by their po- -- sition and the type of the message InitiatorStates : enum { I_SLEEP, -- state after initialization I_WAIT, -- waiting for response from responder I_COMMIT -- initiator commits to session }; -- (thinks responder is authenticated) Initiator : record state: InitiatorStates; responder: AgentId; -- agent with whom the initiator starts the end; -- protocol ResponderStates : enum { R_SLEEP, R_WAIT, R_COMMIT }; Responder : record state: ResponderStates; initiator: AgentId; 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 ini: array[InitiatorId] of Initiator; -- initiators res: array[ResponderId] of Responder; -- responders int: array[IntruderId] of Intruder; -- intruders -------------------------------------------------------------------------------- -- rules -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- -- behavior of initiators -- initiator i starts protocol with responder or intruder j (step 3) ruleset i: InitiatorId do ruleset j: AgentId do rule "initiator starts protocol (step 3)" ini[i].state = I_SLEEP & !ismember(j,InitiatorId) & -- only responders and intruders multisetcount (l:net, true) < NetworkSize ==> var outM: Message; -- outgoing message begin undefine outM; outM.source := i; outM.dest := j; outM.key := j; outM.mType := M_NonceAddress; outM.nonce1 := i; outM.nonce2 := i; multisetadd (outM,net); ini[i].state := I_WAIT; ini[i].responder := j; end; end; end; -- initiator i reacts to nonce received (steps 6/7) ruleset i: InitiatorId do choose j: net do rule "initiator reacts to nonce received (steps 6/7)" ini[i].state = I_WAIT & net[j].dest = i ==> var outM: Message; -- outgoing message inM: Message; -- incoming message begin inM := net[j]; multisetremove (j,net); if inM.key=i then -- message is encrypted with i's key if inM.mType=M_NonceNonce then -- correct message type if inM.nonce1=i then -- correct nonce received undefine outM; outM.source := i; outM.dest := ini[i].responder; outM.key := ini[i].responder; outM.mType := M_Nonce; outM.nonce1 := inM.nonce2; multisetadd (outM,net); ini[i].state := I_COMMIT; else --error "initiator received incorrect nonce" end; end; end; end; end; end; -------------------------------------------------------------------------------- -- behavior of responders -- responder i reacts to initiator's nonce (steps 3/6) ruleset i: ResponderId do choose j: net do rule "responder reacts to initiator's nonce (steps 3/6)" res[i].state = R_SLEEP & net[j].dest = i ==> var outM: Message; -- outgoing message inM: Message; -- incoming message begin inM := net[j]; multisetremove (j,net); if inM.key=i then -- message is encrypted with i's key if inM.mType=M_NonceAddress then -- correct message type undefine outM; outM.source := i; outM.dest := inM.nonce2; -- identifier of initiator outM.key := inM.nonce2; outM.mType := M_NonceNonce; outM.nonce1 := inM.nonce1; outM.nonce2 := i; multisetadd (outM,net); res[i].state := R_WAIT; res[i].initiator := inM.nonce2; end; end; end; end; end; -- responder i reacts to own nonce (step 7) ruleset i: ResponderId do choose j: net do rule "responder reacts to own nonce (step 7)" res[i].state = R_WAIT & net[j].dest = i ==> begin alias inM: net[j] do -- incoming message if inM.key=i then -- message is encrypted with i's key if inM.mType=M_Nonce then -- correct message type if inM.nonce1=i then -- correct nonce received res[i].state := R_COMMIT; else --error "responder received incorrect nonce" end; end; end; multisetremove (j,net); end; end; end; end; -------------------------------------------------------------------------------- -- behavior of intruders -- intruder i overhears and/or intercepts messages ruleset i: IntruderId do choose j: net do ruleset intercept: boolean do rule "intruder overhears/intercepts" !ismember (net[j].source, IntruderId) -- not for intruders' messages ==> var temp: Message; begin alias msg: net[j] do -- message to overhear/intercept if msg.key=i then -- message is encrypted with i's key int[i].nonces[msg.nonce1] := true; -- learn nonces if msg.mType=M_NonceNonce then int[i].nonces[msg.nonce2] := true; end; else -- learn message alias messages: int[i].messages do temp := msg; undefine temp.source; -- delete useless information undefine temp.dest; if multisetcount (l:messages, -- add only if not there messages[l].key = temp.key & messages[l].mType = temp.mType & messages[l].nonce1 = temp.nonce1 & ( messages[l].mType != M_Nonce -> messages[l].nonce2 = temp.nonce2 ) ) = 0 then multisetadd (temp, int[i].messages); end; end; end; if intercept then -- intercept multisetremove (j,net); end; end; end; end; end; end; -- intruder i sends recorded message ruleset i: IntruderId do -- arbitrary choice of choose j: int[i].messages do -- recorded message ruleset k: AgentId do -- destination rule "intruder sends recorded message" !ismember(k, IntruderId) & -- not to intruders multisetcount (l:net, true) < NetworkSize ==> var outM: Message; begin outM := int[i].messages[j]; outM.source := i; outM.dest := k; multisetadd (outM,net); end; end; end; end; -- intruder i generates message with the nonces it knows ruleset i: IntruderId do -- arbitrary choice of ruleset j: AgentId do -- destination = key ruleset l: MessageType do -- message type ruleset m: AgentId do -- nonce1 ruleset n: AgentId do -- nonce2 ruleset o: AgentId do -- address rule "intruder generates message" !ismember(j, IntruderId) & -- not to intruders int[i].nonces[m] = true & -- nonces must be known int[i].nonces[n] = true & multisetcount (t:net, true) < NetworkSize ==> var outM: Message; begin undefine outM; outM.source := i; outM.dest := j; outM.key := j; outM.mType := l; switch l -- set content dependent on message type case M_NonceAddress: outM.nonce1 := m; outM.nonce2 := o; case M_NonceNonce: outM.nonce1 := m; outM.nonce2 := n; case M_Nonce: outM.nonce1 := m; end; multisetadd (outM,net); end; end; end; end; end; end; end; -------------------------------------------------------------------------------- -- startstate -------------------------------------------------------------------------------- startstate -- initialize initiators undefine ini; for i: InitiatorId do ini[i].state := I_SLEEP; end; -- initialize responders undefine res; for i: ResponderId do res[i].state := R_SLEEP; end; -- initialize intruders undefine int; for i: IntruderId do -- the only nonce known is the own one for j: AgentId do int[i].nonces[j] := false; end; int[i].nonces[i] := true; end; -- initialize network undefine net; end; -------------------------------------------------------------------------------- -- invariants -------------------------------------------------------------------------------- invariant "responder correctly authenticated" forall i: InitiatorId do ini[i].state = I_COMMIT & ismember(ini[i].responder, ResponderId) -> res[ini[i].responder].initiator = i & ( res[ini[i].responder].state = R_WAIT | res[ini[i].responder].state = R_COMMIT ) end; invariant "initiator correctly authenticated" forall i: ResponderId do res[i].state = R_COMMIT & ismember(res[i].initiator, InitiatorId) -> ini[res[i].initiator].responder = i & ini[res[i].initiator].state = I_COMMIT end;