50 Crypt {|Agent A, Key (newK evs)|} (shrK B)|} |
50 Crypt {|Agent A, Key (newK evs)|} (shrK B)|} |
51 # evs : yahalom lost" |
51 # evs : yahalom lost" |
52 |
52 |
53 (*Alice receives the Server's (?) message, checks her Nonce, and |
53 (*Alice receives the Server's (?) message, checks her Nonce, and |
54 uses the new session key to send Bob his Nonce.*) |
54 uses the new session key to send Bob his Nonce.*) |
55 YM4 "[| evs: yahalom lost; A ~= B; |
55 YM4 "[| evs: yahalom lost; A ~= Server; A ~= B; |
56 Says S A {|Crypt {|Agent B, Key K, Nonce NA, Nonce NB|} (shrK A), |
56 Says S A {|Crypt {|Agent B, Key K, Nonce NA, Nonce NB|} (shrK A), |
57 X|} |
57 X|} : set_of_list evs; |
58 : set_of_list evs; |
|
59 Says A B {|Agent A, Nonce NA|} : set_of_list evs |] |
58 Says A B {|Agent A, Nonce NA|} : set_of_list evs |] |
60 ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom lost" |
59 ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom lost" |
61 |
60 |
62 (*This message models possible leaks of session keys. The Nonces |
61 (*This message models possible leaks of session keys. The Nonces |
63 identify the protocol run.*) |
62 identify the protocol run.*) |
64 Revl "[| evs: yahalom lost; A ~= Spy; |
63 Oops "[| evs: yahalom lost; A ~= Spy; |
65 Says S A {|Crypt {|Agent B, Key K, Nonce NA, Nonce NB|} (shrK A), |
64 Says Server A {|Crypt {|Agent B, Key K, Nonce NA, Nonce NB|} |
66 X|} |
65 (shrK A), |
67 : set_of_list evs |] |
66 X|} : set_of_list evs |] |
68 ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost" |
67 ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost" |
69 |
68 |
70 end |
69 end |