Expressed most Oops rules using Notes instead of Says, and other tidying
authorpaulson
Thu Jan 08 18:10:34 1998 +0100 (1998-01-08)
changeset 45374e835bd9fada
parent 4536 74f7c556fd90
child 4538 0f40d6e7897d
Expressed most Oops rules using Notes instead of Says, and other tidying
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/NS_Shared.thy
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
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom.thy
src/HOL/Auth/Yahalom2.ML
src/HOL/Auth/Yahalom2.thy
     1.1 --- a/src/HOL/Auth/NS_Shared.ML	Thu Jan 08 18:09:47 1998 +0100
     1.2 +++ b/src/HOL/Auth/NS_Shared.ML	Thu Jan 08 18:10:34 1998 +0100
     1.3 @@ -258,7 +258,7 @@
     1.4  \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
     1.5  \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
     1.6  \             : set evs -->                                            \
     1.7 -\        (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs) -->         \
     1.8 +\        (ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs) -->          \
     1.9  \        Key K ~: analz (spies evs)";
    1.10  by (etac ns_shared.induct 1);
    1.11  by analz_spies_tac;
    1.12 @@ -288,7 +288,7 @@
    1.13  goal thy 
    1.14   "!!evs. [| Says Server A                                        \
    1.15  \              (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;   \
    1.16 -\           ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs;     \
    1.17 +\           ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs;      \
    1.18  \           A ~: bad;  B ~: bad;  evs : ns_shared                \
    1.19  \        |] ==> Key K ~: analz (spies evs)";
    1.20  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
    1.21 @@ -345,7 +345,7 @@
    1.22  goal thy
    1.23   "!!evs. [| Crypt K (Nonce NB) : parts (spies evs);                   \
    1.24  \           Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
    1.25 -\           ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs;          \
    1.26 +\           ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs;           \
    1.27  \           A ~: bad;  B ~: bad;  evs : ns_shared |]                  \
    1.28  \        ==> Says B A (Crypt K (Nonce NB)) : set evs";
    1.29  by (blast_tac (claset() addSIs [A_trusts_NS2, A_trusts_NS4_lemma]
    1.30 @@ -415,7 +415,7 @@
    1.31   "!!evs. [| Crypt K {|Nonce NB, Nonce NB|} : parts (spies evs);      \
    1.32  \           Says B A (Crypt K (Nonce NB))  : set evs;                \
    1.33  \           Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs);   \
    1.34 -\           ALL NA NB. Says A Spy {|NA, NB, Key K|} ~: set evs;      \
    1.35 +\           ALL NA NB. Notes Spy {|NA, NB, Key K|} ~: set evs;       \
    1.36  \           A ~: bad;  B ~: bad;  evs : ns_shared |]                 \
    1.37  \        ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) : set evs";
    1.38  by (dtac B_trusts_NS3 1);
     2.1 --- a/src/HOL/Auth/NS_Shared.thy	Thu Jan 08 18:09:47 1998 +0100
     2.2 +++ b/src/HOL/Auth/NS_Shared.thy	Thu Jan 08 18:10:34 1998 +0100
     2.3 @@ -75,6 +75,6 @@
     2.4               Says B A (Crypt K (Nonce NB)) : set evso;
     2.5               Says Server A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
     2.6                 : set evso |]
     2.7 -          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evso : ns_shared"
     2.8 +          ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : ns_shared"
     2.9  
    2.10  end
     3.1 --- a/src/HOL/Auth/OtwayRees.ML	Thu Jan 08 18:09:47 1998 +0100
     3.2 +++ b/src/HOL/Auth/OtwayRees.ML	Thu Jan 08 18:10:34 1998 +0100
     3.3 @@ -60,15 +60,10 @@
     3.4  qed "OR4_analz_spies";
     3.5  
     3.6  goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
     3.7 -\                 ==> K : parts (spies evs)";
     3.8 +\                ==> K : parts (spies evs)";
     3.9  by (Blast_tac 1);
    3.10  qed "Oops_parts_spies";
    3.11  
    3.12 -(*OR2_analz... and OR4_analz... let us treat those cases using the same 
    3.13 -  argument as for the Fake case.  This is possible for most, but not all,
    3.14 -  proofs: Fake does not invent new nonces (as in OR2), and of course Fake
    3.15 -  messages originate from the Spy. *)
    3.16 -
    3.17  bind_thm ("OR2_parts_spies",
    3.18            OR2_analz_spies RS (impOfSubs analz_subset_parts));
    3.19  bind_thm ("OR4_parts_spies",
    3.20 @@ -86,8 +81,7 @@
    3.21  (** Theorems of the form X ~: parts (spies evs) imply that NOBODY
    3.22      sends messages containing X! **)
    3.23  
    3.24 -
    3.25 -(*Spy never sees another agent's shared key! (unless it's bad at start)*)
    3.26 +(*Spy never sees a good agent's shared key!*)
    3.27  goal thy 
    3.28   "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    3.29  by (parts_induct_tac 1);
    3.30 @@ -111,6 +105,7 @@
    3.31  by (parts_induct_tac 1);
    3.32  (*Fake*)
    3.33  by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
    3.34 +(*OR2, OR3*)
    3.35  by (ALLGOALS Blast_tac);
    3.36  qed_spec_mp "new_keys_not_used";
    3.37  
    3.38 @@ -141,8 +136,7 @@
    3.39  val analz_spies_tac = 
    3.40      dtac OR2_analz_spies 4 THEN 
    3.41      dtac OR4_analz_spies 6 THEN
    3.42 -    forward_tac [Says_Server_message_form] 7 THEN
    3.43 -    assume_tac 7 THEN
    3.44 +    forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN
    3.45      REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
    3.46  
    3.47  
    3.48 @@ -194,7 +188,7 @@
    3.49  by (ALLGOALS Clarify_tac);
    3.50  (*Remaining cases: OR3 and OR4*)
    3.51  by (ex_strip_tac 2);
    3.52 -by (Best_tac 2);
    3.53 +by (Best_tac 2);	(*Blast_tac's too slow (in reconstruction)*)
    3.54  by (expand_case_tac "K = ?y" 1);
    3.55  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
    3.56  (*...we assume X is a recent message, and handle this case by contradiction*)
    3.57 @@ -315,11 +309,11 @@
    3.58      the premises, e.g. by having A=Spy **)
    3.59  
    3.60  goal thy 
    3.61 - "!!evs. [| A ~: bad;  B ~: bad;  evs : otway |]                    \
    3.62 + "!!evs. [| A ~: bad;  B ~: bad;  evs : otway |]                      \
    3.63  \        ==> Says Server B                                            \
    3.64  \              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
    3.65  \                Crypt (shrK B) {|NB, Key K|}|} : set evs -->         \
    3.66 -\            Says B Spy {|NA, NB, Key K|} ~: set evs -->              \
    3.67 +\            Notes Spy {|NA, NB, Key K|} ~: set evs -->               \
    3.68  \            Key K ~: analz (spies evs)";
    3.69  by (etac otway.induct 1);
    3.70  by analz_spies_tac;
    3.71 @@ -341,8 +335,8 @@
    3.72   "!!evs. [| Says Server B                                           \
    3.73  \            {|NA, Crypt (shrK A) {|NA, Key K|},                    \
    3.74  \                  Crypt (shrK B) {|NB, Key K|}|} : set evs;        \
    3.75 -\           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
    3.76 -\           A ~: bad;  B ~: bad;  evs : otway |]                  \
    3.77 +\           Notes Spy {|NA, NB, Key K|} ~: set evs;                 \
    3.78 +\           A ~: bad;  B ~: bad;  evs : otway |]                    \
    3.79  \        ==> Key K ~: analz (spies evs)";
    3.80  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
    3.81  by (blast_tac (claset() addSEs [lemma]) 1);
     4.1 --- a/src/HOL/Auth/OtwayRees.thy	Thu Jan 08 18:09:47 1998 +0100
     4.2 +++ b/src/HOL/Auth/OtwayRees.thy	Thu Jan 08 18:10:34 1998 +0100
     4.3 @@ -75,6 +75,6 @@
     4.4      Oops "[| evso: otway;  B ~= Spy;
     4.5               Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
     4.6                 : set evso |]
     4.7 -          ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
     4.8 +          ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
     4.9  
    4.10  end
     5.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Thu Jan 08 18:09:47 1998 +0100
     5.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Thu Jan 08 18:10:34 1998 +0100
     5.3 @@ -58,10 +58,6 @@
     5.4  by (Blast_tac 1);
     5.5  qed "Oops_parts_spies";
     5.6  
     5.7 -(*OR4_analz_spies lets us treat those cases using the same 
     5.8 -  argument as for the Fake case.  This is possible for most, but not all,
     5.9 -  proofs, since Fake messages originate from the Spy. *)
    5.10 -
    5.11  bind_thm ("OR4_parts_spies",
    5.12            OR4_analz_spies RS (impOfSubs analz_subset_parts));
    5.13  
    5.14 @@ -76,7 +72,7 @@
    5.15  (** Theorems of the form X ~: parts (spies evs) imply that NOBODY
    5.16      sends messages containing X! **)
    5.17  
    5.18 -(*Spy never sees another agent's shared key! (unless it's bad at start)*)
    5.19 +(*Spy never sees a good agent's shared key!*)
    5.20  goal thy 
    5.21   "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    5.22  by (parts_induct_tac 1);
    5.23 @@ -248,12 +244,12 @@
    5.24      the premises, e.g. by having A=Spy **)
    5.25  
    5.26  goal thy 
    5.27 - "!!evs. [| A ~: bad;  B ~: bad;  evs : otway |]                 \
    5.28 + "!!evs. [| A ~: bad;  B ~: bad;  evs : otway |]                   \
    5.29  \        ==> Says Server B                                         \
    5.30  \             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
    5.31  \               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
    5.32  \            : set evs -->                                         \
    5.33 -\            Says B Spy {|NA, NB, Key K|} ~: set evs -->           \
    5.34 +\            Notes Spy {|NA, NB, Key K|} ~: set evs -->            \
    5.35  \            Key K ~: analz (spies evs)";
    5.36  by (etac otway.induct 1);
    5.37  by analz_spies_tac;
    5.38 @@ -276,8 +272,8 @@
    5.39  \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
    5.40  \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
    5.41  \             : set evs;                                            \
    5.42 -\           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
    5.43 -\           A ~: bad;  B ~: bad;  evs : otway |]                  \
    5.44 +\           Notes Spy {|NA, NB, Key K|} ~: set evs;                 \
    5.45 +\           A ~: bad;  B ~: bad;  evs : otway |]                    \
    5.46  \        ==> Key K ~: analz (spies evs)";
    5.47  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
    5.48  by (blast_tac (claset() addSEs [lemma]) 1);
     6.1 --- a/src/HOL/Auth/OtwayRees_AN.thy	Thu Jan 08 18:09:47 1998 +0100
     6.2 +++ b/src/HOL/Auth/OtwayRees_AN.thy	Thu Jan 08 18:10:34 1998 +0100
     6.3 @@ -68,6 +68,6 @@
     6.4                        {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}, 
     6.5                          Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|}
     6.6                 : set evso |]
     6.7 -          ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
     6.8 +          ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
     6.9  
    6.10  end
     7.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Thu Jan 08 18:09:47 1998 +0100
     7.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Thu Jan 08 18:10:34 1998 +0100
     7.3 @@ -20,6 +20,10 @@
     7.4  set proof_timing;
     7.5  HOL_quantifiers := false;
     7.6  
     7.7 +AddEs spies_partsEs;
     7.8 +AddDs [impOfSubs analz_subset_parts];
     7.9 +AddDs [impOfSubs Fake_parts_insert];
    7.10 +
    7.11  
    7.12  (*A "possibility property": there are traces that reach the end*)
    7.13  goal thy 
    7.14 @@ -46,26 +50,23 @@
    7.15  
    7.16  (** For reasoning about the encrypted portion of messages **)
    7.17  
    7.18 -goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs ==> \
    7.19 -\                X : analz (spies evs)";
    7.20 -by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
    7.21 +goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs \
    7.22 +\                ==> X : analz (spies evs)";
    7.23 +by (dtac (Says_imp_spies RS analz.Inj) 1);
    7.24 +by (Blast_tac 1);
    7.25  qed "OR2_analz_spies";
    7.26  
    7.27 -goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs ==> \
    7.28 -\                X : analz (spies evs)";
    7.29 -by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
    7.30 +goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
    7.31 +\                ==> X : analz (spies evs)";
    7.32 +by (dtac (Says_imp_spies RS analz.Inj) 1);
    7.33 +by (Blast_tac 1);
    7.34  qed "OR4_analz_spies";
    7.35  
    7.36  goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
    7.37 -\                 ==> K : parts (spies evs)";
    7.38 -by (blast_tac (claset() addSEs spies_partsEs) 1);
    7.39 +\                ==> K : parts (spies evs)";
    7.40 +by (Blast_tac 1);
    7.41  qed "Oops_parts_spies";
    7.42  
    7.43 -(*OR2_analz... and OR4_analz... let us treat those cases using the same 
    7.44 -  argument as for the Fake case.  This is possible for most, but not all,
    7.45 -  proofs: Fake does not invent new nonces (as in OR2), and of course Fake
    7.46 -  messages originate from the Spy. *)
    7.47 -
    7.48  bind_thm ("OR2_parts_spies",
    7.49            OR2_analz_spies RS (impOfSubs analz_subset_parts));
    7.50  bind_thm ("OR4_parts_spies",
    7.51 @@ -83,11 +84,10 @@
    7.52  (** Theorems of the form X ~: parts (spies evs) imply that NOBODY
    7.53      sends messages containing X! **)
    7.54  
    7.55 -(*Spy never sees another agent's shared key! (unless it's bad at start)*)
    7.56 +(*Spy never sees a good agent's shared key!*)
    7.57  goal thy 
    7.58   "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    7.59  by (parts_induct_tac 1);
    7.60 -by (Fake_parts_insert_tac 1);
    7.61  by (ALLGOALS Blast_tac);
    7.62  qed "Spy_see_shrK";
    7.63  Addsimps [Spy_see_shrK];
    7.64 @@ -108,7 +108,7 @@
    7.65  by (parts_induct_tac 1);
    7.66  (*Fake*)
    7.67  by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
    7.68 -(*OR1-3*)
    7.69 +(*OR2, OR3*)
    7.70  by (ALLGOALS Blast_tac);
    7.71  qed_spec_mp "new_keys_not_used";
    7.72  
    7.73 @@ -125,14 +125,13 @@
    7.74  (*Describes the form of K and NA when the Server sends this message.  Also
    7.75    for Oops case.*)
    7.76  goal thy 
    7.77 - "!!evs. [| Says Server B                                                 \
    7.78 -\            {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;           \
    7.79 -\           evs : otway |]                                                \
    7.80 + "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
    7.81 +\           evs : otway |]                                           \
    7.82  \     ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
    7.83  by (etac rev_mp 1);
    7.84  by (etac otway.induct 1);
    7.85 -by (prove_simple_subgoals_tac 1);
    7.86 -by (Blast_tac 1); 
    7.87 +by (ALLGOALS Simp_tac);
    7.88 +by (ALLGOALS Blast_tac);
    7.89  qed "Says_Server_message_form";
    7.90  
    7.91  
    7.92 @@ -140,7 +139,7 @@
    7.93  val analz_spies_tac = 
    7.94      dtac OR2_analz_spies 4 THEN 
    7.95      dtac OR4_analz_spies 6 THEN
    7.96 -    forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN 
    7.97 +    forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN
    7.98      REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
    7.99  
   7.100  
   7.101 @@ -192,12 +191,11 @@
   7.102  by (ALLGOALS Clarify_tac);
   7.103  (*Remaining cases: OR3 and OR4*)
   7.104  by (ex_strip_tac 2);
   7.105 -by (Blast_tac 2);
   7.106 +by (Best_tac 2);	(*Blast_tac's too slow (in reconstruction)*)
   7.107  by (expand_case_tac "K = ?y" 1);
   7.108  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   7.109  (*...we assume X is a recent message, and handle this case by contradiction*)
   7.110 -by (blast_tac (claset() addSEs spies_partsEs
   7.111 -                      delrules [conjI]    (*no split-up to 4 subgoals*)) 1);
   7.112 +by (blast_tac (claset() addSEs spies_partsEs) 1);
   7.113  val lemma = result();
   7.114  
   7.115  goal thy 
   7.116 @@ -208,37 +206,39 @@
   7.117  qed "unique_session_keys";
   7.118  
   7.119  
   7.120 -(*Crucial security property, but not itself enough to guarantee correctness!*)
   7.121 +(** Crucial secrecy property: Spy does not see the keys sent in msg OR3
   7.122 +    Does not in itself guarantee security: an attack could violate 
   7.123 +    the premises, e.g. by having A=Spy **)
   7.124 +
   7.125  goal thy 
   7.126 - "!!evs. [| A ~: bad;  B ~: bad;  evs : otway |]                    \
   7.127 + "!!evs. [| A ~: bad;  B ~: bad;  evs : otway |]                      \
   7.128  \        ==> Says Server B                                            \
   7.129  \              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   7.130  \                Crypt (shrK B) {|NB, Key K|}|} : set evs -->         \
   7.131 -\            Says B Spy {|NA, NB, Key K|} ~: set evs -->              \
   7.132 +\            Notes Spy {|NA, NB, Key K|} ~: set evs -->               \
   7.133  \            Key K ~: analz (spies evs)";
   7.134  by (etac otway.induct 1);
   7.135  by analz_spies_tac;
   7.136  by (ALLGOALS
   7.137      (asm_simp_tac (simpset() addcongs [conj_cong] 
   7.138 -                            addsimps [analz_insert_eq, analz_insert_freshK]
   7.139 -                            addsimps (pushes@expand_ifs))));
   7.140 +                             addsimps [analz_insert_eq, analz_insert_freshK]
   7.141 +                             addsimps (pushes@expand_ifs))));
   7.142  (*Oops*)
   7.143  by (blast_tac (claset() addSDs [unique_session_keys]) 4);
   7.144  (*OR4*) 
   7.145  by (Blast_tac 3);
   7.146  (*OR3*)
   7.147 -by (blast_tac (claset() addSEs spies_partsEs
   7.148 -                       addIs [impOfSubs analz_subset_parts]) 2);
   7.149 +by (Blast_tac 2);
   7.150  (*Fake*) 
   7.151  by (spy_analz_tac 1);
   7.152  val lemma = result() RS mp RS mp RSN(2,rev_notE);
   7.153  
   7.154  goal thy 
   7.155 - "!!evs. [| Says Server B                                         \
   7.156 -\            {|NA, Crypt (shrK A) {|NA, Key K|},                  \
   7.157 -\                  Crypt (shrK B) {|NB, Key K|}|} : set evs;      \
   7.158 -\           Says B Spy {|NA, NB, Key K|} ~: set evs;              \
   7.159 -\           A ~: bad;  B ~: bad;  evs : otway |]                \
   7.160 + "!!evs. [| Says Server B                                           \
   7.161 +\            {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   7.162 +\                  Crypt (shrK B) {|NB, Key K|}|} : set evs;        \
   7.163 +\           Notes Spy {|NA, NB, Key K|} ~: set evs;                 \
   7.164 +\           A ~: bad;  B ~: bad;  evs : otway |]                    \
   7.165  \        ==> Key K ~: analz (spies evs)";
   7.166  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   7.167  by (blast_tac (claset() addSEs [lemma]) 1);
   7.168 @@ -257,8 +257,7 @@
   7.169  \            Says A B {|NA, Agent A, Agent B,                  \
   7.170  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  : set evs";
   7.171  by (parts_induct_tac 1);
   7.172 -by (Fake_parts_insert_tac 1);
   7.173 -by (Blast_tac 1);
   7.174 +by (ALLGOALS Blast_tac);
   7.175  qed_spec_mp "Crypt_imp_OR1";
   7.176  
   7.177  
   7.178 @@ -277,16 +276,15 @@
   7.179  \                   Crypt (shrK A) {|NA, Key K|},                    \
   7.180  \                   Crypt (shrK B) {|NB, Key K|}|}  : set evs)";
   7.181  by (parts_induct_tac 1);
   7.182 -by (Fake_parts_insert_tac 1);
   7.183 +(*Fake*)
   7.184 +by (Blast_tac 1);
   7.185  (*OR1: it cannot be a new Nonce, contradiction.*)
   7.186 -by (blast_tac (claset() addSIs [parts_insertI]
   7.187 -                       addSEs spies_partsEs) 1);
   7.188 +by (Blast_tac 1);
   7.189  (*OR3 and OR4*)
   7.190  by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
   7.191  by (ALLGOALS Clarify_tac);
   7.192  (*OR4*)
   7.193 -by (blast_tac (claset() addSIs [Crypt_imp_OR1]
   7.194 -                       addEs  spies_partsEs) 2);
   7.195 +by (blast_tac (claset() addSIs [Crypt_imp_OR1]) 2);
   7.196  (*OR3*)  (** LEVEL 5 **)
   7.197  (*The hypotheses at this point suggest an attack in which nonce NB is used
   7.198    in two different roles:
     8.1 --- a/src/HOL/Auth/OtwayRees_Bad.thy	Thu Jan 08 18:09:47 1998 +0100
     8.2 +++ b/src/HOL/Auth/OtwayRees_Bad.thy	Thu Jan 08 18:10:34 1998 +0100
     8.3 @@ -72,6 +72,6 @@
     8.4      Oops "[| evso: otway;  B ~= Spy;
     8.5               Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
     8.6                 : set evso |]
     8.7 -          ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
     8.8 +          ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
     8.9  
    8.10  end
     9.1 --- a/src/HOL/Auth/Yahalom.ML	Thu Jan 08 18:09:47 1998 +0100
     9.2 +++ b/src/HOL/Auth/Yahalom.ML	Thu Jan 08 18:10:34 1998 +0100
     9.3 @@ -202,12 +202,12 @@
     9.4  (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
     9.5  
     9.6  goal thy 
     9.7 - "!!evs. [| A ~: bad;  B ~: bad;  evs : yahalom |]         \
     9.8 + "!!evs. [| A ~: bad;  B ~: bad;  evs : yahalom |]                \
     9.9  \        ==> Says Server A                                        \
    9.10  \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
    9.11  \                Crypt (shrK B) {|Agent A, Key K|}|}              \
    9.12  \             : set evs -->                                       \
    9.13 -\            Says A Spy {|na, nb, Key K|} ~: set evs -->          \
    9.14 +\            Notes Spy {|na, nb, Key K|} ~: set evs -->           \
    9.15  \            Key K ~: analz (spies evs)";
    9.16  by (etac yahalom.induct 1);
    9.17  by analz_spies_tac;
    9.18 @@ -232,8 +232,8 @@
    9.19  \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
    9.20  \                Crypt (shrK B) {|Agent A, Key K|}|}              \
    9.21  \             : set evs;                                          \
    9.22 -\           Says A Spy {|na, nb, Key K|} ~: set evs;              \
    9.23 -\           A ~: bad;  B ~: bad;  evs : yahalom |]         \
    9.24 +\           Notes Spy {|na, nb, Key K|} ~: set evs;               \
    9.25 +\           A ~: bad;  B ~: bad;  evs : yahalom |]                \
    9.26  \        ==> Key K ~: analz (spies evs)";
    9.27  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
    9.28  by (blast_tac (claset() addSEs [lemma]) 1);
    9.29 @@ -322,6 +322,12 @@
    9.30  qed "KeyWithNonce_Says";
    9.31  Addsimps [KeyWithNonce_Says];
    9.32  
    9.33 +goalw thy [KeyWithNonce_def]
    9.34 +   "KeyWithNonce K NB (Notes A X # evs) = KeyWithNonce K NB evs";
    9.35 +by (Simp_tac 1);
    9.36 +qed "KeyWithNonce_Notes";
    9.37 +Addsimps [KeyWithNonce_Notes];
    9.38 +
    9.39  (*A fresh key cannot be associated with any nonce 
    9.40    (with respect to a given trace). *)
    9.41  goalw thy [KeyWithNonce_def]
    9.42 @@ -372,7 +378,8 @@
    9.43       (analz_image_freshK_ss 
    9.44         addsimps expand_ifs
    9.45         addsimps [all_conj_distrib, analz_image_freshK,
    9.46 -		 KeyWithNonce_Says, fresh_not_KeyWithNonce, 
    9.47 +		 KeyWithNonce_Says, KeyWithNonce_Notes,
    9.48 +		 fresh_not_KeyWithNonce, 
    9.49  		 imp_disj_not1,		     (*Moves NBa~=NB to the front*)
    9.50  		 Says_Server_KeyWithNonce])));
    9.51  (*Fake*) 
    9.52 @@ -478,7 +485,7 @@
    9.53  \ ==> Says B Server                                                    \
    9.54  \          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
    9.55  \     : set evs -->                                                    \
    9.56 -\     (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs) -->     \
    9.57 +\     (ALL k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs) -->      \
    9.58  \     Nonce NB ~: analz (spies evs)";
    9.59  by (etac yahalom.induct 1);
    9.60  by analz_spies_tac;
    9.61 @@ -529,7 +536,7 @@
    9.62  
    9.63  
    9.64  (*B's session key guarantee from YM4.  The two certificates contribute to a
    9.65 -  single conclusion about the Server's message.  Note that the "Says A Spy"
    9.66 +  single conclusion about the Server's message.  Note that the "Notes Spy"
    9.67    assumption must quantify over ALL POSSIBLE keys instead of our particular K.
    9.68    If this run is broken and the spy substitutes a certificate containing an
    9.69    old key, B has no means of telling.*)
    9.70 @@ -539,7 +546,7 @@
    9.71  \             : set evs;                                                    \
    9.72  \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
    9.73  \                       Crypt K (Nonce NB)|} : set evs;                     \
    9.74 -\           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs;         \
    9.75 +\           ALL k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs;          \
    9.76  \           A ~: bad;  B ~: bad;  evs : yahalom |]       \
    9.77  \         ==> Says Server A                                                 \
    9.78  \                     {|Crypt (shrK A) {|Agent B, Key K,                    \
    9.79 @@ -636,7 +643,7 @@
    9.80  \             : set evs;                                                    \
    9.81  \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
    9.82  \                       Crypt K (Nonce NB)|} : set evs;                     \
    9.83 -\           (ALL NA k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs);    \
    9.84 +\           (ALL NA k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs);     \
    9.85  \           A ~: bad;  B ~: bad;  evs : yahalom |]       \
    9.86  \        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
    9.87  by (dtac B_trusts_YM4 1);
    10.1 --- a/src/HOL/Auth/Yahalom.thy	Thu Jan 08 18:09:47 1998 +0100
    10.2 +++ b/src/HOL/Auth/Yahalom.thy	Thu Jan 08 18:10:34 1998 +0100
    10.3 @@ -64,7 +64,7 @@
    10.4               Says Server A {|Crypt (shrK A)
    10.5                                     {|Agent B, Key K, Nonce NA, Nonce NB|},
    10.6                               X|}  : set evso |]
    10.7 -          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evso : yahalom"
    10.8 +          ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : yahalom"
    10.9  
   10.10  
   10.11  constdefs 
    11.1 --- a/src/HOL/Auth/Yahalom2.ML	Thu Jan 08 18:09:47 1998 +0100
    11.2 +++ b/src/HOL/Auth/Yahalom2.ML	Thu Jan 08 18:10:34 1998 +0100
    11.3 @@ -209,7 +209,7 @@
    11.4  \              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},     \
    11.5  \                    Crypt (shrK B) {|nb, Key K, Agent A|}|}    \
    11.6  \             : set evs -->                                     \
    11.7 -\            Says A Spy {|na, nb, Key K|} ~: set evs -->        \
    11.8 +\            Notes Spy {|na, nb, Key K|} ~: set evs -->         \
    11.9  \            Key K ~: analz (spies evs)";
   11.10  by (etac yahalom.induct 1);
   11.11  by analz_spies_tac;
   11.12 @@ -235,8 +235,8 @@
   11.13  \              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},  \
   11.14  \                    Crypt (shrK B) {|nb, Key K, Agent A|}|} \
   11.15  \           : set evs;                                       \
   11.16 -\           Says A Spy {|na, nb, Key K|} ~: set evs;         \
   11.17 -\           A ~: bad;  B ~: bad;  evs : yahalom |]         \
   11.18 +\           Notes Spy {|na, nb, Key K|} ~: set evs;          \
   11.19 +\           A ~: bad;  B ~: bad;  evs : yahalom |]           \
   11.20  \        ==> Key K ~: analz (spies evs)";
   11.21  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   11.22  by (blast_tac (claset() addSEs [lemma]) 1);
   11.23 @@ -249,8 +249,8 @@
   11.24    May now apply Spy_not_see_encrypted_key, subject to its conditions.*)
   11.25  goal thy
   11.26   "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na|}                      \
   11.27 -\            : parts (spies evs);                                   \
   11.28 -\           A ~: bad;  evs : yahalom |]                               \
   11.29 +\            : parts (spies evs);                                      \
   11.30 +\           A ~: bad;  evs : yahalom |]                                \
   11.31  \         ==> EX nb. Says Server A                                     \
   11.32  \                      {|nb, Crypt (shrK A) {|Agent B, Key K, na|},    \
   11.33  \                            Crypt (shrK B) {|nb, Key K, Agent A|}|}   \
   11.34 @@ -384,7 +384,7 @@
   11.35  goal thy 
   11.36   "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|},    \
   11.37  \                       Crypt K (Nonce NB)|} : set evs;                 \
   11.38 -\           (ALL NA. Says A Spy {|Nonce NA, Nonce NB, Key K|} ~: set evs); \
   11.39 +\           (ALL NA. Notes Spy {|Nonce NA, Nonce NB, Key K|} ~: set evs); \
   11.40  \           A ~: bad;  B ~: bad;  evs : yahalom |]                    \
   11.41  \        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
   11.42  by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1);
    12.1 --- a/src/HOL/Auth/Yahalom2.thy	Thu Jan 08 18:09:47 1998 +0100
    12.2 +++ b/src/HOL/Auth/Yahalom2.thy	Thu Jan 08 18:10:34 1998 +0100
    12.3 @@ -68,6 +68,6 @@
    12.4               Says Server A {|Nonce NB, 
    12.5                               Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
    12.6                               X|}  : set evso |]
    12.7 -          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evso : yahalom"
    12.8 +          ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : yahalom"
    12.9  
   12.10  end