--- a/src/HOL/Auth/WooLam.thy Tue Jul 01 17:37:42 1997 +0200
+++ b/src/HOL/Auth/WooLam.thy Tue Jul 01 17:38:49 1997 +0200
@@ -42,7 +42,7 @@
(*Alice responds to Bob's challenge by encrypting NB with her key.
B is *not* properly determined -- Alice essentially broadcasts
her reply.*)
- WL3 "[| evs: woolam; A ~= B;
+ WL3 "[| evs: woolam;
Says A B (Agent A) : set evs;
Says B' A (Nonce NB) : set evs |]
==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam"
--- a/src/HOL/Auth/Yahalom.thy Tue Jul 01 17:37:42 1997 +0200
+++ b/src/HOL/Auth/Yahalom.thy Tue Jul 01 17:38:49 1997 +0200
@@ -50,7 +50,7 @@
(*Alice receives the Server's (?) message, checks her Nonce, and
uses the new session key to send Bob his Nonce.*)
- YM4 "[| evs: yahalom lost; A ~= Server; A ~= B;
+ YM4 "[| evs: yahalom lost; A ~= Server;
Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
X|} : set evs;
Says A B {|Agent A, Nonce NA|} : set evs |]
--- a/src/HOL/Auth/Yahalom2.thy Tue Jul 01 17:37:42 1997 +0200
+++ b/src/HOL/Auth/Yahalom2.thy Tue Jul 01 17:38:49 1997 +0200
@@ -55,7 +55,7 @@
(*Alice receives the Server's (?) message, checks her Nonce, and
uses the new session key to send Bob his Nonce.*)
- YM4 "[| evs: yahalom lost; A ~= Server; A ~= B;
+ YM4 "[| evs: yahalom lost; A ~= Server;
Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
X|} : set evs;
Says A B {|Agent A, Nonce NA|} : set evs |]