equal
deleted
inserted
replaced
73 the true senders in order to make them accurate.*) |
73 the true senders in order to make them accurate.*) |
74 Oops "[| evso: ns_shared; A ~= Spy; |
74 Oops "[| evso: ns_shared; A ~= Spy; |
75 Says B A (Crypt K (Nonce NB)) : set evso; |
75 Says B A (Crypt K (Nonce NB)) : set evso; |
76 Says Server A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) |
76 Says Server A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) |
77 : set evso |] |
77 : set evso |] |
78 ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evso : ns_shared" |
78 ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : ns_shared" |
79 |
79 |
80 end |
80 end |