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