-------------------------------------------------------------------------------- -- -- Murphi Model of the IP Encapsulating Security Payload (ESP) protocol -- -------------------------------------------------------------------------------- -- -- version: 1.0 -- -- written by: Ulrich Stern -- date: Sep 1997 -- affiliation: Stanford University (visiting researcher), -- Technical University of Munich (PhD student) -- -------------------------------------------------------------------------------- -- -- the focus is on problems with cipher block chaining -- -- comments: -- -- - it is assumed that even if a message is sent to a user on the same -- host, this message travels over the network (which is controlled by -- the intruder). Hence, one host seems sufficient to discover the -- majority of the attacks. -- -- - the "source" and "dest" fields of a block containing data -- ("DataBlock") are used to record the true source and destination -- of this block. This info is used for detecting attacks. -- -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- -- constants, types, and variables -------------------------------------------------------------------------------- -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - const NumHosts: 1; -- number of hosts NumHonestUsers: 1; -- number of honest users NumDishonestUsers: 1; -- number of dishonest users NumBlocks: 4; -- number of blocks in message NetworkSize: 1; -- max. number of outstanding messages in network MaxMessages: 3; -- max. number of messages intruder can remember -- set one of the following flags to true to let Murphi search for the -- corresponding class of attacks E_SourceCheck: false; -- sources of header and data match E_ChosenCipher: false; -- chosen ciphertext E_Disclosure: true; -- data disclosed to wrong user -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - type HostId: scalarset (NumHosts); -- identifiers HonestUserId: scalarset (NumHonestUsers); DishonestUserId: scalarset (NumDishonestUsers); UserId: union {HonestUserId, DishonestUserId}; MessageId: scalarset (MaxMessages); BlockType : enum { DataBlock, HeaderBlock, ChosenCipher }; Block : record bType: BlockType; source: UserId; dest: UserId; decryptable: boolean; -- block might become undecryptable due to cut -- and paste operations end; -- remark: possibly add counter to allow for different blocks for the -- same pair of users Plainmessage : array[1..NumBlocks-1] of Block; -- header block is -- generated by host Ciphermessage : record source: HostId; -- source and dest fields also encode the key dest: HostId; -- used (host-pair keying) blocks: array[1..NumBlocks] of Block; fromInt: boolean; -- indicate whether message is from intruder end; Intruder : record messages: array[MessageId] of Ciphermessage; -- known messages end; -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - var -- state variables for net: multiset[NetworkSize] of Ciphermessage; -- network int: Intruder; -- intruders -------------------------------------------------------------------------------- -- procedures and functions -------------------------------------------------------------------------------- -- generate cipermessage and send it procedure SendMessage (u: UserId; i: HostId; v: UserId; j: HostId; m: Plainmessage); var outM: Ciphermessage; begin outM.source := i; outM.dest := j; -- generate header outM.blocks[1].bType := HeaderBlock; outM.blocks[1].source := u; outM.blocks[1].dest := v; outM.blocks[1].decryptable := true; -- set remaining blocks for k := 2 to NumBlocks do outM.blocks[k] := m[k-1]; outM.blocks[k].decryptable := true; end; outM.fromInt := false; multisetadd (outM,net); end; -------------------------------------------------------------------------------- -- rules -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- -- behavior of honest users -- honest user u on host i sends message to user v on host j ruleset u: HonestUserId; v: UserId; i: HostId; j: HostId do rule "honest user sends message" multisetcount (l:net, true) < NetworkSize ==> var msg: Plainmessage; begin undefine msg; for k := 1 to NumBlocks-1 do msg[k].bType := DataBlock; msg[k].source := u; msg[k].dest := v; end; SendMessage (u,i,v,j,msg); end; end; -- honest user receives message choose j: net do rule "honest user receives message" net[j].fromInt -- every message goes through intruder ==> begin alias msg: net[j] do -- check if decryption possible -- remark: not modeled since host addresses also encode the used key -- check if message is for honest user -- remark: header is assumed to be always decryptable (IV is sent -- unencrypted) if ismember(msg.blocks[1].dest, HonestUserId) then -- check if blocks were created by user who is source in header if E_SourceCheck then for k := 2 to NumBlocks do if msg.blocks[k].decryptable & msg.blocks[k].bType = DataBlock & msg.blocks[k].source != msg.blocks[1].source then error "header and data not from same source"; end; end; end; -- delete message multisetremove (j,net); end; end; end; end; -------------------------------------------------------------------------------- -- behavior of dishonest users -- dishonest user u1 on host i1 sends message to user v1 on host j1 -- it is assumed that the dishonest user can also generate a fake -- headers in the first data block ruleset u1: DishonestUserId; v1: UserId; i: HostId; j: HostId do ruleset u2: UserId; v2: UserId do rule "dishonest user sends message" multisetcount (l:net, true) < NetworkSize ==> var msg: Plainmessage; begin undefine msg; -- fake header msg[1].bType := HeaderBlock; msg[1].source := u2; msg[1].dest := v2; for k := 2 to NumBlocks-1 do msg[k].bType := DataBlock; msg[k].source := u1; msg[k].dest := v1; end; SendMessage (u1,i,v1,j,msg); end; end; end; -- dishonest user receives message choose j: net do rule "dishonest user receives message" net[j].fromInt ==> begin alias msg: net[j] do -- check if decryption possible -- remark: not modeled since host addresses also encode the used key -- check if message is for dishonest user if ismember(msg.blocks[1].dest, DishonestUserId) then -- check if there is block with chosen ciphertext -- remark: intruder knows previous cipherblock when he inserts -- ChosenCipher block if E_ChosenCipher then for k := 2 to NumBlocks do if msg.blocks[k].decryptable & msg.blocks[k].bType = ChosenCipher then error "chosen ciphertext attack"; end; end; end; -- check if dishonest user gets data that it should not have gotten if E_Disclosure then for k := 2 to NumBlocks do if msg.blocks[k].decryptable & msg.blocks[k].bType = DataBlock & msg.blocks[k].dest != msg.blocks[1].dest & ismember(msg.blocks[k].source, HonestUserId) then error "data disclosed to dishonest user"; end; end; end; -- delete message multisetremove (j,net); end; end; end; end; -------------------------------------------------------------------------------- -- behavior of intruders -- intruder intercepts and learns choose j: net do ruleset a: MessageId do rule "intruder intercepts and learns" !net[j].fromInt & isundefined(int.messages[a].blocks[1].bType) ==> var found: boolean; begin alias msg: net[j] do -- check if message is already there found := false; for i: MessageId do if !isundefined(int.messages[i].blocks[1].bType) then if int.messages[i].source = msg.source & int.messages[i].dest = msg.dest & forall k := 1 to NumBlocks do int.messages[i].blocks[k].bType = msg.blocks[k].bType & int.messages[i].blocks[k].source = msg.blocks[k].source & int.messages[i].blocks[k].dest = msg.blocks[k].dest end then found := true; end; end; end; -- add message -- remark: decryptable should be true for all blocks if !found then int.messages[a] := msg; end; -- delete message multisetremove (j,net); end; end; end; end; -- intruder generates message using cut and paste -- it is assumed here that the intruder picks two messages that -- have the same source and destination fields, and also uses the -- values of these fields in the generated message (otherwise the -- corresponding blocks could not be decrypted) -- intruder may also insert chosen ciphertext ruleset i: MessageId do -- first message ruleset j: MessageId do -- second message ruleset k: 0..NumBlocks-1 do -- cut after this block in first msg ruleset cc: boolean; p: 2..NumBlocks do -- insert chosen cipertext at -- position p rule "intruder generates message" !isundefined(int.messages[i].blocks[1].bType) & !isundefined(int.messages[j].blocks[1].bType) & int.messages[i].source = int.messages[j].source & int.messages[i].dest = int.messages[j].dest & multisetcount (t:net, true) < NetworkSize ==> var outM: Ciphermessage; begin undefine outM; outM.source := int.messages[i].source; outM.dest := int.messages[i].dest; -- cut and paste blocks -- assumes the interesting part of a message is always in the -- first blocks for l := 1 to k do outM.blocks[l] := int.messages[i].blocks[l]; end; for l := k+1 to NumBlocks do outM.blocks[l] := int.messages[j].blocks[l-k]; end; -- check if block becomes undecryptable after cut -- simplification: it is not modeled that if messages i and j are -- identical in the first k blocks, then the (k+1)st -- block is decryptable if i != j & k != 0 then outM.blocks[k+1].decryptable := false; end; -- insert chosen ciphertext if cc then undefine outM.blocks[p]; outM.blocks[p].bType := ChosenCipher; outM.blocks[p].decryptable := true; end; outM.fromInt := true; -- send message multisetadd (outM,net); end; end; end; end; end; -------------------------------------------------------------------------------- -- startstate -------------------------------------------------------------------------------- startstate -- initialize intruders undefine int; -- initialize network undefine net; end; -------------------------------------------------------------------------------- -- invariants -------------------------------------------------------------------------------- -- not needed thus far