-------------------------------------------------------------------------------- -- -- Murphi Model of the XML-Security -- -------------------------------------------------------------------------------- -- -- version: 1.0 -- -- written by: Jun Yoshida -- date: March 2004 -- affiliation: Stanford University (visiting scholar from Hitachi) -- -------------------------------------------------------------------------------- -- -- only the following four steps of the protocol are modeled: -- -- A->B: {E1}PKb, {SSKa}PKb -- B->A: {E2}PKa, {SSKb}PKa -- A->B: {E3}SSKb -- B->A: {E4}SSKa -- -- A: Client, B: Server -- Ex: XML elements, PKx: public key, SSKx: shared secret key -- -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- -- constants, types and variables -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- const NumClients: 1; NumServers: 1; NumIntruders: 1; NetworkSize: 1; MaxKeys: 10; -------------------------------------------------------------------------------- type ClientId: scalarset (NumClients); ServerId: scalarset (NumServers); IntruderId: scalarset (NumIntruders); AgentId: union {ClientId, ServerId, IntruderId}; -------------------------------------------------------------------------------- -- messages MessageType : enum { -- different types of messages M_PK, -- public key based messages M_SSK -- shared secret key based messages }; SharedSecretKeyId: 1..MaxKeys; Message: record source: AgentId; -- source of message dest: AgentId; -- intended destination of message mType: MessageType; element1: AgentId; -- encrypted XML elements enKey1_1: AgentId; -- public key for encryption enKey1_2: SharedSecretKeyId; -- shared secret key for encryption element2: SharedSecretKeyId; -- encrypted shared secret key enKey2: AgentId; -- public key for encryption end; -------------------------------------------------------------------------------- -- client ClientStatus : enum { C_SLEEP, C_WAIT_PK_MESSAGE, C_WAIT_SSK_MESSAGE, C_DONE }; Client : record state: ClientStatus; server: AgentId; -- server which client wants to contact cSSK: SharedSecretKeyId; -- shared secret key for client sSSK: SharedSecretKeyId; -- shared secret key for server end; -------------------------------------------------------------------------------- -- server ServerStatus : enum { S_SLEEP, S_COMMIT_PK_MESSAGE, S_COMMIT_SSK_MESSAGE }; Server : record state: ServerStatus; client: AgentId; cSSK: SharedSecretKeyId; -- shared secret key for client sSSK: SharedSecretKeyId; -- shared secret key for server end; -------------------------------------------------------------------------------- -- intruder Intruder : record elements: array[AgentId] of boolean; -- known XML elements keys: array[SharedSecretKeyId] of boolean; -- known shared secret keys end; -------------------------------------------------------------------------------- var -- state variables for net: multiset[NetworkSize] of Message; -- network cli: array[ClientId] of Client; -- clients ser: array[ServerId] of Server; -- servers int: array[IntruderId] of Intruder; -- intruders nextKey: SharedSecretKeyId; -- next shared secret key -------------------------------------------------------------------------------- -- procedures and functions -------------------------------------------------------------------------------- -- generate next shared secret key function GenSharedSecretKey(): SharedSecretKeyId; var r: SharedSecretKeyId; begin if isundefined(nextKey) then error "out of shared secret keys"; end; r := nextKey; if nextKey = MaxKeys then undefine nextKey; else nextKey := nextKey + 1; end; return r; end; -------------------------------------------------------------------------------- -- rules -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- -- behavior of clients -------------------------------------------------------------------------------- -- Client i sends a public key based message to Server j ruleset i: ClientId do ruleset j: ServerId do rule "client sends pk based message to server" cli[i].state = C_SLEEP & multisetcount (l:net, true) < NetworkSize ==> var outM: Message; -- outgoing message cSSK: SharedSecretKeyId; -- shared secret key for client begin cSSK := GenSharedSecretKey(); undefine outM; outM.source := i; outM.dest := j; outM.mType := M_PK; outM.element1 := i; outM.enKey1_1 := j; outM.element2 := cSSK; outM.enKey2 := j; multisetadd (outM, net); cli[i].state := C_WAIT_PK_MESSAGE; cli[i].server := j; cli[i].cSSK := cSSK; end; end; end; -- Client i sends a shared secret key based message to Server ruleset i: ClientId do choose j: net do rule "client sends sk based message to server" cli[i].state = C_WAIT_PK_MESSAGE & net[j].dest = i ==> var outM: Message; -- outgoing message inM: Message; -- incoming message sSSK: SharedSecretKeyId; -- shared secret key for Server begin inM := net[j]; multisetremove (j, net); if inM.mType = M_PK then if inM.enKey1_1 = i & inM.enKey2 = i then sSSK := inM.element2; undefine outM; outM.source := i; outM.dest := cli[i].server; outM.mType := M_SSK; outM.element1 := i; outM.enKey1_2 := sSSK; multisetadd (outM, net); cli[i].state := C_WAIT_SSK_MESSAGE; cli[i].sSSK := sSSK; else --error "client received incorrect pk message" end; end; end; end; end; -- Client i receives a shared secret key based message from Server ruleset i: ClientId do choose j: net do rule "client receives ssk based message from server" cli[i].state = C_WAIT_SSK_MESSAGE & net[j].dest = i ==> var inM: Message; -- incoming message begin inM := net[j]; multisetremove (j, net); if inM.mType = M_SSK then if inM.enKey1_2 = cli[i].cSSK then cli[i].state := C_DONE; else --error "client received incorrect ssk message" end; end; end; end; end; -------------------------------------------------------------------------------- -- behavior of servers -------------------------------------------------------------------------------- -- Server i receives a public key based message from Client ruleset i: ServerId do choose j: net do rule "server receives pk based message from client" ser[i].state = S_SLEEP & net[j].dest = i ==> var outM: Message; -- outgoing message inM: Message; -- incoming message cSSK: SharedSecretKeyId; -- shared secret key for Client sSSK: SharedSecretKeyId; -- shared secret key for Server begin inM := net[j]; multisetremove (j, net); if inM.mType = M_PK then if inM.enKey1_1 = i & inM.enKey2 = i then sSSK := GenSharedSecretKey(); cSSK := inM.element2; undefine outM; outM.source := i; outM.dest := inM.source; outM.mType := M_PK; outM.element1 := i; outM.enKey1_1 := inM.source; outM.element2 := sSSK; outM.enKey2 := inM.source; multisetadd (outM,net); ser[i].state := S_COMMIT_PK_MESSAGE; ser[i].client := inM.source; ser[i].cSSK := cSSK; ser[i].sSSK := sSSK; else --error "server received incorrect pk message" end; end; end; end; end; -- Server i receives a shared secret key based message from Client ruleset i: ServerId do choose j: net do rule "server receives sk based message from client" ser[i].state = S_COMMIT_PK_MESSAGE & net[j].dest = i ==> var outM: Message; -- outgoing message inM: Message; -- incoming message begin inM := net[j]; multisetremove (j, net); if inM.mType = M_SSK then if inM.enKey1_2 = ser[i].sSSK then undefine outM; outM.source := i; outM.dest := inM.source; outM.mType := M_SSK; outM.element1 := i; outM.enKey1_2 := ser[i].cSSK; multisetadd (outM, net); ser[i].state := S_COMMIT_SSK_MESSAGE; else --error "server received incorrect ssk message" end; 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 intruder's message ==> begin alias msg: net[j] do -- message to overhear/intercept -- learn public key based messages if msg.mType = M_PK then if msg.enKey1_1 = i then int[i].elements[msg.element1] := true; end; if msg.enKey2 = i then int[i].keys[msg.element2] := true; end; end; -- learn shared secret key based messages if msg.mType = M_SSK & int[i].keys[msg.enKey1_2] = true then int[i].elements[msg.element1] := true; end; end; end; end; end; end; -- generate key, change message ruleset i: IntruderId do choose j: net do ruleset intercept : boolean do rule "intruder overhears/intercepts and alter ssk" !ismember(net[j].source, IntruderId) -- not for intruder's message ==> var iSSK: SharedSecretKeyId; -- shared secret key for intruder begin alias msg: net[j] do -- message to overhear/intercept if msg.mType = M_PK then iSSK := GenSharedSecretKey(); msg.element2 := iSSK; int[i].keys[iSSK] := true; end; end; end; end; end; end; -------------------------------------------------------------------------------- -- startstate -------------------------------------------------------------------------------- startstate -- initialize clients undefine cli; for i: ClientId do cli[i].state := C_SLEEP; end; -- initialize servers undefine ser; for i: ServerId do ser[i].state := S_SLEEP; end; -- initialize intruders undefine int; for i: IntruderId do for j: AgentId do int[i].elements[j] := false; end; for j: SharedSecretKeyId do int[i].keys[j] := false; end; end; -- initialize network undefine net; -- initialize shared secret key generator nextKey := 1; end; -------------------------------------------------------------------------------- -- invariants -------------------------------------------------------------------------------- invariant "client secrecy" forall i: ClientId do ismember(cli[i].server, ServerId) -> forall j: IntruderId do int[j].elements[i] = false end end; invariant "server secrecy" forall i: ServerId do ismember(ser[i].client, ClientId) -> forall j: IntruderId do int[j].elements[i] = false end end;