--- a/src/HOL/Auth/Yahalom2.thy Mon Jun 22 15:50:59 1998 +0200
+++ b/src/HOL/Auth/Yahalom2.thy Mon Jun 22 15:53:24 1998 +0200
@@ -42,7 +42,7 @@
(*The Server receives Bob's message. He responds by sending a
new session key to Alice, with a certificate for forwarding to Bob.
- Fields are reversed in the 2nd certificate to prevent attacks!! *)
+ Both agents are quoted in the 2nd certificate to prevent attacks!*)
YM3 "[| evs3: yahalom; A ~= B; A ~= Server; Key KAB ~: used evs3;
Says B' Server {|Agent B, Nonce NB,
Crypt (shrK B) {|Agent A, Nonce NA|}|}
@@ -50,7 +50,7 @@
==> Says Server A
{|Nonce NB,
Crypt (shrK A) {|Agent B, Key KAB, Nonce NA|},
- Crypt (shrK B) {|Nonce NB, Key KAB, Agent A|}|}
+ Crypt (shrK B) {|Agent A, Agent B, Key KAB, Nonce NB|}|}
# evs3 : yahalom"
(*Alice receives the Server's (?) message, checks her Nonce, and