equal
deleted
inserted
replaced
57 X|} |
57 X|} |
58 : set_of_list evs; |
58 : set_of_list evs; |
59 Says A B {|Agent A, Nonce NA|} : set_of_list evs |] |
59 Says A B {|Agent A, Nonce NA|} : set_of_list evs |] |
60 ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom lost" |
60 ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom lost" |
61 |
61 |
|
62 (*This message models possible leaks of session keys. The Nonces |
|
63 identify the protocol run.*) |
|
64 Revl "[| evs: yahalom lost; A ~= Spy; |
|
65 Says S A {|Crypt {|Agent B, Key K, Nonce NA, Nonce NB|} (shrK A), |
|
66 X|} |
|
67 : set_of_list evs |] |
|
68 ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost" |
|
69 |
62 end |
70 end |