theory UM_one_pass_fix begin /* The one-pass UM protocol. See "Combined Security Analysis of the One- and Three-Pass Unified Model Key Agreement Protocols" Sanjit Chatterjee, Alfred Menezes and Berkant Ustaoglu There is a flaw in the definition of the model and the proof. The problem is that the session id does not contain the role and since this is a one-pass protocol, this means that a responder session can match another responder session if X is replayed. We therefore adapt the definition of clean in the paper as follows. We change 3. A is the responder and one of the following holds: (a) M issued Corrupt(A) (b) s* exists and M issued either Corrupt(B) before Expire(s*) or both Corrupt(B) and SessionStateReveal(s*) (c) s* does not exist and M issued CORRUPT( B ). To 3. A is the responder and one of the following holds: (a) M issued Corrupt(A) (b) _An initiator session_ s* exists and M issued either Corrupt(B) before Expire(s*) or both Corrupt(B) and SessionStateReveal(s*) (c) _No initiator session_ s* exists and M issued CORRUPT( B ). */ builtins: diffie-hellman, hashing /* Key registration */ rule Register_key_honest: let pkA = 'g'^~ea in [ Fr( ~ea ) // select random longterm private ] --[ KeyReg( $A ) ]-> // a key for A has been registered [ !Ltk( $A, ~ea ) // ~ea is the longterm private key of A , !Pk( $A, pkA ) // pkA = 'g'^~ea is the longterm public key of A , Out( pkA ) ] // the adversary can learn the public key /* Initiator */ // Activate the session: choose ephemeral private key, compute ephemeral public key X. rule I_Activate: let X = 'g'^~ex // the ephemeral public key sid = <$A, $B, X> // the session id, not unique because there might // be responder session with actor B and peer A // which receives X in [ Fr( ~ex ) ] // select random ephemeral private key --[ Activate( sid ) ]-> // sid is 'Activate'd after this step [ I_Act( ~ex, $A, $B ) // the state of this session, identified by ex (unique) , !SessionState( sid, $A, ~ex ) // the session state of sid with actor $A consists only of ex, // available for reveals ] // Complete the session: send X, and compute key. rule I_Complete: let X = 'g'^~ex // recompute X sid = <$A, $B, X> // recompute sid pB = 'g'^~eb // we do not model key registration by adversary, // hence key always of this form k = h(pB^~ex, pB^~ea, $A, $B) // we do not include the public string in [ I_Act( ~ex, $A, $B ) // this session was activated , !Ltk( $A, ~ea ) // lookup own longterm private key , !Pk( $B, pB ) ] // lookup peer's public key --[ Complete( sid, 'I', k ) ]-> // sid is 'Complete'd after this step [ I_Comp( sid ) // state of this session , Out( <$B, $A, X> ) // send message , !SessionKey( sid, $A, k ) ] // the session key of sid with actor $A, available // for reveals // Expire the session rule I_Expire: [ I_Comp( sid ) ] --[ Expire( sid ) ]-> // sid is expired after this step [ ] /* Responder */ // R has no Activated state since there is no ephemeral key. rule R_Complete: let pA = 'g'^~ea // we do not model key registration by adversary, // hence key always of this form sid = <$B, $A, X> // sid is not unique because of initiator sessions with // same sid and replay k = h(X^~eb, pA^~eb, $A, $B ) in [ In( X ) , !Ltk( $B, ~eb ) , !Pk( $A, pA ) ] --[ Activate(sid), Complete( sid, 'R', k ) ]-> // sid is 'Complete'd and 'Activate'd after this step [ R_Comp( sid ) , !SessionKey( sid, $B, k ) ] rule R_Expire: [ R_Comp( sid ) ] --[ Expire( sid ) ]-> // sid is expired after this step [ ] /* Corrupt an agent: We model corruption by three different rules. We do not model static key selection for corrupted agents. */ // Corrupt and obtain longterm key rule Corrupt_Ltk: [ !Ltk( $A, ~ea ) ] --[ Corrupt( $A ) ]-> [ Out( ~ea ) ] // Corrupt and obtain session state. Must occur before complete which // we ensure with BeforeComplete action and axiom. rule Corrupt_SessionState: [ !SessionState( sid, ~x, $A ) ] --[ Corrupt( $A ), BeforeComplete( sid ) ]-> [ Out( ~x ) ] // Corrupt and obtain session key. Must occur before expire which // we ensure with BeforeExpire action and axiom. rule Corrupt_SessionKey: [ !SessionKey( sid, $A, k ) ] --[ Corrupt( $A ), BeforeExpire( sid ) ]-> [ Out( k ) ] /* Reveals for session state and session key */ rule Reveal_SessionState: [ !SessionState( sid, ~x, $A ) ] --[SessionStateReveal( sid ), BeforeComplete( sid ) ]-> [ Out( ~x ) ] rule Reveal_SessionKey: [ !SessionKey( sid, $A, k) ] --[ SessionKeyReveal( sid ), BeforeExpire( sid ) ]-> [ Out( k ) ] /* We only consider traces which satisfy these axioms */ // we enforce unique sids since the paper states that "At any point in time a session is // in exactly one of the following states: active, completed, aborted, expired." axiom sid_unique: "All #i #j sid. Activate(sid) @ i & Activate(sid) @ j ==> #i = #j" // every agent has at most one registered key axiom keyreg_unique: "All #i #j A. KeyReg(A) @ i & KeyReg(A) @ j ==> #i = #j" // The reveals and the corrupt rules that reveal session state and session key are not performed // too late. axiom corrupt_and_reveal_not_too_early: " (All #i #j s role_ k_. BeforeComplete( s ) @ i & Complete(s, role_, k_ ) @ j ==> #i < #j) & (All #i #j s. BeforeExpire( s ) @ i & Expire( s ) @ j ==> #i < #j)" // Key agreement for initiator and responder is reachable without any adversary interaction. lemma key_agreement_reachable: exists-trace "Ex #i #j sid sidm k. Complete( sid , 'I', k ) @ i & Complete( sidm, 'R', k ) @ j & (not (Ex #j C. Corrupt( C ) @ j)) & (not (Ex #j s. SessionKeyReveal( s ) @ j)) & (not (Ex #j s. SessionStateReveal( s ) @ j))" lemma CK_secure: "(All #i #j role A B X k s sp. /* The key of a complete session 's' is known (whose partner is 'sp') */ Complete( , role, k ) @ i & K( k ) @ j & s = & sp = /* then one of the following must have happened */ ==> /* 1. (a) The session key of s was revealed */ (Ex #k. SessionKeyReveal( s ) @ k) /* (b) the session key of some s* was revealed */ | (Ex #i1. SessionKeyReveal( sp ) @ i1) | (/* 2. s is an initiator session */ (role = 'I') & ( /* (a) A was corrupted before expire*/ (Ex #k. Corrupt(A) @ k & ( (Ex #l. Expire(s) @ l & k < l) | not (Ex #l. Expire(s) @ l ))) | /* (b) A was corrupted and s's session state was revealed */ (Ex #k #l. SessionStateReveal(s) @ k & Corrupt(A) @ l) | /* (c) B was corrupted */ (Ex #k. Corrupt(B) @ k ))) | (/* 2. s is a responder session */ (role = 'R') & ( /* (a) A was corrupted */ Ex #k. Corrupt(A) @ k ) | /* (b) There is a matching initiator session and */ (Ex #k k_. Complete( sp, 'I', k_ ) @ k /* there is a corrupt B before expire s* */ & ( (Ex #k. Corrupt(B) @ k & ( (Ex #l. Expire(sp) @ l & k < l) | not (Ex #l. Expire(sp) @ l ))) /* or both session state reveal s* and corrupt B */ | (Ex #k #l. SessionStateReveal(sp) @ k & Corrupt(B) @ l ))) | /* (c) There is no matching initiator session and */ ( (not (Ex #k k_ . Complete( sp, 'I', k_) @ k)) /* there is corrupt B */ & (Ex #k. Corrupt(B) @ k))))" end