Trivial renamings (for consistency with CSFW papers)
authorpaulson
Tue Mar 25 10:43:01 1997 +0100 (1997-03-25)
changeset 2837dee1c7f1f576
parent 2836 148829646a51
child 2838 2e908f29bc3d
Trivial renamings (for consistency with CSFW papers)
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees.thy
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_AN.thy
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/OtwayRees_Bad.thy
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Tue Mar 25 10:41:44 1997 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Tue Mar 25 10:43:01 1997 +0100
     1.3 @@ -57,7 +57,7 @@
     1.4  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
     1.5  qed "OR2_analz_sees_Spy";
     1.6  
     1.7 -goal thy "!!evs. Says S B {|N, X, Crypt (shrK B) X'|} : set_of_list evs \
     1.8 +goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set_of_list evs \
     1.9  \                ==> X : analz (sees lost Spy evs)";
    1.10  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    1.11  qed "OR4_analz_sees_Spy";
    1.12 @@ -487,7 +487,7 @@
    1.13    has sent the correct message.*)
    1.14  goal thy 
    1.15   "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway lost;               \
    1.16 -\           Says S B {|NA, X, Crypt (shrK B) {|NB, Key K|}|}       \
    1.17 +\           Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|}      \
    1.18  \            : set_of_list evs;                                    \
    1.19  \           Says B Server {|NA, Agent A, Agent B, X',              \
    1.20  \                           Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
     2.1 --- a/src/HOL/Auth/OtwayRees.thy	Tue Mar 25 10:41:44 1997 +0100
     2.2 +++ b/src/HOL/Auth/OtwayRees.thy	Tue Mar 25 10:43:01 1997 +0100
     2.3 @@ -66,7 +66,7 @@
     2.4                               Crypt (shrK B)
     2.5                                     {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
     2.6                 : set_of_list evs;
     2.7 -             Says S B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
     2.8 +             Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
     2.9                 : set_of_list evs |]
    2.10            ==> Says B A {|Nonce NA, X|} # evs : otway lost"
    2.11  
     3.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Tue Mar 25 10:41:44 1997 +0100
     3.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Tue Mar 25 10:43:01 1997 +0100
     3.3 @@ -52,7 +52,7 @@
     3.4  
     3.5  (** For reasoning about the encrypted portion of messages **)
     3.6  
     3.7 -goal thy "!!evs. Says S B {|X, Crypt(shrK B) X'|} : set_of_list evs ==> \
     3.8 +goal thy "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set_of_list evs ==> \
     3.9  \                X : analz (sees lost Spy evs)";
    3.10  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    3.11  qed "OR4_analz_sees_Spy";
    3.12 @@ -353,7 +353,7 @@
    3.13    has sent the correct message in round 3.*)
    3.14  goal thy 
    3.15   "!!evs. [| B ~: lost;  evs : otway lost;                                   \
    3.16 -\           Says S B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}  \
    3.17 +\           Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
    3.18  \            : set_of_list evs |]                                           \
    3.19  \        ==> EX NA. Says Server B                                           \
    3.20  \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
     4.1 --- a/src/HOL/Auth/OtwayRees_AN.thy	Tue Mar 25 10:41:44 1997 +0100
     4.2 +++ b/src/HOL/Auth/OtwayRees_AN.thy	Tue Mar 25 10:43:01 1997 +0100
     4.3 @@ -58,7 +58,7 @@
     4.4      OR4  "[| evs: otway lost;  A ~= B;
     4.5               Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
     4.6                 : set_of_list evs;
     4.7 -             Says S B {|X, Crypt(shrK B){|Nonce NB, Agent A, Agent B, Key K|}|}
     4.8 +             Says S' B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
     4.9                 : set_of_list evs |]
    4.10            ==> Says B A X # evs : otway lost"
    4.11  
     5.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Tue Mar 25 10:41:44 1997 +0100
     5.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Tue Mar 25 10:43:01 1997 +0100
     5.3 @@ -51,7 +51,7 @@
     5.4  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
     5.5  qed "OR2_analz_sees_Spy";
     5.6  
     5.7 -goal thy "!!evs. Says S B {|N, X, Crypt (shrK B) X'|} : set_of_list evs ==> \
     5.8 +goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set_of_list evs ==> \
     5.9  \                X : analz (sees lost Spy evs)";
    5.10  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    5.11  qed "OR4_analz_sees_Spy";
     6.1 --- a/src/HOL/Auth/OtwayRees_Bad.thy	Tue Mar 25 10:41:44 1997 +0100
     6.2 +++ b/src/HOL/Auth/OtwayRees_Bad.thy	Tue Mar 25 10:43:01 1997 +0100
     6.3 @@ -63,7 +63,7 @@
     6.4      OR4  "[| evs: otway;  A ~= B;
     6.5               Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
     6.6                 : set_of_list evs;
     6.7 -             Says S B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
     6.8 +             Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
     6.9                 : set_of_list evs |]
    6.10            ==> Says B A {|Nonce NA, X|} # evs : otway"
    6.11