-------------------------------------------------------------------------------- -- -- Murphi Model of the octopus protocol -- -------------------------------------------------------------------------------- -- -------------------------------------------------------------------------------- -- -- Here, we model the case where we assume that the diffie-hellman -- key exchange works and analyze the interactions between 1 core -- member and its connected peer(s). -- Authentication information is supposed to be present before the -- start of this protocol, but it does not provide a method to use -- this information. We would like to see what way this information -- can be intergrated into the messages to ensure security. -- -- A: core-member, B: connecting peer -- -------------------------------------------------------------------------------- -- We assume -- * standard (Dolev-Yao) attacker model for this analysis -- * there has been a round of authentication before the start of this key -- exchange, and also a round to decide who will be a part of the core. -- * each peer knows exactly which core member it should talk to. -- * Later on we would like to analyze the methods of forming cores. -- Attacks and revisions: -- -- 1. Since there is no identity information, the first attack is simple, -- in which the attacker can pose as a peer and participate in the protocol -- on behalf of another protocol. So the first step is to put in the identity -- information in the messages. -- -- 2. Only putting in identity information obviously did not work. We need to -- be able to prove that the person who is sending the information is the -- person he claims to be. To do this let us add some authentication information -- that we have to assume. Since the protocol assumes everyone knows who the -- peers are, we can assume that they have some kind of public key, known to -- all the other peers. So lets add secure messages from the peer side. -- -- 3. This is still a problem, because the intruder can still masquerade as a core -- member as there is no way for the core to prove to the peer that the message -- really a message from the core. To handle this let us assume that the core -- also sends along with the reply the actual DH element that the peer had sent -- it. Also we must assume that the peer DH is sent encrypted over the secure -- channel built earlier. -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - const NumPeers: 2; -- number of connecting peers NumCore: 1; -- number of members in the core -- standard parameters for a Dolev Yao intruder NumIntruders: 1; -- number of intruders NetworkSize: 1; -- max. number of outstanding messages in network MaxKnowledge: 10; -- max. number of messages intruder can remember -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - type PeerId: scalarset (NumPeers); CoreId: scalarset (NumCore); IntruderId: scalarset (NumIntruders); AgentId: union {PeerId, CoreId, IntruderId}; ValidAgentId: union {PeerId, CoreId}; keyType: array[ValidAgentId] of AgentId; keyType_V: array[ValidAgentId] of boolean; MessageType : enum { -- different types of messages M_PeerKeyPart, -- the part of the DH key from the peer M_CoreKeyPart -- the part of the DH key after core-exchange }; Message : record source: AgentId; -- source of message dest: AgentId; -- intended destination of message mType: MessageType; -- type of message key_1: ValidAgentId; -- key used to encrypt the message fromId: ValidAgentId; -- sender information fromId_E: ValidAgentId; -- sender information encrypted useKey: ValidAgentId; -- sender key to use toId: AgentId; -- recepient DH_Key_V: keyType_V; --array[ValidAgentId] of boolean; DH_Key: keyType; --array[ValidAgentId] of AgentId; DH_Key_P: AgentId; -- key generated ny peer; replayedAs : array[ValidAgentId] of boolean; end; -- the core member will return the DH_1 part in the return message to -- identify what it thinks the whole key is PeerStates : enum { P_READY, -- intially (ready to send DH part1) P_WAIT, -- waiting for key from core P_GOTKEY -- got some message containing the key }; Peer : record state: PeerStates; keyMaterial_V: keyType_V; --array[ValidAgentId] of boolean; keyMaterial: keyType; --array[ValidAgentId] of AgentId; end; CoreMainStates: enum { C_RECEIVING, C_SENDING, C_MAINDONE }; CoreStates : enum { C_WAIT, -- waiting for key material from peer C_GOTKEY, -- sending the key material back to peer C_DONE -- done sending }; Core : record mainState: CoreMainStates; state: array[ValidAgentId] of CoreStates; keyMaterial_V: keyType_V; --array[ValidAgentId] of boolean; keyMaterial: keyType; --array[ValidAgentId] of AgentId; end; Intruder : record messages: multiset[MaxKnowledge] of Message; -- known messages end; -- Note that it is fairly obvious in this scenario that the intruder -- would not be able to guess the secret from the network messages. -- Hence we will not check that case in the intruder model, nor will we -- put in actions that are specifically meant to passively decipher the -- shared secret. -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - var -- state variables for net: multiset[NetworkSize] of Message; -- network peer: array[PeerId] of Peer; -- peers core: array[CoreId] of Core; -- core members int: array[IntruderId] of Intruder; -- intruders -------------------------------------------------------------------------------- -- rules -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- -- behavior of peers -------------------------------------------------------------------------------- -- peer i starts protocol with core member j ruleset i: PeerId do ruleset j: CoreId do rule 20 "peer sends DH key material" peer[i].state = P_READY & multisetcount (l:net, true) < NetworkSize ==> var outM: Message; -- outgoing message begin undefine outM; peer[i].keyMaterial_V[i] := true; peer[i].keyMaterial[i] := i; outM.source := i; outM.dest := j; outM.mType := M_PeerKeyPart; outM.key_1 := j; -- use the core's public key. outM.DH_Key_P := peer[i].keyMaterial[i]; outM.fromId := i; outM.fromId_E := i; outM.toId := j; multisetadd (outM,net); peer[i].state := P_WAIT; end; end; end; -- peer receives key material from core member ruleset i: PeerId do choose j: net do rule 20 "peer receives key material" peer[i].state = P_WAIT & net[j].dest = i & ismember(net[j].source, IntruderId) & -- valid optimization as the attacker is a powerful Dolev Yao attacker ismember(net[j].fromId, CoreId) & -- must be a message from a known core net[j].mType = M_CoreKeyPart -- must be a message from a known core ==> var inM: Message; -- incoming message begin inM := net[j]; multisetremove (j,net); if inM.mType = M_CoreKeyPart then -- correct message type for k: ValidAgentId do if inM.DH_Key_V[k] = true then peer[i].keyMaterial_V[k] := true; peer[i].keyMaterial[k] := inM.DH_Key[k]; endif; endfor; peer[i].state := P_GOTKEY; end; end; end; end; -------------------------------------------------------------------------------- -- behavior of core -- core member i receives key material ruleset i: CoreId do choose j: net do rule 120 "core receives key material" core[i].mainState = C_RECEIVING & ismember(net[j].fromId, PeerId) & -- ensure this message is from a valid peer core[i].state[net[j].fromId] = C_WAIT & -- hasnt seen this message before net[j].dest = i & -- is destined for the core ismember(net[j].source,IntruderId) & -- is replayed net[j].key_1 = i & -- is encrypted using core's key net[j].mType = M_PeerKeyPart & true ==> var inM: Message; -- incoming message begin inM := net[j]; if inM.toId = i then if inM.fromId = inM.fromId_E then multisetremove (j,net); core[i].keyMaterial_V[inM.fromId] := true; core[i].keyMaterial[inM.fromId] := inM.DH_Key_P; core[i].state[inM.fromId] := C_GOTKEY; endif endif; end; endchoose; endruleset; ----------------------- -- core got messages from all the nodes and can now exchange keys ----------------------- ruleset i: CoreId do rule 90 "core switches state to send all keys" forall k:PeerId do core[i].state[k] = C_GOTKEY endforall & true ==> begin core[i].mainState := C_SENDING end endruleset; ----------------------- -- send message to all peers about the shared key ----------------------- ruleset i: CoreId do ruleset j: PeerId do rule 90 "Core sending out keys" core[i].mainState = C_SENDING & core[i].state[j] = C_GOTKEY & multisetcount (l:net, true) < NetworkSize ==> var outM: Message; begin outM.source := i; outM.dest := j; outM.mType := M_CoreKeyPart; outM.key_1 := j; -- no key for k:ValidAgentId do outM.DH_Key_V[k] := false; if k != j then if core[i].keyMaterial_V[k] = true then outM.DH_Key_V[k] := true; outM.DH_Key[k] := core[i].keyMaterial[k]; endif; endif; endfor; outM.fromId := i; outM.toId := j; multisetadd (outM,net); core[i].state[j] := C_DONE; end; endruleset; endruleset; -- if all messages sent, set the main state to C_MAINDONE ruleset i:CoreId do rule 90 "Core done sending all messages" core[i].mainState = C_SENDING & forall k:PeerId do core[i].state[k] = C_DONE endforall ==> begin core[i].mainState := C_MAINDONE end; endruleset; -------------------------------------------------------------------------------- -- behavior of intruder -- intruder i intercepts messages -- let us make the intruder remember the whole message that it -- intercepted and then later send all the messages that the -- intruder can generate from this message. ruleset i: IntruderId do choose j: net do rule 10 "intruder intercepts" !ismember (net[j].source, IntruderId) & -- not an intruder's message --ismember(net[j].toId, PeerId) true ==> var temp: Message; begin temp := net[j]; temp.source := i; for k:ValidAgentId do temp.replayedAs[k] := false; endfor; multisetadd(temp, int[i].messages); multisetremove (j,net); end; endchoose; endruleset; --end; -- intruder replays messages that it knows ruleset i: IntruderId do choose j: int[i].messages do ruleset k: ValidAgentId do rule 90 "intruder replays learnt message" multisetcount (l:net, true) < NetworkSize & int[i].messages[j].replayedAs[k] = false & true ==> var temp: Message; outM: Message; begin undefine outM; outM := int[i].messages[j]; if outM.mType = M_PeerKeyPart then outM.fromId := k; endif; if outM.mType = M_CoreKeyPart then -- nothing is visible so only replay endif; multisetadd(outM, net); int[i].messages[j].replayedAs[k] := true; end; endruleset; endchoose; endruleset; -------------------------------------------------------------------------------- -- startstate -------------------------------------------------------------------------------- startstate -- initialize peers undefine peer; for i: PeerId do peer[i].state := P_READY; for j: ValidAgentId do peer[i].keyMaterial_V[j] := false; endfor; peer[i].keyMaterial_V[i] := true; peer[i].keyMaterial[i] := i; end; -- initialize core members undefine core; for i: CoreId do core[i].mainState := C_RECEIVING; for j: PeerId do core[i].state[j] := C_WAIT; endfor; for j: ValidAgentId do core[i].keyMaterial_V[j] := false; endfor; core[i].keyMaterial_V[i] := true; core[i].keyMaterial[i] := i; 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 "key agreement" forall i: CoreId do core[i].mainState = C_MAINDONE -> forall j: PeerId do forall k:PeerId do (peer[j].state = P_GOTKEY & peer[k].state = P_GOTKEY) -> forall l:ValidAgentId do peer[j].keyMaterial_V[l] = peer[j].keyMaterial_V[l] & (peer[j].keyMaterial_V[l] = true -> peer[j].keyMaterial[l] = peer[k].keyMaterial[l] ) endforall endforall endforall endforall;