tamarin-prover-0.8.4.0: data/examples/ake/dh/UM_three_pass_combined_fixed.spthy
theory UM_three_pass_combined
begin
/*
The three-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
*/
builtins: diffie-hellman, hashing, multiset
functions: MAC/2, first/1, second/1, concat/2
equations: concat(first(x), second(x)) = x
/* 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
/* UM3 Initiator */
// UM3 session creation for initiator:
// choose ephemeral private key, compute ephemeral public key X, and send
rule I_Activate:
let X = 'g'^~ex // the ephemeral public key
sid = <'UM3', $A, $B, X> // the session id is unique
in
[ Fr( ~ex ) ] // select random ephemeral private key
--[ Activate( sid )
, Sid( sid )
, Agents($A,$B) ]-> // 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
, Out( X ) // send message
]
// UM3 session update for initiator:
// receive key confirmation and Y, compute key, check key confirmation.
rule I_Complete:
let X = 'g'^~ex // recompute X
pB = 'g'^~eb // we do not model key registration by adversary,
// hence key always of this form
kstring = h(Y^~ex, pB^~ea, $A, $B, X, Y, 'UM3') // we do not include the public string Lambda
key = second(kstring)
conf = MAC(first(kstring), <'R', $B, $A, Y, X>) // we do not include Lambda_1
confB = MAC(first(kstring), <'I', $A, $B, X, Y>) // we do not include Lambda_2
sidOld = <'UM3',$A, $B, <'1',X>>
sid = <'UM3',$A, $B, <'1',X> + <'2', <Y,confB>> + <'3', conf> > // new sid
in
[ I_Act( ~ex, $A, $B ) // this session was activated
, In( <Y, confB> )
, !Ltk( $A, ~ea ) // lookup own longterm private key
, !Pk( $B, pB ) ] // lookup peer's public key
--[ Complete( sid, 'I', key ) // sid is 'Complete'd after this step
, SidUpdated( sidOld )
, Sid( sid ) ]->
[ I_Comp( sid ) // state of this session
, Out( conf )
, !SessionKey( sid, $A, key ) ] // the session key of sid with actor $A, available
// for reveals
// UM3 session expiration
rule I_Expire:
[ I_Comp( sid ) ]
--[ Expire( sid ) ]-> // sid is expired after this step
[ ]
/* UM3_Responder */
// Session creation:
rule R_Activate:
let pA = 'g'^~ea // we do not model key registration by adversary,
// hence key always of this form
Y = 'g'^~ey
kstring = h(X^~ey, pA^~eb, $A, $B, X, Y, 'UM3')
key = second(kstring)
conf = MAC(first(kstring), <'I', $A, $B, X, Y>) // we do not include Lambda_2
sid = <'UM3', $B, $A, <'1',X> + <'2',<Y, conf>> > // sid is unique
in
[ Fr( ~ey )
, In( X )
, !Ltk( $B, ~eb )
, !Pk( $A, pA ) ]
--[ Activate(sid)
, Sid( sid )
, Agents($A,$B) ]->
[ Out( <Y,conf>)
, R_Act( ~ey, $B, $A, X )
, !SessionState( sid, $A, ~ey )
]
// Session update:
rule R_Complete:
let pA = 'g'^~ea
Y = 'g'^~ey
kstring = h(X^~ey, pA^~eb, $A, $B, X, Y, 'UM3' )
key = second(kstring)
confA = MAC(first(kstring), <'R', $B, $A, Y, X>) // we do not include Lambda_1
conf = MAC(first(kstring), <'I', $A, $B, X, Y>) // we do not include Lambda_2
sidOld = <'UM3', $B, $A, <'1',X> + <'2', <Y, conf>>> // sid is unique
sid = <'UM3', $B, $A, <'1',X> + <'2', <Y, conf>> + <'3', confA> > // sid is unique
in
[ R_Act( ~ey, $B, $A, X )
, In( confA )
, !Ltk( $B, ~eb )
, !Pk( $A, pA )
]
--[ Complete( sid, 'R', key ) // sid is 'Complete'd after this step
, SidUpdated( sidOld )
, Sid( sid ) ]->
[ R_Comp( sid )
, !SessionKey( sid, $B, key ) ] // the session key of sid with actor $B, available
// for reveals
rule R_Expire:
[ R_Comp( sid ) ]
--[ Expire( sid ) ]->
[ ]
/* UM1 Initiator */
// We prefix all facts with UM1
// Activate the session: choose ephemeral private key, compute ephemeral public key X.
rule UM1_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
--[ UM1_Activate( sid ) ]-> // sid is 'Activate'd after this step
[ UM1_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 UM1_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, X, pB, 'UM1') // we do not include the public string
in
[ UM1_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
--[ UM1_Complete( sid, 'I', k ) ]-> // sid is 'Complete'd after this step
[ UM1_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 UM1_I_Expire:
[ UM1_I_Comp( sid ) ]
--[ UM1_Expire( sid ) ]-> // sid is expired after this step
[ ]
/* UM1 Responder */
// R has no Activated state since there is no ephemeral key.
rule UM1_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, X, 'g'^~eb, 'UM1' )
in
[ In( X )
, !Ltk( $B, ~eb )
, !Pk( $A, pA ) ]
--[ UM1_Activate(sid)
, UM1_Complete( sid, 'R', k )
]-> // sid is 'Complete'd and 'Activate'd after this step
[ UM1_R_Comp( sid )
, !SessionKey( sid, $B, k )
]
rule UM1_R_Expire:
[ UM1_R_Comp( sid ) ]
--[ UM1_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. UM1_Activate(sid) @ i & UM1_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"
// this assumption is used in the proof. Without this restriction, a completed
// session with actor and peer A is its own matching session.
axiom actor_ineq_peer:
"not (Ex #i A. Agents(A,A) @ i)"
// 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_UM3:
"(All #i #j role A B k s comm.
/* The key of a complete session 's' is known */
Complete( <'UM3',A,B,comm> , role, k ) @ i & K( k ) @ j & s = <'UM3',A,B,comm>
/* then one of the following must have happened */
==>
/* 1. (a) The session key of s was revealed (see 4. for 1. (b)) */
(Ex #k. SessionKeyReveal( s ) @ k)
/* 2. Corrupt(A) before Expire(s) */
| (Ex #k. Corrupt(A) @ k &
( not (Ex #l. Expire(s) @ l & l < k)))
/* 3. SessionStateReveal(s) and either Corrupt(A) or Corrupt(B) */
| (Ex #k. SessionStateReveal(s) @ k
& ((Ex #l. Corrupt(A) @ l) | (Ex #l. Corrupt(B) @ l)))
/* 4. s* exists and */
| (Ex #l ms matchingComm.
Sid(<'UM3',B,A,matchingComm>) @ l
& ms = <'UM3',B,A,matchingComm>
& ((Ex rest. matchingComm + rest = comm) | matchingComm = comm)
// the session has not been updated
& not (Ex #v. SidUpdated(ms) @ v)
& (
/* SessionKeyReveal(s*) (see 1. (b)) */
(Ex #k. SessionKeyReveal( ms ) @ k)
/* (a) Corrupt(B) before Expire(s*) */
| (Ex #k. Corrupt(B) @ k &
(not (Ex #l. Expire(ms) @ l & l < k)))
/* (b) SessionStateReveal(s*) and either Corrupt(A) or Corrupt(B) */
| (Ex #k. SessionStateReveal(ms) @ k
& ((Ex #l. Corrupt(A) @ l) | (Ex #l. Corrupt(B) @ l)))))
/* 5. s* does not exist and Corrupt(B) before Expire(s) */
| ((not (Ex #l matchingComm.
Sid(<'UM3',B,A,matchingComm>) @ l
& ((Ex rest. matchingComm + rest = comm) | matchingComm = comm)
// the session has not been updated
& not (Ex #v. SidUpdated(<'UM3',B,A,matchingComm>) @ v)))
& (Ex #k. Corrupt(B) @ k &
(not (Ex #l. Expire(s) @ l & l < k)))))"
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') */
UM1_Complete( <A,B,X> , role, k ) @ i & K( k ) @ j & s = <A,B,X> & sp = <B,A,X>
/* 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_. UM1_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_ . UM1_Complete( sp, 'I', k_) @ k))
/* there is corrupt B */
& (Ex #k. Corrupt(B) @ k))))"
end