-- ------------------------------------------------------------------------------ type InitiatorId: scalarset (NumInitiators); -- identifiers ResponderId: scalarset (NumResponders); IntruderId: scalarset (NumIntruders); AgentId: union {InitiatorId, ResponderId, IntruderId}; MessageType : enum { M_Hello, M_HashCommit, M_DH, M_SAS, M_INIT_CONVERSATION, M_RESP_CONVERSATION }; Message : record source: AgentId; -- source of message dest: AgentId; -- intended destination of message zid: AgentId; -- sender identifier or voice mType: MessageType; -- type of message hash: AgentId; -- hash commitment OR hash of shared secret or voice text publicDH: AgentId; -- a DH public value privateDH: AgentId; -- the pair of publicDH and privateDH specify who can decrypt the message responseTo: AgentId; -- for M_{INIT,RESP}_CONVERSATION, refers to who generated the text this is a response to. end; InitiatorStates : enum { I_SLEEP, -- state after initialization, or after first run of protocol is complete I_WAIT, -- waiting for hash commit from responder I_SENT_DH, -- waiting for DH response I_COMMIT, -- initiator commits to session I_READYTOTALK, -- initiator is ready to talk I_DONE -- initiator has said "yo, what's up?" and heard a response. }; Initiator : record state: InitiatorStates; responder: AgentId; -- agent with whom the initiator starts the protocol responderDH: AgentId; -- public DH value of other side responderSASVoice: AgentId; -- the voice of the responder in SAS responderConvVoice: array[AgentId] of AgentId; -- the voice of the responder in conversation responderConvTextSender: array[AgentId] of AgentId; -- the text generator of the responder in conversation resSharedSecret: array[AgentId] of AgentId; -- the secret we share with the responder connectedBefore: boolean; -- only used to prevent the state space from exploding end; ResponderStates : enum { R_SLEEP, -- state after initialization, or after first run of protocol is complete R_HASH_COMMITTED, -- committed to hash value waiting for DH R_COMMIT, -- received DH message and sent off own DH R_READYTOTALK, -- responder is ready to talk R_DONE -- responder has heard "yo, what's up?" and responded. }; Responder : record state: ResponderStates; initiator: AgentId; initiatorDH: AgentId; initiatorSASVoice: AgentId; -- the voice of the initiator in SAS initiatorConvVoice: array[AgentId] of AgentId; -- the voice of the initiator in conversation initiatorConvTextSender: array[AgentId] of AgentId; -- the text generator of the initiator in conversation iniSharedSecret: array[AgentId] of AgentId; -- the secret we share with the responder connectedBefore: boolean; -- only used to prevent the state space from exploding end; Intruder : record conversationtext: array[AgentId] of array[AgentId] of AgentId; 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 -- ------------------------------------------------------------------------------ ruleset i: InitiatorId do ruleset j: AgentId do rule "initiator starts protocol" ini[i].state = I_SLEEP & !ismember(j,InitiatorId) & -- only responders and intruders multisetcount (l:net, true) < NetworkSize ==> var outM: Message; -- outgoing message fooM: Message; begin undefine outM; outM.source := i; outM.dest := j; outM.zid := i; outM.mType := M_Hello; multisetadd (outM,net); ini[i].state := I_WAIT; ini[i].responder := j; end; end; end; ruleset i: InitiatorId do choose j: net do rule "initiator reacts to M_HashCommit received" ini[i].state = I_WAIT & net[j].dest = i & !ismember(net[j].source,InitiatorId) -- talk to everyone but initiators ==> var outM: Message; -- outgoing message inM: Message; -- incoming message begin inM := net[j]; multisetremove (j,net); if inM.mType = M_HashCommit then -- correct message type if inM.zid = ini[i].responder then -- correct zid undefine outM; outM.source := i; outM.dest := ini[i].responder; outM.mType := M_DH; outM.publicDH := i; outM.hash := i; -- we put our id in as the shared secret multisetadd (outM,net); ini[i].state := I_SENT_DH; end; end; end; end; end; ruleset i: InitiatorId do choose j: net do rule "initiator reacts to M_DH" ini[i].state = I_SENT_DH & net[j].dest = i & !ismember(net[j].source,InitiatorId) -- talk to everyone but initiators ==> var outM: Message; -- outgoing message inM: Message; -- incoming message begin inM := net[j]; multisetremove (j,net); if inM.mType = M_DH then -- correct message type ini[i].responderDH := inM.publicDH; undefine outM; -- if we share a secret with the responer, go straight to voice traffic -- the hash holds the secret that we supposedly share if ini[i].resSharedSecret[ini[i].responder] = inM.hash then outM.source := i; outM.dest := ini[i].responder; outM.mType := M_INIT_CONVERSATION; outM.publicDH := ini[i].responderDH; outM.privateDH := i; outM.zid := i; -- voice outM.hash := i; -- text of conversation outM.responseTo := ini[i].responder; multisetadd (outM,net); ini[i].state := I_READYTOTALK; else outM.source := i; outM.dest := ini[i].responder; outM.mType := M_SAS; outM.publicDH := ini[i].responderDH; outM.privateDH := i; outM.zid := i; outM.hash := i; -- we put our id in as the shared secret multisetadd (outM,net); ini[i].state := I_COMMIT; end; end; end; end; end; ruleset i: InitiatorId do choose j: net do rule "initiator reacts to M_SAS" ini[i].state = I_COMMIT & net[j].dest = i & !ismember(net[j].source,InitiatorId) -- talk to everyone but initiators ==> var outM: Message; -- outgoing message begin alias inM: net[j] do -- incoming message if inM.mType = M_SAS & inM.publicDH = i & inM.privateDH = ini[i].responderDH & (InitiatorUnawareOfRespondersVoiceInAdvance | ini[i].responder = inM.zid) then undefine outM; outM.source := i; outM.dest := ini[i].responder; outM.mType := M_INIT_CONVERSATION; outM.publicDH := ini[i].responderDH; outM.privateDH := i; outM.zid := i; -- voice outM.hash := i; -- text of conversation outM.responseTo := ini[i].responder; ini[i].state := I_READYTOTALK; ini[i].responderSASVoice := inM.zid; ini[i].resSharedSecret[ini[i].responder] := inM.hash; multisetremove (j,net); multisetadd (outM,net); else multisetremove (j,net); end; end; end; end; end; ruleset i: InitiatorId do choose j: net do rule "initiator reacts to M_RESP_CONVERSATION" ini[i].state = I_READYTOTALK & net[j].dest = i & !ismember(net[j].source,InitiatorId) -- talk to everyone but initiators ==> begin alias inM: net[j] do -- incoming message if inM.mType = M_RESP_CONVERSATION & inM.publicDH = i & inM.privateDH = ini[i].responderDH & inM.responseTo = i & (inM.zid = ini[i].responderSASVoice | (isUndefined(ini[i].responderSASVoice) & (InitiatorForgetsVoiceBetweenSessions | inM.zid = ini[i].responderConvVoice[ini[i].responder]))) & (InitiatorUnawareOfRespondersVoiceInAdvance | (ini[i].responder = inM.zid & ini[i].responder = inM.hash)) then ini[i].responderConvVoice[ini[i].responder] := inM.zid; ini[i].responderConvTextSender[ini[i].responder] := inM.hash; -- if we haven't connected before, then set it and go back to beginning if !ini[i].connectedBefore then ini[i].connectedBefore := true; ini[i].state := I_SLEEP; undefine ini[i].responderSASVoice; else ini[i].state := I_DONE; end; end; multisetremove (j,net); end; end; end; end; -- ------------------------------------------------------------------------------ -- behavior of responders -- ------------------------------------------------------------------------------ ruleset i: ResponderId do choose j: net do rule "responder reacts to initiator's M_Hello" res[i].state = R_SLEEP & net[j].dest = i & !ismember(net[j].source, ResponderId) ==> var outM: Message; -- outgoing message inM: Message; -- incoming message begin inM := net[j]; multisetremove (j,net); if inM.mType = M_Hello then -- correct message type undefine outM; outM.source := i; outM.dest := inM.zid; -- just respond to whoever spoke to you outM.mType := M_HashCommit; outM.zid := i; multisetadd (outM,net); res[i].state := R_HASH_COMMITTED; res[i].initiator := inM.zid; end; end; end; end; ruleset i: ResponderId do choose j: net do rule "responder reacts to M_DH received" res[i].state = R_HASH_COMMITTED & net[j].dest = i & !ismember(net[j].source,ResponderId) -- talk to everyone but responders ==> var outM: Message; -- outgoing message inM: Message; -- incoming message begin inM := net[j]; multisetremove (j,net); if inM.mType = M_DH then -- correct message type -- store the public value res[i].initiatorDH := inM.publicDH; undefine outM; -- if we recognize the hash, we are ready to converse, otherwise we -- commit and wait for SAS if res[i].iniSharedSecret[res[i].initiator] = inM.hash then res[i].state := R_READYTOTALK; else res[i].state := R_COMMIT; end; outM.source := i; outM.dest := res[i].initiator; outM.mType := M_DH; outM.publicDH := i; outM.hash := i; multisetadd (outM,net); end; end; end; end; ruleset i: ResponderId do choose j: net do rule "responder reacts to M_SAS received" res[i].state = R_COMMIT & net[j].dest = i & !ismember(net[j].source,ResponderId) -- talk to everyone but responders ==> var outM: Message; -- outgoing message inM: Message; -- incoming message begin inM := net[j]; multisetremove (j,net); if inM.mType = M_SAS & inM.publicDH = i & inM.privateDH = res[i].initiatorDH & (ResponderUnawareOfInitiatorsVoiceInAdvance | inM.zid = res[i].initiator) then undefine outM; outM.source := i; outM.dest := res[i].initiator; outM.mType := M_SAS; outM.publicDH := res[i].initiatorDH; outM.privateDH := i; outM.zid := i; outM.hash := i; -- we put our id in as the shared secret multisetadd (outM,net); res[i].state := R_READYTOTALK; res[i].initiatorSASVoice := inM.zid; res[i].iniSharedSecret[res[i].initiator] := inM.hash; end; end; end; end; ruleset i: ResponderId do choose j: net do rule "responder reacts to M_INIT_CONVERSATION received" res[i].state = R_READYTOTALK & net[j].dest = i & !ismember(net[j].source,ResponderId) -- talk to everyone but responders ==> var outM: Message; -- outgoing message inM: Message; -- incoming message begin inM := net[j]; multisetremove (j,net); if inM.mType = M_INIT_CONVERSATION & inM.publicDH = i & inM.privateDH = res[i].initiatorDH & (inM.zid = res[i].initiatorSASVoice | (isUndefined(res[i].initiatorSASVoice) & (ResponderForgetsVoiceBetweenSessions | inM.zid = res[i].initiatorConvVoice[res[i].initiator]))) & (ResponderUnawareOfInitiatorsVoiceInAdvance | (inM.zid = res[i].initiator & inM.hash = res[i].initiator)) then undefine outM; outM.source := i; outM.dest := res[i].initiator; outM.mType := M_RESP_CONVERSATION; outM.publicDH := res[i].initiatorDH; outM.privateDH := i; outM.zid := i; -- voice outM.hash := i; -- text of conversation outM.responseTo := inM.hash; -- text of conversation multisetadd (outM,net); res[i].initiatorConvVoice[res[i].initiator] := inM.zid; res[i].initiatorConvTextSender[res[i].initiator] := inM.hash; -- if we haven't connected before, then set it and go back to beginning if !res[i].connectedBefore then res[i].connectedBefore := true; res[i].state := R_SLEEP; undefine res[i].initiatorSASVoice; else res[i].state := R_DONE; end; end; end; end; end; -- ------------------------------------------------------------------------------ -- behavior of intruders -- ------------------------------------------------------------------------------ ruleset i: IntruderId do choose j: net do rule "intruder intercepts" !ismember (net[j].source, IntruderId) -- not for intruders' messages ==> begin alias msg: net[j] do -- message to intercept switch msg.mType case M_RESP_CONVERSATION: if msg.publicDH = i then int[i].conversationtext[net[j].hash][net[j].responseTo] := net[j].zid; end; case M_INIT_CONVERSATION: if msg.publicDH = i then int[i].conversationtext[net[j].hash][net[j].responseTo] := net[j].zid; end; end; multisetremove (j,net); end; end; end; end; ruleset i: IntruderId do ruleset k: AgentId do -- destination choose j: net do rule "intruder intercepts and forwards M_{INIT,RESP}_CONVERSATION" !ismember (net[j].source, IntruderId) -- not for intruders' messages & !ismember(k, IntruderId) -- not to intruders & (net[j].mType = M_INIT_CONVERSATION | net[j].mType = M_RESP_CONVERSATION) & net[j].publicDH = i ==> var outM: Message; begin alias inM: net[j] do -- message to intercept int[i].conversationtext[net[j].hash][net[j].responseTo] := net[j].zid; undefine outM; outM.source := i; outM.dest := k; outM.mType := inM.mType; outM.publicDH := k; outM.privateDH := i; outM.zid := inM.zid; -- voice outM.hash := inM.hash; -- text of conversation outM.responseTo := inM.responseTo; multisetremove (j,net); multisetadd (outM,net); end; end; end; end; end; ruleset i: IntruderId do -- arbitrary choice of ruleset j: AgentId do -- destination ruleset l: MessageType do -- message type ruleset z: AgentId do -- zid ruleset p: AgentId do -- publicDH rule "intruder generates M_Hello or M_HashCommit message" !ismember(j, IntruderId) & -- not to intruders (l = M_Hello | l = M_HashCommit) & -- only these cases are handled by this ruleset multisetcount (t:net, true) < NetworkSize ==> var outM: Message; begin undefine outM; outM.source := i; outM.dest := j; outM.mType := l; outM.zid := z; multisetadd (outM,net); end; end; end; end; end; end; ruleset i: IntruderId do -- arbitrary choice of ruleset j: AgentId do -- destination ruleset p: AgentId do -- publicDH rule "intruder generates M_DH message" !ismember(j, IntruderId) & -- not to intruders multisetcount (t:net, true) < NetworkSize ==> var outM: Message; begin undefine outM; outM.source := i; outM.dest := j; outM.mType := M_DH; outM.publicDH := p; outM.hash := i; multisetadd (outM,net); end; end; end; end; ruleset i: IntruderId do -- arbitrary choice of ruleset j: AgentId do -- destination ruleset p: AgentId do -- publicDH ruleset v: AgentId do -- voice rule "intruder generates M_SAS message for his own conversations" !ismember(j, IntruderId) & -- not to intruders multisetcount (t:net, true) < NetworkSize & (ismember(v, IntruderId) | (ismember(v, InitiatorId) & IntruderCanForgeInitiatorVoice) | (ismember(v, ResponderId) & IntruderCanForgeResponderVoice)) ==> var outM: Message; begin undefine outM; outM.source := i; outM.dest := j; outM.mType := M_SAS; outM.publicDH := p; outM.zid := v; outM.privateDH := i; outM.hash := i; multisetadd (outM,net); end; end; end; end; end; ruleset i: IntruderId do -- arbitrary choice of ruleset j: AgentId do -- destination rule "intruder generates M_INIT_CONVERSATION message with own voice and own text" !ismember(j, IntruderId) & -- not to intruders multisetcount (t:net, true) < NetworkSize ==> var outM: Message; begin undefine outM; outM.source := i; outM.dest := j; outM.mType := M_INIT_CONVERSATION; outM.privateDH := i; outM.publicDH := j; outM.zid := i; outM.hash := i; outM.responseTo := j; multisetadd (outM,net); end; end; end; ruleset i: IntruderId do choose j: net do rule "intruder generates message of type M_RESP_CONVERSATION in response to M_INIT_CONVERSATION" !ismember (net[j].source, IntruderId) -- not for intruders' messages & net[j].mType = M_INIT_CONVERSATION & net[j].publicDH = i ==> var outM: Message; begin alias inM: net[j] do -- message to intercept undefine outM; outM.source := i; outM.dest := inM.source; outM.mType := M_RESP_CONVERSATION; outM.publicDH := inM.source; outM.privateDH := i; outM.zid := i; -- voice outM.hash := i; -- text of conversation outM.responseTo := inM.hash; multisetremove (j,net); multisetadd (outM,net); end; end; end; end; ruleset i: IntruderId do -- arbitrary choice of ruleset j: AgentId do -- destination ruleset p: AgentId do -- text of conversation rule "intruder i generates message of type M_INIT_CONVERSATION with the information it knows, using the INTRUDER's voice" IntruderHasCourtReporters & !ismember(j, IntruderId) & -- not to intruders multisetcount (t:net, true) < NetworkSize & !isundefined(int[i].conversationtext[p][j]) ==> var outM: Message; begin undefine outM; outM.source := i; outM.dest := j; outM.mType := M_INIT_CONVERSATION; outM.privateDH := i; outM.publicDH := j; outM.zid := i; outM.hash := p; outM.responseTo := j; multisetadd (outM,net); end; end; end; end; ruleset i: IntruderId do -- arbitrary choice of ruleset j: AgentId do -- destination ruleset p: AgentId do -- text of conversation rule "intruder i generates message of type M_RESP_CONVERSATION with the information it knows, using the INTRUDER's voice" IntruderHasCourtReporters & !ismember(j, IntruderId) & -- not to intruders multisetcount (t:net, true) < NetworkSize & !isundefined(int[i].conversationtext[p][j]) ==> var outM: Message; begin undefine outM; outM.source := i; outM.dest := j; outM.mType := M_RESP_CONVERSATION; outM.privateDH := i; outM.publicDH := j; outM.zid := i; outM.hash := p; outM.responseTo := j; multisetadd (outM,net); end; end; end; end; -- ------------------------------------------------------------------------------ -- startstate -- ------------------------------------------------------------------------------ startstate -- initialize initiators undefine ini; for i: InitiatorId do ini[i].state := I_SLEEP; ini[i].responder := i; ini[i].responderDH := i; ini[i].connectedBefore := false; for j: AgentId do ini[i].resSharedSecret[j] := i; ini[i].responderConvVoice[j] := i; end; end; -- initialize responders undefine res; for i: ResponderId do res[i].state := R_SLEEP; res[i].initiator := i; res[i].initiatorDH := i; res[i].connectedBefore := false; for j: AgentId do res[i].iniSharedSecret[j] := i; res[i].initiatorConvVoice[j] := i; end; end; -- initialize intruders undefine int; for i: IntruderId do for j: AgentId do int[i].conversationtext[i][j] := i; end; end; -- initialize network undefine net; end; -- ------------------------------------------------------------------------------ -- invariants -- ------------------------------------------------------------------------------ invariant "no man in the middle attack" forall i: InitiatorId do forall j: ResponderId do forall k: IntruderId do -- if two people have initiated conversation (ini[i].state = I_DONE | (ini[i].state = I_SLEEP & ini[i].connectedBefore = true)) & (res[j].state = R_DONE | (res[j].state = R_SLEEP & res[j].connectedBefore = true)) & ini[i].responder = j & res[j].initiator = i & res[j].initiatorConvTextSender[i] = i & ini[i].responderConvTextSender[j] = j -> isundefined(int[k].conversationtext[i][j]) & isundefined(int[k].conversationtext[j][i]) end end end;