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