47 {|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|}, |
47 {|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|}, |
48 Crypt (shrK B) {|Agent A, Key KAB|}|} |
48 Crypt (shrK B) {|Agent A, Key KAB|}|} |
49 # evs3 : yahalom" |
49 # evs3 : yahalom" |
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. The premise |
|
53 A ~= Server is needed to prove Says_Server_message_form.*) |
53 YM4 "[| evs4: yahalom; A ~= Server; |
54 YM4 "[| evs4: yahalom; A ~= Server; |
54 Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, |
55 Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, |
55 X|} : set evs4; |
56 X|} : set evs4; |
56 Says A B {|Agent A, Nonce NA|} : set evs4 |] |
57 Says A B {|Agent A, Nonce NA|} : set evs4 |] |
57 ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 : yahalom" |
58 ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 : yahalom" |