equal
deleted
inserted
replaced
53 Crypt (shrK B) {|Nonce NB, Key KAB, Agent A|}|} |
53 Crypt (shrK B) {|Nonce NB, Key KAB, Agent A|}|} |
54 # evs : yahalom lost" |
54 # evs : yahalom lost" |
55 |
55 |
56 (*Alice receives the Server's (?) message, checks her Nonce, and |
56 (*Alice receives the Server's (?) message, checks her Nonce, and |
57 uses the new session key to send Bob his Nonce.*) |
57 uses the new session key to send Bob his Nonce.*) |
58 YM4 "[| evs: yahalom lost; A ~= Server; A ~= B; |
58 YM4 "[| evs: yahalom lost; A ~= Server; |
59 Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, |
59 Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, |
60 X|} : set evs; |
60 X|} : set evs; |
61 Says A B {|Agent A, Nonce NA|} : set evs |] |
61 Says A B {|Agent A, Nonce NA|} : set evs |] |
62 ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom lost" |
62 ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom lost" |
63 |
63 |