--- a/src/HOL/Auth/OtwayRees.ML Tue Mar 25 10:41:44 1997 +0100
+++ b/src/HOL/Auth/OtwayRees.ML Tue Mar 25 10:43:01 1997 +0100
@@ -57,7 +57,7 @@
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
qed "OR2_analz_sees_Spy";
-goal thy "!!evs. Says S B {|N, X, Crypt (shrK B) X'|} : set_of_list evs \
+goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set_of_list evs \
\ ==> X : analz (sees lost Spy evs)";
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
qed "OR4_analz_sees_Spy";
@@ -487,7 +487,7 @@
has sent the correct message.*)
goal thy
"!!evs. [| B ~: lost; B ~= Spy; evs : otway lost; \
-\ Says S B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \
+\ Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \
\ : set_of_list evs; \
\ Says B Server {|NA, Agent A, Agent B, X', \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
--- a/src/HOL/Auth/OtwayRees.thy Tue Mar 25 10:41:44 1997 +0100
+++ b/src/HOL/Auth/OtwayRees.thy Tue Mar 25 10:43:01 1997 +0100
@@ -66,7 +66,7 @@
Crypt (shrK B)
{|Nonce NA, Nonce NB, Agent A, Agent B|}|}
: set_of_list evs;
- Says S B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
+ Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
: set_of_list evs |]
==> Says B A {|Nonce NA, X|} # evs : otway lost"
--- a/src/HOL/Auth/OtwayRees_AN.ML Tue Mar 25 10:41:44 1997 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML Tue Mar 25 10:43:01 1997 +0100
@@ -52,7 +52,7 @@
(** For reasoning about the encrypted portion of messages **)
-goal thy "!!evs. Says S B {|X, Crypt(shrK B) X'|} : set_of_list evs ==> \
+goal thy "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set_of_list evs ==> \
\ X : analz (sees lost Spy evs)";
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
qed "OR4_analz_sees_Spy";
@@ -353,7 +353,7 @@
has sent the correct message in round 3.*)
goal thy
"!!evs. [| B ~: lost; evs : otway lost; \
-\ Says S B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
+\ Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
\ : set_of_list evs |] \
\ ==> EX NA. Says Server B \
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
--- a/src/HOL/Auth/OtwayRees_AN.thy Tue Mar 25 10:41:44 1997 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.thy Tue Mar 25 10:43:01 1997 +0100
@@ -58,7 +58,7 @@
OR4 "[| evs: otway lost; A ~= B;
Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
: set_of_list evs;
- Says S B {|X, Crypt(shrK B){|Nonce NB, Agent A, Agent B, Key K|}|}
+ Says S' B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
: set_of_list evs |]
==> Says B A X # evs : otway lost"
--- a/src/HOL/Auth/OtwayRees_Bad.ML Tue Mar 25 10:41:44 1997 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Tue Mar 25 10:43:01 1997 +0100
@@ -51,7 +51,7 @@
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
qed "OR2_analz_sees_Spy";
-goal thy "!!evs. Says S B {|N, X, Crypt (shrK B) X'|} : set_of_list evs ==> \
+goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set_of_list evs ==> \
\ X : analz (sees lost Spy evs)";
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
qed "OR4_analz_sees_Spy";
--- a/src/HOL/Auth/OtwayRees_Bad.thy Tue Mar 25 10:41:44 1997 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.thy Tue Mar 25 10:43:01 1997 +0100
@@ -63,7 +63,7 @@
OR4 "[| evs: otway; A ~= B;
Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
: set_of_list evs;
- Says S B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
+ Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
: set_of_list evs |]
==> Says B A {|Nonce NA, X|} # evs : otway"