Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
authorpaulson
Tue Mar 09 11:01:39 1999 +0100 (1999-03-09)
changeset 630876f3865a2b1d
parent 6307 fdf236c98914
child 6309 ca52347e259a
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
Changing "spies" to "knows Spy", etc. Retaining the constant "spies" as a
translation.
src/HOL/Auth/Event.ML
src/HOL/Auth/Event.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/Public.ML
src/HOL/Auth/Shared.ML
src/HOL/Auth/TLS.ML
     1.1 --- a/src/HOL/Auth/Event.ML	Mon Mar 08 13:49:53 1999 +0100
     1.2 +++ b/src/HOL/Auth/Event.ML	Tue Mar 09 11:01:39 1999 +0100
     1.3 @@ -2,90 +2,170 @@
     1.4      ID:         $Id$
     1.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.6      Copyright   1996  University of Cambridge
     1.7 -
     1.8 -Theory of events for security protocols
     1.9 -
    1.10 -Datatype of events; function "sees"; freshness
    1.11  *)
    1.12  
    1.13  AddIffs [Spy_in_bad, Server_not_bad];
    1.14  
    1.15 -(**** Function "spies" ****)
    1.16 +Addsimps [knows_Cons, used_Cons];
    1.17 +
    1.18 +(**** Function "knows" ****)
    1.19  
    1.20 -(** Simplifying   parts (insert X (spies evs))
    1.21 -      = parts {X} Un parts (spies evs) -- since general case loops*)
    1.22 +(** Simplifying   parts (insert X (knows Spy evs))
    1.23 +      = parts {X} Un parts (knows Spy evs) -- since general case loops*)
    1.24  
    1.25 -bind_thm ("parts_insert_spies",
    1.26 +bind_thm ("parts_insert_knows_Spy",
    1.27  	  parts_insert |> 
    1.28 -	  read_instantiate_sg (sign_of thy) [("H", "spies evs")]);
    1.29 +	  read_instantiate_sg (sign_of thy) [("H", "knows Spy evs")]);
    1.30  
    1.31  
    1.32 -Goal "P(event_case sf nf ev) = \
    1.33 +Goal "P(event_case sf nf gf ev) = \
    1.34  \      ((ALL A B X. ev = Says A B X --> P(sf A B X)) & \
    1.35 -\       (ALL A X. ev = Notes A X --> P(nf A X)))";
    1.36 +\       (ALL A X. ev = Notes A X --> P(nf A X)) & \
    1.37 +\       (ALL A X. ev = Gets A X --> P(gf A X)))";
    1.38  by (induct_tac "ev" 1);
    1.39  by Auto_tac;
    1.40  qed "expand_event_case";
    1.41  
    1.42 -Goal "spies (Says A B X # evs) = insert X (spies evs)";
    1.43 +Goal "knows Spy (Says A B X # evs) = insert X (knows Spy evs)";
    1.44  by (Simp_tac 1);
    1.45 -qed "spies_Says";
    1.46 +qed "knows_Spy_Says";
    1.47  
    1.48  (*The point of letting the Spy see "bad" agents' notes is to prevent
    1.49    redundant case-splits on whether A=Spy and whether A:bad*)
    1.50 -Goal "spies (Notes A X # evs) = \
    1.51 -\         (if A:bad then insert X (spies evs) else spies evs)";
    1.52 +Goal "knows Spy (Notes A X # evs) = \
    1.53 +\         (if A:bad then insert X (knows Spy evs) else knows Spy evs)";
    1.54  by (Simp_tac 1);
    1.55 -qed "spies_Notes";
    1.56 +qed "knows_Spy_Notes";
    1.57  
    1.58 -Goal "spies evs <= spies (Says A B X # evs)";
    1.59 +Goal "knows Spy (Gets A X # evs) = knows Spy evs";
    1.60 +by (Simp_tac 1);
    1.61 +qed "knows_Spy_Gets";
    1.62 +
    1.63 +Goal "knows Spy evs <= knows Spy (Says A B X # evs)";
    1.64  by (simp_tac (simpset() addsimps [subset_insertI]) 1);
    1.65 -qed "spies_subset_spies_Says";
    1.66 +qed "knows_Spy_subset_knows_Spy_Says";
    1.67  
    1.68 -Goal "spies evs <= spies (Notes A X # evs)";
    1.69 +Goal "knows Spy evs <= knows Spy (Notes A X # evs)";
    1.70  by (Simp_tac 1);
    1.71  by (Fast_tac 1);
    1.72 -qed "spies_subset_spies_Notes";
    1.73 +qed "knows_Spy_subset_knows_Spy_Notes";
    1.74  
    1.75 -(*Spy sees all traffic*)
    1.76 -Goal "Says A B X : set evs --> X : spies evs";
    1.77 +Goal "knows Spy evs <= knows Spy (Gets A X # evs)";
    1.78 +by (simp_tac (simpset() addsimps [subset_insertI]) 1);
    1.79 +qed "knows_Spy_subset_knows_Spy_Gets";
    1.80 +
    1.81 +(*Spy sees what is sent on the traffic*)
    1.82 +Goal "Says A B X : set evs --> X : knows Spy evs";
    1.83  by (induct_tac "evs" 1);
    1.84  by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
    1.85 -qed_spec_mp "Says_imp_spies";
    1.86 +qed_spec_mp "Says_imp_knows_Spy";
    1.87  
    1.88 -(*Spy sees Notes of bad agents*)
    1.89 -Goal "Notes A X : set evs --> A: bad --> X : spies evs";
    1.90 +Goal "Notes A X : set evs --> A: bad --> X : knows Spy evs";
    1.91  by (induct_tac "evs" 1);
    1.92  by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
    1.93 -qed_spec_mp "Notes_imp_spies";
    1.94 +qed_spec_mp "Notes_imp_knows_Spy";
    1.95 +
    1.96  
    1.97  (*Use with addSEs to derive contradictions from old Says events containing
    1.98    items known to be fresh*)
    1.99 -val spies_partsEs = make_elim (Says_imp_spies RS parts.Inj) :: partsEs;
   1.100 +val knows_Spy_partsEs = make_elim (Says_imp_knows_Spy RS parts.Inj) :: partsEs;
   1.101 +
   1.102 +Addsimps [knows_Spy_Says, knows_Spy_Notes, knows_Spy_Gets];
   1.103 +
   1.104 +
   1.105 +(*Begin lemmas about agents' knowledge*)
   1.106 +
   1.107 +Goal "knows A (Says A B X # evs) = insert X (knows A evs)";
   1.108 +by (Simp_tac 1);
   1.109 +qed "knows_Says";
   1.110 +
   1.111 +Goal "knows A (Notes A X # evs) = insert X (knows A evs)";
   1.112 +by (Simp_tac 1);
   1.113 +qed "knows_Notes";
   1.114 +
   1.115 +Goal "A ~= Spy --> knows A (Gets A X # evs) = insert X (knows A evs)";
   1.116 +by (Simp_tac 1);
   1.117 +qed "knows_Gets";
   1.118 +
   1.119 +
   1.120 +Goal "knows A evs <= knows A (Says A B X # evs)";
   1.121 +by (simp_tac (simpset() addsimps [subset_insertI]) 1);
   1.122 +qed "knows_subset_knows_Says";
   1.123 +
   1.124 +Goal "knows A evs <= knows A (Notes A X # evs)";
   1.125 +by (simp_tac (simpset() addsimps [subset_insertI]) 1);
   1.126 +qed "knows_subset_knows_Notes";
   1.127 +
   1.128 +Goal "knows A evs <= knows A (Gets A X # evs)";
   1.129 +by (simp_tac (simpset() addsimps [subset_insertI]) 1);
   1.130 +qed "knows_subset_knows_Gets";
   1.131  
   1.132 -Addsimps [spies_Says, spies_Notes];
   1.133 +(*Agents know what they say*)
   1.134 +Goal "Says A B X : set evs --> X : knows A evs";
   1.135 +by (induct_tac "evs" 1);
   1.136 +by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
   1.137 +by (Blast_tac 1);
   1.138 +qed_spec_mp "Says_imp_knows";
   1.139 +
   1.140 +(*Agents know what they note*)
   1.141 +Goal "Notes A X : set evs --> X : knows A evs";
   1.142 +by (induct_tac "evs" 1);
   1.143 +by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
   1.144 +by (Blast_tac 1);
   1.145 +qed_spec_mp "Notes_imp_knows";
   1.146 +
   1.147 +(*Agents know what they receive*)
   1.148 +Goal "A ~= Spy --> Gets A X : set evs --> X : knows A evs";
   1.149 +by (induct_tac "evs" 1);
   1.150 +by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
   1.151 +qed_spec_mp "Gets_imp_knows_agents";
   1.152 +
   1.153 +
   1.154 +(*What agents DIFFERENT FROM Spy know 
   1.155 +  was either said, or noted, or got, or known initially*)
   1.156 +Goal "[| X : knows A evs; A ~= Spy |] ==> EX B. \
   1.157 +\ Says A B X : set evs | Gets A X : set evs | Notes A X : set evs | X : initState A";
   1.158 +by (etac rev_mp 1);
   1.159 +by (induct_tac "evs" 1);
   1.160 +by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
   1.161 +by (Blast_tac 1);
   1.162 +qed_spec_mp "knows_imp_Says_Gets_Notes_initState";
   1.163 +
   1.164 +(*What the Spy knows -- for the time being --
   1.165 +  was either said or noted, or known initially*)
   1.166 +Goal "[| X : knows Spy evs |] ==> EX A B. \
   1.167 +\ Says A B X : set evs | Notes A X : set evs | X : initState Spy";
   1.168 +by (etac rev_mp 1);
   1.169 +by (induct_tac "evs" 1);
   1.170 +by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
   1.171 +by (Blast_tac 1);
   1.172 +qed_spec_mp "knows_Spy_imp_Says_Notes_initState";
   1.173 +
   1.174 +(*END lemmas about agents' knowledge*)
   1.175 +
   1.176 +
   1.177  
   1.178  (**** NOTE REMOVAL--laws above are cleaner, as they don't involve "case" ****)
   1.179 -Delsimps [spies_Cons];   
   1.180 +Delsimps [knows_Cons];   
   1.181  
   1.182  
   1.183  (*** Fresh nonces ***)
   1.184  
   1.185 -Goal "parts (spies evs) <= used evs";
   1.186 +Goal "parts (knows Spy evs) <= used evs";
   1.187  by (induct_tac "evs" 1);
   1.188  by (ALLGOALS (asm_simp_tac
   1.189 -	      (simpset() addsimps [parts_insert_spies]
   1.190 +	      (simpset() addsimps [parts_insert_knows_Spy]
   1.191  	                addsplits [expand_event_case])));
   1.192  by (ALLGOALS Blast_tac);
   1.193 -qed "parts_spies_subset_used";
   1.194 +qed "parts_knows_Spy_subset_used";
   1.195  
   1.196 -bind_thm ("usedI", impOfSubs parts_spies_subset_used);
   1.197 +bind_thm ("usedI", impOfSubs parts_knows_Spy_subset_used);
   1.198  AddIs [usedI];
   1.199  
   1.200  Goal "parts (initState B) <= used evs";
   1.201  by (induct_tac "evs" 1);
   1.202  by (ALLGOALS (asm_simp_tac
   1.203 -	      (simpset() addsimps [parts_insert_spies]
   1.204 +	      (simpset() addsimps [parts_insert_knows_Spy]
   1.205  	                addsplits [expand_event_case])));
   1.206  by (ALLGOALS Blast_tac);
   1.207  bind_thm ("initState_into_used", impOfSubs (result()));
   1.208 @@ -100,6 +180,11 @@
   1.209  qed "used_Notes";
   1.210  Addsimps [used_Notes];
   1.211  
   1.212 +Goal "used (Gets A X # evs) = used evs";
   1.213 +by (Simp_tac 1);
   1.214 +qed "used_Gets";
   1.215 +Addsimps [used_Gets];
   1.216 +
   1.217  Goal "used [] <= used evs";
   1.218  by (Simp_tac 1);
   1.219  by (blast_tac (claset() addIs [initState_into_used]) 1);
   1.220 @@ -109,29 +194,34 @@
   1.221  Delsimps [used_Nil, used_Cons];   
   1.222  
   1.223  
   1.224 -(*currently unused*)
   1.225 -Goal "used evs <= used (evs@evs')";
   1.226 -by (induct_tac "evs" 1);
   1.227 -by (simp_tac (simpset() addsimps [used_nil_subset]) 1);
   1.228 -by (induct_tac "a" 1);
   1.229 -by (ALLGOALS Asm_simp_tac);
   1.230 -by (ALLGOALS Blast_tac);
   1.231 -qed "used_subset_append";
   1.232 -
   1.233 -
   1.234 -(*For proving theorems of the form X ~: analz (spies evs) --> P
   1.235 +(*For proving theorems of the form X ~: analz (knows Spy evs) --> P
   1.236    New events added by induction to "evs" are discarded.  Provided 
   1.237    this information isn't needed, the proof will be much shorter, since
   1.238    it will omit complicated reasoning about analz.*)
   1.239  val analz_mono_contra_tac = 
   1.240    let val analz_impI = read_instantiate_sg (sign_of thy)
   1.241 -                [("P", "?Y ~: analz (spies ?evs)")] impI;
   1.242 +                [("P", "?Y ~: analz (knows Spy ?evs)")] impI;
   1.243    in
   1.244      rtac analz_impI THEN' 
   1.245      REPEAT1 o 
   1.246        (dresolve_tac 
   1.247 -       [spies_subset_spies_Says  RS analz_mono RS contra_subsetD,
   1.248 -	spies_subset_spies_Notes RS analz_mono RS contra_subsetD])
   1.249 +       [knows_Spy_subset_knows_Spy_Says RS analz_mono RS contra_subsetD,
   1.250 +        knows_Spy_subset_knows_Spy_Notes RS analz_mono RS contra_subsetD,
   1.251 +	knows_Spy_subset_knows_Spy_Gets RS analz_mono RS contra_subsetD])
   1.252      THEN'
   1.253      mp_tac
   1.254    end;
   1.255 +
   1.256 +fun Reception_tac i =
   1.257 +    blast_tac (claset() addDs [Says_imp_knows_Spy RS parts.Inj, 
   1.258 +                               impOfSubs (parts_insert RS equalityD1), 
   1.259 +			       parts_trans,
   1.260 +                               Says_imp_knows_Spy RS analz.Inj,
   1.261 +                               impOfSubs analz_mono, analz_cut] 
   1.262 +                        addIs [less_SucI]) i;
   1.263 +
   1.264 +
   1.265 +(*Compatibility for the old "spies" function*)
   1.266 +val spies_partsEs = knows_Spy_partsEs;
   1.267 +val Says_imp_spies = Says_imp_knows_Spy;
   1.268 +val parts_insert_spies = parts_insert_knows_Spy;
     2.1 --- a/src/HOL/Auth/Event.thy	Mon Mar 08 13:49:53 1999 +0100
     2.2 +++ b/src/HOL/Auth/Event.thy	Tue Mar 09 11:01:39 1999 +0100
     2.3 @@ -19,24 +19,49 @@
     2.4  datatype  (*Messages--could add another constructor for agent knowledge*)
     2.5    event = Says  agent agent msg
     2.6          | Notes agent       msg
     2.7 +        | Gets  agent       msg
     2.8 +       
     2.9 +consts 
    2.10 +  bad    :: agent set        (*compromised agents*)
    2.11 +  knows  :: agent => event list => msg set
    2.12  
    2.13 -consts  
    2.14 -  bad    :: agent set        (*compromised agents*)
    2.15 +
    2.16 +(*"spies" is retained for compability's sake*)
    2.17 +syntax
    2.18    spies  :: event list => msg set
    2.19  
    2.20 +translations
    2.21 +  "spies"   => "knows Spy"
    2.22 +
    2.23 +
    2.24  rules
    2.25    (*Spy has access to his own key for spoof messages, but Server is secure*)
    2.26    Spy_in_bad     "Spy: bad"
    2.27    Server_not_bad "Server ~: bad"
    2.28  
    2.29  primrec
    2.30 -           (*Spy reads all traffic whether addressed to him or not*)
    2.31 -  spies_Nil   "spies []       = initState Spy"
    2.32 -  spies_Cons  "spies (ev # evs) =
    2.33 -	         (case ev of
    2.34 -		    Says A B X => insert X (spies evs)
    2.35 -		  | Notes A X  => 
    2.36 -	              if A:bad then insert X (spies evs) else spies evs)"
    2.37 +  knows_Nil   "knows A []         = initState A"
    2.38 +  knows_Cons  "knows A (ev # evs) =
    2.39 +	        (if A = Spy then 
    2.40 +                  (case ev of
    2.41 +		    Says A' B X => insert X (knows Spy evs)
    2.42 +		  | Notes A' X  => 
    2.43 +                   if A' : bad then insert X (knows Spy evs) else knows Spy evs
    2.44 +                  | Gets A' X => knows Spy evs)
    2.45 +                 else
    2.46 +                  (case ev of
    2.47 +		    Says A' B X => 
    2.48 +                      if A'=A then insert X (knows A evs) else knows A evs
    2.49 +		  | Notes A' X    => 
    2.50 +                      if A'=A then insert X (knows A evs) else knows A evs
    2.51 +		  | Gets A' X    => 
    2.52 +                      if A'=A then insert X (knows A evs) else knows A evs))"
    2.53 +
    2.54 +(*
    2.55 +  Case A=Spy on the Gets event
    2.56 +  enforces the fact that if a message is received then it must have been sent,
    2.57 +  therefore the oops case must use Notes
    2.58 +*)
    2.59  
    2.60  consts
    2.61    (*Set of items that might be visible to somebody:
    2.62 @@ -48,6 +73,9 @@
    2.63    used_Cons  "used (ev # evs) =
    2.64  	         (case ev of
    2.65  		    Says A B X => parts {X} Un (used evs)
    2.66 -		  | Notes A X  => parts {X} Un (used evs))"
    2.67 +		  | Notes A X  => parts {X} Un (used evs)
    2.68 +		  | Gets A X   => used evs)"
    2.69 +
    2.70 +
    2.71  
    2.72  end
     3.1 --- a/src/HOL/Auth/OtwayRees.ML	Mon Mar 08 13:49:53 1999 +0100
     3.2 +++ b/src/HOL/Auth/OtwayRees.ML	Tue Mar 09 11:01:39 1999 +0100
     3.3 @@ -12,68 +12,81 @@
     3.4    Proc. Royal Soc. 426 (1989)
     3.5  *)
     3.6  
     3.7 -AddEs spies_partsEs;
     3.8 +AddEs knows_Spy_partsEs;
     3.9  AddDs [impOfSubs analz_subset_parts];
    3.10  AddDs [impOfSubs Fake_parts_insert];
    3.11  
    3.12  
    3.13  (*A "possibility property": there are traces that reach the end*)
    3.14  Goal "[| B ~= Server |]   \
    3.15 -\     ==> EX K. EX NA. EX evs: otway.          \
    3.16 +\     ==> EX NA K. EX evs: otway.          \
    3.17  \            Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
    3.18  \              : set evs";
    3.19  by (REPEAT (resolve_tac [exI,bexI] 1));
    3.20 -by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
    3.21 +by (rtac (otway.Nil RS 
    3.22 +          otway.OR1 RS otway.Reception RS
    3.23 +          otway.OR2 RS otway.Reception RS 
    3.24 +          otway.OR3 RS otway.Reception RS otway.OR4) 2);
    3.25  by possibility_tac;
    3.26  result();
    3.27  
    3.28 +Goal "[| Gets B X : set evs; evs : otway |] ==> EX A. Says A B X : set evs";
    3.29 +by (etac rev_mp 1);
    3.30 +by (etac otway.induct 1);
    3.31 +by Auto_tac;
    3.32 +qed"Gets_imp_Says";
    3.33 +
    3.34 +(*Must be proved separately for each protocol*)
    3.35 +Goal "[| Gets B X : set evs; evs : otway |]  ==> X : knows Spy evs";
    3.36 +by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1);
    3.37 +qed"Gets_imp_knows_Spy";
    3.38 +AddDs [Gets_imp_knows_Spy RS parts.Inj];
    3.39 +
    3.40  
    3.41  (**** Inductive proofs about otway ****)
    3.42  
    3.43  (** For reasoning about the encrypted portion of messages **)
    3.44  
    3.45 -Goal "Says A' B {|N, Agent A, Agent B, X|} : set evs \
    3.46 -\      ==> X : analz (spies evs)";
    3.47 -by (dtac (Says_imp_spies RS analz.Inj) 1);
    3.48 -by (Blast_tac 1);
    3.49 -qed "OR2_analz_spies";
    3.50 +Goal "[| Gets B {|N, Agent A, Agent B, X|} : set evs;  evs : otway |]  \
    3.51 +\     ==> X : analz (knows Spy evs)";
    3.52 +by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);
    3.53 +qed "OR2_analz_knows_Spy";
    3.54  
    3.55 -Goal "Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
    3.56 -\      ==> X : analz (spies evs)";
    3.57 -by (dtac (Says_imp_spies RS analz.Inj) 1);
    3.58 -by (Blast_tac 1);
    3.59 -qed "OR4_analz_spies";
    3.60 +Goal "[| Gets B {|N, X, Crypt (shrK B) X'|} : set evs;  evs : otway |] \
    3.61 +\     ==> X : analz (knows Spy evs)";
    3.62 +by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);
    3.63 +qed "OR4_analz_knows_Spy";
    3.64  
    3.65  Goal "Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
    3.66 -\      ==> K : parts (spies evs)";
    3.67 +\     ==> K : parts (knows Spy evs)";
    3.68  by (Blast_tac 1);
    3.69 -qed "Oops_parts_spies";
    3.70 +qed "Oops_parts_knows_Spy";
    3.71  
    3.72 -bind_thm ("OR2_parts_spies",
    3.73 -          OR2_analz_spies RS (impOfSubs analz_subset_parts));
    3.74 -bind_thm ("OR4_parts_spies",
    3.75 -          OR4_analz_spies RS (impOfSubs analz_subset_parts));
    3.76 +bind_thm ("OR2_parts_knows_Spy",
    3.77 +          OR2_analz_knows_Spy RS (impOfSubs analz_subset_parts));
    3.78 +bind_thm ("OR4_parts_knows_Spy",
    3.79 +          OR4_analz_knows_Spy RS (impOfSubs analz_subset_parts));
    3.80  
    3.81 -(*For proving the easier theorems about X ~: parts (spies evs).*)
    3.82 +(*For proving the easier theorems about X ~: parts (knows Spy evs).*)
    3.83  fun parts_induct_tac i = 
    3.84      etac otway.induct i			THEN 
    3.85 -    forward_tac [Oops_parts_spies] (i+6) THEN
    3.86 -    forward_tac [OR4_parts_spies]  (i+5) THEN
    3.87 -    forward_tac [OR2_parts_spies]  (i+3) THEN 
    3.88 +    forward_tac [Oops_parts_knows_Spy] (i+7) THEN
    3.89 +    forward_tac [OR4_parts_knows_Spy]  (i+6) THEN
    3.90 +    forward_tac [OR2_parts_knows_Spy]  (i+4) THEN 
    3.91      prove_simple_subgoals_tac  i;
    3.92  
    3.93  
    3.94 -(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
    3.95 +(** Theorems of the form X ~: parts (knows Spy evs) imply that NOBODY
    3.96      sends messages containing X! **)
    3.97  
    3.98  (*Spy never sees a good agent's shared key!*)
    3.99 -Goal "evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
   3.100 +Goal "evs : otway ==> (Key (shrK A) : parts (knows Spy evs)) = (A : bad)";
   3.101  by (parts_induct_tac 1);
   3.102  by (ALLGOALS Blast_tac);
   3.103  qed "Spy_see_shrK";
   3.104  Addsimps [Spy_see_shrK];
   3.105  
   3.106 -Goal "evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
   3.107 +Goal "evs : otway ==> (Key (shrK A) : analz (knows Spy evs)) = (A : bad)";
   3.108  by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
   3.109  qed "Spy_analz_shrK";
   3.110  Addsimps [Spy_analz_shrK];
   3.111 @@ -83,7 +96,7 @@
   3.112  
   3.113  
   3.114  (*Nobody can have used non-existent keys!*)
   3.115 -Goal "evs : otway ==> Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
   3.116 +Goal "evs : otway ==> Key K ~: used evs --> K ~: keysFor (parts (knows Spy evs))";
   3.117  by (parts_induct_tac 1);
   3.118  (*Fake*)
   3.119  by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
   3.120 @@ -114,18 +127,18 @@
   3.121  
   3.122  
   3.123  (*For proofs involving analz.*)
   3.124 -val analz_spies_tac = 
   3.125 -    dtac OR2_analz_spies 4 THEN 
   3.126 -    dtac OR4_analz_spies 6 THEN
   3.127 -    forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN
   3.128 -    REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
   3.129 +val analz_knows_Spy_tac = 
   3.130 +    dtac OR2_analz_knows_Spy 5 THEN assume_tac 5 THEN 
   3.131 +    dtac OR4_analz_knows_Spy 7 THEN assume_tac 7 THEN
   3.132 +    forward_tac [Says_Server_message_form] 8 THEN assume_tac 8 THEN
   3.133 +    REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 8);
   3.134  
   3.135  
   3.136  (****
   3.137   The following is to prove theorems of the form
   3.138  
   3.139 -  Key K : analz (insert (Key KAB) (spies evs)) ==>
   3.140 -  Key K : analz (spies evs)
   3.141 +  Key K : analz (insert (Key KAB) (knows Spy evs)) ==>
   3.142 +  Key K : analz (knows Spy evs)
   3.143  
   3.144   A more general formula must be proved inductively.
   3.145  ****)
   3.146 @@ -135,10 +148,10 @@
   3.147  
   3.148  (*The equality makes the induction hypothesis easier to apply*)
   3.149  Goal "evs : otway ==> ALL K KK. KK <= - (range shrK) -->           \
   3.150 -\                      (Key K : analz (Key``KK Un (spies evs))) =  \
   3.151 -\                      (K : KK | Key K : analz (spies evs))";
   3.152 +\                      (Key K : analz (Key``KK Un (knows Spy evs))) =  \
   3.153 +\                      (K : KK | Key K : analz (knows Spy evs))";
   3.154  by (etac otway.induct 1);
   3.155 -by analz_spies_tac;
   3.156 +by analz_knows_Spy_tac;
   3.157  by (REPEAT_FIRST (resolve_tac [allI, impI]));
   3.158  by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
   3.159  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   3.160 @@ -148,8 +161,8 @@
   3.161  
   3.162  
   3.163  Goal "[| evs : otway;  KAB ~: range shrK |]               \
   3.164 -\     ==> Key K : analz (insert (Key KAB) (spies evs)) =  \
   3.165 -\         (K = KAB | Key K : analz (spies evs))";
   3.166 +\     ==> Key K : analz (insert (Key KAB) (knows Spy evs)) =  \
   3.167 +\         (K = KAB | Key K : analz (knows Spy evs))";
   3.168  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   3.169  qed "analz_insert_freshK";
   3.170  
   3.171 @@ -169,7 +182,7 @@
   3.172  by (expand_case_tac "K = ?y" 1);
   3.173  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   3.174  (*...we assume X is a recent message, and handle this case by contradiction*)
   3.175 -by (blast_tac (claset() addSEs spies_partsEs) 1);
   3.176 +by (blast_tac (claset() addSEs knows_Spy_partsEs) 1);
   3.177  val lemma = result();
   3.178  
   3.179  Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}   : set evs; \ 
   3.180 @@ -179,12 +192,11 @@
   3.181  qed "unique_session_keys";
   3.182  
   3.183  
   3.184 -
   3.185  (**** Authenticity properties relating to NA ****)
   3.186  
   3.187  (*Only OR1 can have caused such a part of a message to appear.*)
   3.188  Goal "[| A ~: bad;  evs : otway |]                             \
   3.189 -\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
   3.190 +\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (knows Spy evs) --> \
   3.191  \     Says A B {|NA, Agent A, Agent B,                      \
   3.192  \                Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
   3.193  \      : set evs";
   3.194 @@ -192,12 +204,21 @@
   3.195  by (Blast_tac 1);
   3.196  qed_spec_mp "Crypt_imp_OR1";
   3.197  
   3.198 +Goal "[| Gets B {|NA, Agent A, Agent B,                      \
   3.199 +\                 Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
   3.200 +\        A ~: bad; evs : otway |]                             \
   3.201 +\    ==> Says A B {|NA, Agent A, Agent B,                      \
   3.202 +\                Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
   3.203 +\      : set evs";
   3.204 +by (blast_tac (claset() addDs [Crypt_imp_OR1]) 1);
   3.205 +qed"Crypt_imp_OR1_Gets";
   3.206 +
   3.207  
   3.208  (** The Nonce NA uniquely identifies A's message. **)
   3.209  
   3.210  Goal "[| evs : otway; A ~: bad |]               \
   3.211  \ ==> EX B'. ALL B.                                 \
   3.212 -\        Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) \
   3.213 +\        Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (knows Spy evs) \
   3.214  \        --> B = B'";
   3.215  by (parts_induct_tac 1);
   3.216  by (Blast_tac 1);
   3.217 @@ -207,8 +228,8 @@
   3.218  by (Blast_tac 1);
   3.219  val lemma = result();
   3.220  
   3.221 -Goal "[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (spies evs); \
   3.222 -\          Crypt (shrK A) {|NA, Agent A, Agent C|}: parts (spies evs); \
   3.223 +Goal "[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (knows Spy evs); \
   3.224 +\          Crypt (shrK A) {|NA, Agent A, Agent C|}: parts (knows Spy evs); \
   3.225  \          evs : otway;  A ~: bad |]                                   \
   3.226  \        ==> B = C";
   3.227  by (prove_unique_tac lemma 1);
   3.228 @@ -219,19 +240,19 @@
   3.229    OR2 encrypts Nonce NB.  It prevents the attack that can occur in the
   3.230    over-simplified version of this protocol: see OtwayRees_Bad.*)
   3.231  Goal "[| A ~: bad;  evs : otway |]                      \
   3.232 -\        ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
   3.233 +\        ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (knows Spy evs) --> \
   3.234  \            Crypt (shrK A) {|NA', NA, Agent A', Agent A|}  \
   3.235 -\             ~: parts (spies evs)";
   3.236 +\             ~: parts (knows Spy evs)";
   3.237  by (parts_induct_tac 1);
   3.238 -by (ALLGOALS Blast_tac);
   3.239 -qed_spec_mp"no_nonce_OR1_OR2";
   3.240 +by Auto_tac;
   3.241 +qed_spec_mp "no_nonce_OR1_OR2";
   3.242  
   3.243  val nonce_OR1_OR2_E = no_nonce_OR1_OR2 RSN (2, rev_notE);
   3.244  
   3.245  (*Crucial property: If the encrypted message appears, and A has used NA
   3.246    to start a run, then it originated with the Server!*)
   3.247  Goal "[| A ~: bad;  evs : otway |]                                  \
   3.248 -\    ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs)              \
   3.249 +\    ==> Crypt (shrK A) {|NA, Key K|} : parts (knows Spy evs)              \
   3.250  \        --> Says A B {|NA, Agent A, Agent B,                          \
   3.251  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}      \
   3.252  \             : set evs -->                                            \
   3.253 @@ -253,7 +274,7 @@
   3.254  (*OR3, two cases*)  (** LEVEL 7 **)
   3.255  by (blast_tac (claset() addSEs  [nonce_OR1_OR2_E]
   3.256                          delrules [conjI] (*stop split-up into 4 subgoals*)) 2);
   3.257 -by (blast_tac (claset() addIs  [unique_NA]) 1);
   3.258 +by (blast_tac (claset() addIs [unique_NA]) 1);
   3.259  qed_spec_mp "NA_Crypt_imp_Server_msg";
   3.260  
   3.261  
   3.262 @@ -263,7 +284,7 @@
   3.263    Spy_not_see_encrypted_key*)
   3.264  Goal "[| Says A  B {|NA, Agent A, Agent B,                       \
   3.265  \                Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
   3.266 -\    Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
   3.267 +\        Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
   3.268  \    A ~: bad;  evs : otway |]                              \
   3.269  \ ==> EX NB. Says Server B                                  \
   3.270  \              {|NA,                                        \
   3.271 @@ -283,9 +304,9 @@
   3.272  \       {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   3.273  \         Crypt (shrK B) {|NB, Key K|}|} : set evs -->         \
   3.274  \     Notes Spy {|NA, NB, Key K|} ~: set evs -->               \
   3.275 -\     Key K ~: analz (spies evs)";
   3.276 +\     Key K ~: analz (knows Spy evs)";
   3.277  by (etac otway.induct 1);
   3.278 -by analz_spies_tac;
   3.279 +by analz_knows_Spy_tac;
   3.280  by (ALLGOALS
   3.281      (asm_simp_tac (simpset() addcongs [conj_cong] 
   3.282                               addsimps [analz_insert_eq, analz_insert_freshK]
   3.283 @@ -305,7 +326,7 @@
   3.284  \               Crypt (shrK B) {|NB, Key K|}|} : set evs;        \
   3.285  \        Notes Spy {|NA, NB, Key K|} ~: set evs;                 \
   3.286  \        A ~: bad;  B ~: bad;  evs : otway |]                    \
   3.287 -\     ==> Key K ~: analz (spies evs)";
   3.288 +\     ==> Key K ~: analz (knows Spy evs)";
   3.289  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   3.290  by (blast_tac (claset() addSEs [lemma]) 1);
   3.291  qed "Spy_not_see_encrypted_key";
   3.292 @@ -315,10 +336,10 @@
   3.293    what it is.*)
   3.294  Goal "[| Says A  B {|NA, Agent A, Agent B,                       \
   3.295  \                    Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
   3.296 -\        Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
   3.297 +\        Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
   3.298  \        ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs;         \
   3.299  \        A ~: bad;  B ~: bad;  evs : otway |]                    \
   3.300 -\     ==> Key K ~: analz (spies evs)";
   3.301 +\     ==> Key K ~: analz (knows Spy evs)";
   3.302  by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1);
   3.303  qed "A_gets_good_key";
   3.304  
   3.305 @@ -329,7 +350,7 @@
   3.306    know anything about X: it does NOT have to have the right form.*)
   3.307  Goal "[| B ~: bad;  evs : otway |]                         \
   3.308  \     ==> Crypt (shrK B) {|NA, NB, Agent A, Agent B|}       \
   3.309 -\          : parts (spies evs) -->                       \
   3.310 +\          : parts (knows Spy evs) -->                       \
   3.311  \         (EX X. Says B Server                              \
   3.312  \          {|NA, Agent A, Agent B, X,                       \
   3.313  \            Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   3.314 @@ -343,7 +364,7 @@
   3.315  
   3.316  Goal "[| evs : otway; B ~: bad |]  \
   3.317  \ ==> EX NA' A'. ALL NA A.            \
   3.318 -\      Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs) \
   3.319 +\      Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(knows Spy evs) \
   3.320  \      --> NA = NA' & A = A'";
   3.321  by (parts_induct_tac 1);
   3.322  by (Blast_tac 1);
   3.323 @@ -353,18 +374,17 @@
   3.324  by (Blast_tac 1);
   3.325  val lemma = result();
   3.326  
   3.327 -Goal "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs); \
   3.328 -\          Crypt (shrK B) {|NC, NB, Agent C, Agent B|} : parts(spies evs); \
   3.329 +Goal "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(knows Spy evs); \
   3.330 +\          Crypt (shrK B) {|NC, NB, Agent C, Agent B|} : parts(knows Spy evs); \
   3.331  \          evs : otway;  B ~: bad |]             \
   3.332  \        ==> NC = NA & C = A";
   3.333  by (prove_unique_tac lemma 1);
   3.334  qed "unique_NB";
   3.335  
   3.336 -
   3.337  (*If the encrypted message appears, and B has used Nonce NB,
   3.338    then it originated with the Server!*)
   3.339  Goal "[| B ~: bad;  evs : otway |]                                    \
   3.340 -\ ==> Crypt (shrK B) {|NB, Key K|} : parts (spies evs)                \
   3.341 +\ ==> Crypt (shrK B) {|NB, Key K|} : parts (knows Spy evs)                \
   3.342  \     --> (ALL X'. Says B Server                                      \
   3.343  \                    {|NA, Agent A, Agent B, X',                      \
   3.344  \                      Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   3.345 @@ -385,7 +405,8 @@
   3.346  *)
   3.347  by (safe_tac (claset() delrules [disjCI, impCE]));
   3.348  by (Blast_tac 3); 
   3.349 -by (blast_tac (claset() addDs  [unique_NB]) 2);
   3.350 +by (blast_tac (claset() addSDs  [unique_NB]
   3.351 +                        delrules [impCE] (*stop split-up*)) 2);
   3.352  by (blast_tac (claset() addSEs [nonce_OR1_OR2_E]
   3.353                          delrules [conjI] (*stop split-up*)) 1);
   3.354  qed_spec_mp "NB_Crypt_imp_Server_msg";
   3.355 @@ -396,7 +417,7 @@
   3.356  Goal "[| Says B Server {|NA, Agent A, Agent B, X',              \
   3.357  \                        Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
   3.358  \         : set evs;                                            \
   3.359 -\        Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;   \
   3.360 +\        Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;   \
   3.361  \        B ~: bad;  evs : otway |]                              \
   3.362  \     ==> Says Server B                                         \
   3.363  \              {|NA,                                            \
   3.364 @@ -411,10 +432,10 @@
   3.365  Goal "[| Says B Server {|NA, Agent A, Agent B, X',              \
   3.366  \                        Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
   3.367  \          : set evs;                                           \
   3.368 -\        Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;   \
   3.369 +\        Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;   \
   3.370  \        Notes Spy {|NA, NB, Key K|} ~: set evs;                \
   3.371  \        A ~: bad;  B ~: bad;  evs : otway |]                   \
   3.372 -\     ==> Key K ~: analz (spies evs)";
   3.373 +\     ==> Key K ~: analz (knows Spy evs)";
   3.374  by (blast_tac (claset() addSDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1);
   3.375  qed "B_gets_good_key";
   3.376  
   3.377 @@ -436,7 +457,7 @@
   3.378  (*After getting and checking OR4, agent A can trust that B has been active.
   3.379    We could probably prove that X has the expected form, but that is not
   3.380    strictly necessary for authentication.*)
   3.381 -Goal "[| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs;        \
   3.382 +Goal "[| Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs;        \
   3.383  \        Says A  B {|NA, Agent A, Agent B,                                \
   3.384  \                    Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
   3.385  \        A ~: bad;  B ~: bad;  evs : otway |]                             \
     4.1 --- a/src/HOL/Auth/OtwayRees.thy	Mon Mar 08 13:49:53 1999 +0100
     4.2 +++ b/src/HOL/Auth/OtwayRees.thy	Tue Mar 09 11:01:39 1999 +0100
     4.3 @@ -1,19 +1,14 @@
     4.4 -(*  Title:      HOL/Auth/OtwayRees
     4.5 -    ID:         $Id$
     4.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7 -    Copyright   1996  University of Cambridge
     4.8 -
     4.9 -Inductive relation "otway" for the Otway-Rees protocol.
    4.10 +(*  
    4.11 +Inductive relation "otway" for the Otway-Rees protocol
    4.12 +extended by Gets primitive.
    4.13  
    4.14  Version that encrypts Nonce NB
    4.15  
    4.16 -From page 244 of
    4.17 -  Burrows, Abadi and Needham.  A Logic of Authentication.
    4.18 -  Proc. Royal Soc. 426 (1989)
    4.19  *)
    4.20  
    4.21  OtwayRees = Shared + 
    4.22  
    4.23 +
    4.24  consts  otway   :: event list set
    4.25  inductive "otway"
    4.26    intrs 
    4.27 @@ -25,8 +20,13 @@
    4.28           (*The spy MAY say anything he CAN say.  We do not expect him to
    4.29             invent new nonces here, but he can also use NS1.  Common to
    4.30             all similar protocols.*)
    4.31 -    Fake "[| evs: otway;  X: synth (analz (spies evs)) |]
    4.32 -          ==> Says Spy B X  # evs : otway"
    4.33 +    Fake "[| evsa: otway;  X: synth (analz (knows Spy evsa)) |]
    4.34 +          ==> Says Spy B X  # evsa : otway"
    4.35 +
    4.36 +         (*A message that has been sent can be received by the
    4.37 +           intended recipient.*)
    4.38 +    Reception "[| evsr: otway;  Says A B X : set evsr |]
    4.39 +               ==> Gets B X # evsr : otway"
    4.40  
    4.41           (*Alice initiates a protocol run*)
    4.42      OR1  "[| evs1: otway;  Nonce NA ~: used evs1 |]
    4.43 @@ -38,7 +38,7 @@
    4.44  	   the sender is, hence the A' in the sender field.
    4.45             Note that NB is encrypted.*)
    4.46      OR2  "[| evs2: otway;  Nonce NB ~: used evs2;
    4.47 -             Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |]
    4.48 +             Gets B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |]
    4.49            ==> Says B Server 
    4.50                    {|Nonce NA, Agent A, Agent B, X, 
    4.51                      Crypt (shrK B)
    4.52 @@ -49,7 +49,7 @@
    4.53             match.  Then he sends a new session key to Bob with a packet for
    4.54             forwarding to Alice.*)
    4.55      OR3  "[| evs3: otway;  Key KAB ~: used evs3;
    4.56 -             Says B' Server 
    4.57 +             Gets Server 
    4.58                    {|Nonce NA, Agent A, Agent B, 
    4.59                      Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, 
    4.60                      Crypt (shrK B) {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
    4.61 @@ -68,7 +68,7 @@
    4.62                               Crypt (shrK B)
    4.63                                     {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
    4.64                 : set evs4;
    4.65 -             Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
    4.66 +             Gets B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
    4.67                 : set evs4 |]
    4.68            ==> Says B A {|Nonce NA, X|} # evs4 : otway"
    4.69  
     5.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Mon Mar 08 13:49:53 1999 +0100
     5.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Tue Mar 09 11:01:39 1999 +0100
     5.3 @@ -12,7 +12,7 @@
     5.4    IEEE Trans. SE 22 (1), 1996
     5.5  *)
     5.6  
     5.7 -AddEs spies_partsEs;
     5.8 +AddEs knows_Spy_partsEs;
     5.9  AddDs [impOfSubs analz_subset_parts];
    5.10  AddDs [impOfSubs Fake_parts_insert];
    5.11  
    5.12 @@ -23,48 +23,62 @@
    5.13  \          Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
    5.14  \            : set evs";
    5.15  by (REPEAT (resolve_tac [exI,bexI] 1));
    5.16 -by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
    5.17 +by (rtac (otway.Nil RS 
    5.18 +          otway.OR1 RS otway.Reception RS
    5.19 +          otway.OR2 RS otway.Reception RS 
    5.20 +          otway.OR3 RS otway.Reception RS otway.OR4) 2);
    5.21  by possibility_tac;
    5.22  result();
    5.23  
    5.24 +Goal "[| Gets B X : set evs; evs : otway |] ==> EX A. Says A B X : set evs";
    5.25 +by (etac rev_mp 1);
    5.26 +by (etac otway.induct 1);
    5.27 +by Auto_tac;
    5.28 +qed"Gets_imp_Says";
    5.29 +
    5.30 +(*Must be proved separately for each protocol*)
    5.31 +Goal "[| Gets B X : set evs; evs : otway |]  ==> X : knows Spy evs";
    5.32 +by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1);
    5.33 +qed"Gets_imp_knows_Spy";
    5.34 +AddDs [Gets_imp_knows_Spy RS parts.Inj];
    5.35 +
    5.36  
    5.37  (**** Inductive proofs about otway ****)
    5.38  
    5.39  (** For reasoning about the encrypted portion of messages **)
    5.40  
    5.41 -Goal "Says S' B {|X, Crypt(shrK B) X'|} : set evs ==> \
    5.42 -\          X : analz (spies evs)";
    5.43 -by (dtac (Says_imp_spies RS analz.Inj) 1);
    5.44 -by (Blast_tac 1);
    5.45 -qed "OR4_analz_spies";
    5.46 +Goal "[| Gets B {|X, Crypt(shrK B) X'|} : set evs;  evs : otway |] ==> \
    5.47 +\          X : analz (knows Spy evs)";
    5.48 +by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);
    5.49 +qed "OR4_analz_knows_Spy";
    5.50  
    5.51 -Goal "Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
    5.52 -\            : set evs ==> K : parts (spies evs)";
    5.53 +Goal "Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} : set evs \
    5.54 +\     ==> K : parts (knows Spy evs)";
    5.55  by (Blast_tac 1);
    5.56 -qed "Oops_parts_spies";
    5.57 +qed "Oops_parts_knows_Spy";
    5.58  
    5.59 -bind_thm ("OR4_parts_spies",
    5.60 -          OR4_analz_spies RS (impOfSubs analz_subset_parts));
    5.61 +bind_thm ("OR4_parts_knows_Spy",
    5.62 +          OR4_analz_knows_Spy RS (impOfSubs analz_subset_parts));
    5.63  
    5.64 -(*For proving the easier theorems about X ~: parts (spies evs).*)
    5.65 +(*For proving the easier theorems about X ~: parts (knows Spy evs).*)
    5.66  fun parts_induct_tac i = 
    5.67      etac otway.induct i			THEN 
    5.68 -    forward_tac [Oops_parts_spies] (i+6) THEN
    5.69 -    forward_tac [OR4_parts_spies]  (i+5) THEN
    5.70 +    forward_tac [Oops_parts_knows_Spy] (i+7) THEN
    5.71 +    forward_tac [OR4_parts_knows_Spy]  (i+6) THEN
    5.72      prove_simple_subgoals_tac  i;
    5.73  
    5.74  
    5.75 -(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
    5.76 +(** Theorems of the form X ~: parts (knows Spy evs) imply that NOBODY
    5.77      sends messages containing X! **)
    5.78  
    5.79  (*Spy never sees a good agent's shared key!*)
    5.80 -Goal "evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    5.81 +Goal "evs : otway ==> (Key (shrK A) : parts (knows Spy evs)) = (A : bad)";
    5.82  by (parts_induct_tac 1);
    5.83  by (ALLGOALS Blast_tac);
    5.84  qed "Spy_see_shrK";
    5.85  Addsimps [Spy_see_shrK];
    5.86  
    5.87 -Goal "evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
    5.88 +Goal "evs : otway ==> (Key (shrK A) : analz (knows Spy evs)) = (A : bad)";
    5.89  by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
    5.90  qed "Spy_analz_shrK";
    5.91  Addsimps [Spy_analz_shrK];
    5.92 @@ -74,7 +88,7 @@
    5.93  
    5.94  
    5.95  (*Nobody can have used non-existent keys!*)
    5.96 -Goal "evs : otway ==> Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
    5.97 +Goal "evs : otway ==> Key K ~: used evs --> K ~: keysFor (parts (knows Spy evs))";
    5.98  by (parts_induct_tac 1);
    5.99  (*Fake*)
   5.100  by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
   5.101 @@ -107,18 +121,17 @@
   5.102  
   5.103  
   5.104  (*For proofs involving analz.*)
   5.105 -val analz_spies_tac = 
   5.106 -    dtac OR4_analz_spies 6 THEN
   5.107 -    forward_tac [Says_Server_message_form] 7 THEN
   5.108 -    assume_tac 7 THEN
   5.109 -    REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
   5.110 +val analz_knows_Spy_tac = 
   5.111 +    dtac OR4_analz_knows_Spy 7 THEN assume_tac 7 THEN
   5.112 +    forward_tac [Says_Server_message_form] 8 THEN assume_tac 8 THEN
   5.113 +    REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 8);
   5.114  
   5.115  
   5.116  (****
   5.117   The following is to prove theorems of the form
   5.118  
   5.119 -  Key K : analz (insert (Key KAB) (spies evs)) ==>
   5.120 -  Key K : analz (spies evs)
   5.121 +  Key K : analz (insert (Key KAB) (knows Spy evs)) ==>
   5.122 +  Key K : analz (knows Spy evs)
   5.123  
   5.124   A more general formula must be proved inductively.
   5.125  ****)
   5.126 @@ -129,10 +142,10 @@
   5.127  (*The equality makes the induction hypothesis easier to apply*)
   5.128  Goal "evs : otway ==>                                 \
   5.129  \  ALL K KK. KK <= -(range shrK) -->                  \
   5.130 -\         (Key K : analz (Key``KK Un (spies evs))) =  \
   5.131 -\         (K : KK | Key K : analz (spies evs))";
   5.132 +\         (Key K : analz (Key``KK Un (knows Spy evs))) =  \
   5.133 +\         (K : KK | Key K : analz (knows Spy evs))";
   5.134  by (etac otway.induct 1);
   5.135 -by analz_spies_tac;
   5.136 +by analz_knows_Spy_tac;
   5.137  by (REPEAT_FIRST (resolve_tac [allI, impI]));
   5.138  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
   5.139  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   5.140 @@ -142,8 +155,8 @@
   5.141  
   5.142  
   5.143  Goal "[| evs : otway;  KAB ~: range shrK |] ==>       \
   5.144 -\     Key K : analz (insert (Key KAB) (spies evs)) =  \
   5.145 -\     (K = KAB | Key K : analz (spies evs))";
   5.146 +\     Key K : analz (insert (Key KAB) (knows Spy evs)) =  \
   5.147 +\     (K = KAB | Key K : analz (knows Spy evs))";
   5.148  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   5.149  qed "analz_insert_freshK";
   5.150  
   5.151 @@ -165,7 +178,7 @@
   5.152  by (expand_case_tac "K = ?y" 1);
   5.153  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   5.154  (*...we assume X is a recent message and handle this case by contradiction*)
   5.155 -by (blast_tac (claset() addSEs spies_partsEs) 1);
   5.156 +by (blast_tac (claset() addSEs knows_Spy_partsEs) 1);
   5.157  val lemma = result();
   5.158  
   5.159  
   5.160 @@ -188,7 +201,7 @@
   5.161  
   5.162  (*If the encrypted message appears then it originated with the Server!*)
   5.163  Goal "[| A ~: bad;  A ~= B;  evs : otway |]                 \
   5.164 -\     ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} : parts (spies evs) \
   5.165 +\     ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} : parts (knows Spy evs) \
   5.166  \      --> (EX NB. Says Server B                                          \
   5.167  \                   {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   5.168  \                     Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   5.169 @@ -203,7 +216,7 @@
   5.170  
   5.171  (*Corollary: if A receives B's OR4 message then it originated with the Server.
   5.172    Freshness may be inferred from nonce NA.*)
   5.173 -Goal "[| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
   5.174 +Goal "[| Gets A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
   5.175  \         : set evs;                                                 \
   5.176  \        A ~: bad;  A ~= B;  evs : otway |]                          \
   5.177  \     ==> EX NB. Says Server B                                       \
   5.178 @@ -224,9 +237,9 @@
   5.179  \            Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
   5.180  \         : set evs -->                                         \
   5.181  \         Notes Spy {|NA, NB, Key K|} ~: set evs -->            \
   5.182 -\         Key K ~: analz (spies evs)";
   5.183 +\         Key K ~: analz (knows Spy evs)";
   5.184  by (etac otway.induct 1);
   5.185 -by analz_spies_tac;
   5.186 +by analz_knows_Spy_tac;
   5.187  by (ALLGOALS
   5.188      (asm_simp_tac (simpset() addcongs [conj_cong, if_weak_cong] 
   5.189                               addsimps [analz_insert_eq, analz_insert_freshK]
   5.190 @@ -247,7 +260,7 @@
   5.191  \          : set evs;                                            \
   5.192  \        Notes Spy {|NA, NB, Key K|} ~: set evs;                 \
   5.193  \        A ~: bad;  B ~: bad;  evs : otway |]                    \
   5.194 -\     ==> Key K ~: analz (spies evs)";
   5.195 +\     ==> Key K ~: analz (knows Spy evs)";
   5.196  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   5.197  by (blast_tac (claset() addSEs [lemma]) 1);
   5.198  qed "Spy_not_see_encrypted_key";
   5.199 @@ -255,11 +268,11 @@
   5.200  
   5.201  (*A's guarantee.  The Oops premise quantifies over NB because A cannot know
   5.202    what it is.*)
   5.203 -Goal "[| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
   5.204 +Goal "[| Gets A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
   5.205  \         : set evs;                                                 \
   5.206  \        ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs;             \
   5.207  \        A ~: bad;  B ~: bad;  A ~= B;  evs : otway |]               \
   5.208 -\     ==> Key K ~: analz (spies evs)";
   5.209 +\     ==> Key K ~: analz (knows Spy evs)";
   5.210  by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1);
   5.211  qed "A_gets_good_key";
   5.212  
   5.213 @@ -268,7 +281,7 @@
   5.214  
   5.215  (*If the encrypted message appears then it originated with the Server!*)
   5.216  Goal "[| B ~: bad;  A ~= B;  evs : otway |]                              \
   5.217 -\ ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} : parts (spies evs) \
   5.218 +\ ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} : parts (knows Spy evs) \
   5.219  \     --> (EX NA. Says Server B                                          \
   5.220  \                  {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   5.221  \                    Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   5.222 @@ -283,7 +296,7 @@
   5.223  
   5.224  (*Guarantee for B: if it gets a well-formed certificate then the Server
   5.225    has sent the correct message in round 3.*)
   5.226 -Goal "[| Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
   5.227 +Goal "[| Gets B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
   5.228  \          : set evs;                                                    \
   5.229  \        B ~: bad;  A ~= B;  evs : otway |]                              \
   5.230  \     ==> EX NA. Says Server B                                           \
   5.231 @@ -295,10 +308,10 @@
   5.232  
   5.233  
   5.234  (*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*)
   5.235 -Goal "[| Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
   5.236 +Goal "[| Gets B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
   5.237  \         : set evs;                                                     \
   5.238  \        ALL NA. Notes Spy {|NA, NB, Key K|} ~: set evs;                 \
   5.239  \        A ~: bad;  B ~: bad;  A ~= B;  evs : otway |]                   \
   5.240 -\     ==> Key K ~: analz (spies evs)";
   5.241 +\     ==> Key K ~: analz (knows Spy evs)";
   5.242  by (blast_tac (claset() addDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1);
   5.243  qed "B_gets_good_key";
     6.1 --- a/src/HOL/Auth/OtwayRees_AN.thy	Mon Mar 08 13:49:53 1999 +0100
     6.2 +++ b/src/HOL/Auth/OtwayRees_AN.thy	Tue Mar 09 11:01:39 1999 +0100
     6.3 @@ -28,9 +28,14 @@
     6.4           (*The spy MAY say anything he CAN say.  We do not expect him to
     6.5             invent new nonces here, but he can also use NS1.  Common to
     6.6             all similar protocols.*)
     6.7 -    Fake "[| evs: otway;  X: synth (analz (spies evs)) |]
     6.8 +    Fake "[| evs: otway;  X: synth (analz (knows Spy evs)) |]
     6.9            ==> Says Spy B X  # evs : otway"
    6.10  
    6.11 +         (*A message that has been sent can be received by the
    6.12 +           intended recipient.*)
    6.13 +    Reception "[| evsr: otway;  Says A B X : set evsr |]
    6.14 +               ==> Gets B X # evsr : otway"
    6.15 +
    6.16           (*Alice initiates a protocol run*)
    6.17      OR1  "[| evs1: otway |]
    6.18            ==> Says A B {|Agent A, Agent B, Nonce NA|} # evs1 : otway"
    6.19 @@ -38,14 +43,14 @@
    6.20           (*Bob's response to Alice's message.  Bob doesn't know who 
    6.21  	   the sender is, hence the A' in the sender field.*)
    6.22      OR2  "[| evs2: otway;  
    6.23 -             Says A' B {|Agent A, Agent B, Nonce NA|} : set evs2 |]
    6.24 +             Gets B {|Agent A, Agent B, Nonce NA|} : set evs2 |]
    6.25            ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
    6.26                   # evs2 : otway"
    6.27  
    6.28           (*The Server receives Bob's message.  Then he sends a new
    6.29             session key to Bob with a packet for forwarding to Alice.*)
    6.30      OR3  "[| evs3: otway;  Key KAB ~: used evs3;
    6.31 -             Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
    6.32 +             Gets Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
    6.33                 : set evs3 |]
    6.34            ==> Says Server B 
    6.35                 {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key KAB|},
    6.36 @@ -57,7 +62,7 @@
    6.37             Need B ~= Server because we allow messages to self.*)
    6.38      OR4  "[| evs4: otway;  B ~= Server; 
    6.39               Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} : set evs4;
    6.40 -             Says S' B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
    6.41 +             Gets B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
    6.42                 : set evs4 |]
    6.43            ==> Says B A X # evs4 : otway"
    6.44  
     7.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Mon Mar 08 13:49:53 1999 +0100
     7.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Tue Mar 09 11:01:39 1999 +0100
     7.3 @@ -15,7 +15,7 @@
     7.4  indicates the possibility of this attack.
     7.5  *)
     7.6  
     7.7 -AddEs spies_partsEs;
     7.8 +AddEs knows_Spy_partsEs;
     7.9  AddDs [impOfSubs analz_subset_parts];
    7.10  AddDs [impOfSubs Fake_parts_insert];
    7.11  
    7.12 @@ -26,58 +26,71 @@
    7.13  \           Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
    7.14  \             : set evs";
    7.15  by (REPEAT (resolve_tac [exI,bexI] 1));
    7.16 -by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
    7.17 +by (rtac (otway.Nil RS 
    7.18 +          otway.OR1 RS otway.Reception RS
    7.19 +          otway.OR2 RS otway.Reception RS 
    7.20 +          otway.OR3 RS otway.Reception RS otway.OR4) 2);
    7.21  by possibility_tac;
    7.22  result();
    7.23  
    7.24 +Goal "[| Gets B X : set evs; evs : otway |] ==> EX A. Says A B X : set evs";
    7.25 +by (etac rev_mp 1);
    7.26 +by (etac otway.induct 1);
    7.27 +by Auto_tac;
    7.28 +qed"Gets_imp_Says";
    7.29 +
    7.30 +(*Must be proved separately for each protocol*)
    7.31 +Goal "[| Gets B X : set evs; evs : otway |]  ==> X : knows Spy evs";
    7.32 +by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1);
    7.33 +qed"Gets_imp_knows_Spy";
    7.34 +AddDs [Gets_imp_knows_Spy RS parts.Inj];
    7.35 +
    7.36  
    7.37  (**** Inductive proofs about otway ****)
    7.38  
    7.39  
    7.40  (** For reasoning about the encrypted portion of messages **)
    7.41  
    7.42 -Goal "Says A' B {|N, Agent A, Agent B, X|} : set evs \
    7.43 -\          ==> X : analz (spies evs)";
    7.44 -by (dtac (Says_imp_spies RS analz.Inj) 1);
    7.45 -by (Blast_tac 1);
    7.46 -qed "OR2_analz_spies";
    7.47 +Goal "[| Gets B {|N, Agent A, Agent B, X|} : set evs;  evs : otway |] \
    7.48 +\     ==> X : analz (knows Spy evs)";
    7.49 +by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);
    7.50 +qed "OR2_analz_knows_Spy";
    7.51  
    7.52 -Goal "Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
    7.53 -\          ==> X : analz (spies evs)";
    7.54 -by (dtac (Says_imp_spies RS analz.Inj) 1);
    7.55 -by (Blast_tac 1);
    7.56 -qed "OR4_analz_spies";
    7.57 +Goal "[| Gets B {|N, X, Crypt (shrK B) X'|} : set evs;  evs : otway |] \
    7.58 +\     ==> X : analz (knows Spy evs)";
    7.59 +by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);
    7.60 +qed "OR4_analz_knows_Spy";
    7.61  
    7.62  Goal "Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
    7.63 -\          ==> K : parts (spies evs)";
    7.64 +\     ==> K : parts (knows Spy evs)";
    7.65  by (Blast_tac 1);
    7.66 -qed "Oops_parts_spies";
    7.67 +qed "Oops_parts_knows_Spy";
    7.68  
    7.69 -bind_thm ("OR2_parts_spies",
    7.70 -          OR2_analz_spies RS (impOfSubs analz_subset_parts));
    7.71 -bind_thm ("OR4_parts_spies",
    7.72 -          OR4_analz_spies RS (impOfSubs analz_subset_parts));
    7.73 +bind_thm ("OR2_parts_knows_Spy",
    7.74 +          OR2_analz_knows_Spy RS (impOfSubs analz_subset_parts));
    7.75 +bind_thm ("OR4_parts_knows_Spy",
    7.76 +          OR4_analz_knows_Spy RS (impOfSubs analz_subset_parts));
    7.77  
    7.78 -(*For proving the easier theorems about X ~: parts (spies evs).*)
    7.79 +(*For proving the easier theorems about X ~: parts (knows Spy evs).*)
    7.80  fun parts_induct_tac i = 
    7.81      etac otway.induct i			THEN 
    7.82 -    forward_tac [Oops_parts_spies] (i+6) THEN
    7.83 -    forward_tac [OR4_parts_spies]  (i+5) THEN
    7.84 -    forward_tac [OR2_parts_spies]  (i+3) THEN 
    7.85 +    forward_tac [Oops_parts_knows_Spy] (i+7) THEN
    7.86 +    forward_tac [OR4_parts_knows_Spy]  (i+6) THEN
    7.87 +    forward_tac [OR2_parts_knows_Spy]  (i+4) THEN 
    7.88      prove_simple_subgoals_tac  i;
    7.89  
    7.90  
    7.91 -(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
    7.92 +(** Theorems of the form X ~: parts (knows Spy evs) imply that NOBODY
    7.93      sends messages containing X! **)
    7.94  
    7.95  (*Spy never sees a good agent's shared key!*)
    7.96 -Goal "evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    7.97 +Goal "evs : otway ==> (Key (shrK A) : parts (knows Spy evs)) = (A : bad)";
    7.98  by (parts_induct_tac 1);
    7.99  by (ALLGOALS Blast_tac);
   7.100  qed "Spy_see_shrK";
   7.101  Addsimps [Spy_see_shrK];
   7.102  
   7.103 -Goal "evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
   7.104 +Goal "evs : otway ==> (Key (shrK A) : analz (knows Spy evs)) = (A : bad)";
   7.105  by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
   7.106  qed "Spy_analz_shrK";
   7.107  Addsimps [Spy_analz_shrK];
   7.108 @@ -87,7 +100,7 @@
   7.109  
   7.110  
   7.111  (*Nobody can have used non-existent keys!*)
   7.112 -Goal "evs : otway ==> Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
   7.113 +Goal "evs : otway ==> Key K ~: used evs --> K ~: keysFor (parts (knows Spy evs))";
   7.114  by (parts_induct_tac 1);
   7.115  (*Fake*)
   7.116  by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
   7.117 @@ -118,18 +131,18 @@
   7.118  
   7.119  
   7.120  (*For proofs involving analz.*)
   7.121 -val analz_spies_tac = 
   7.122 -    dtac OR2_analz_spies 4 THEN 
   7.123 -    dtac OR4_analz_spies 6 THEN
   7.124 -    forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN
   7.125 -    REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
   7.126 +val analz_knows_Spy_tac = 
   7.127 +    dtac OR2_analz_knows_Spy 5 THEN assume_tac 5 THEN 
   7.128 +    dtac OR4_analz_knows_Spy 7 THEN assume_tac 7 THEN
   7.129 +    forward_tac [Says_Server_message_form] 8 THEN assume_tac 8 THEN
   7.130 +    REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 8);
   7.131  
   7.132  
   7.133  (****
   7.134   The following is to prove theorems of the form
   7.135  
   7.136 -  Key K : analz (insert (Key KAB) (spies evs)) ==>
   7.137 -  Key K : analz (spies evs)
   7.138 +  Key K : analz (insert (Key KAB) (knows Spy evs)) ==>
   7.139 +  Key K : analz (knows Spy evs)
   7.140  
   7.141   A more general formula must be proved inductively.
   7.142  ****)
   7.143 @@ -140,10 +153,10 @@
   7.144  (*The equality makes the induction hypothesis easier to apply*)
   7.145  Goal "evs : otway ==>                                 \
   7.146  \  ALL K KK. KK <= - (range shrK) -->                 \
   7.147 -\         (Key K : analz (Key``KK Un (spies evs))) =  \
   7.148 -\         (K : KK | Key K : analz (spies evs))";
   7.149 +\         (Key K : analz (Key``KK Un (knows Spy evs))) =  \
   7.150 +\         (K : KK | Key K : analz (knows Spy evs))";
   7.151  by (etac otway.induct 1);
   7.152 -by analz_spies_tac;
   7.153 +by analz_knows_Spy_tac;
   7.154  by (REPEAT_FIRST (resolve_tac [allI, impI]));
   7.155  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
   7.156  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   7.157 @@ -153,8 +166,8 @@
   7.158  
   7.159  
   7.160  Goal "[| evs : otway;  KAB ~: range shrK |] ==>       \
   7.161 -\     Key K : analz (insert (Key KAB) (spies evs)) =  \
   7.162 -\     (K = KAB | Key K : analz (spies evs))";
   7.163 +\     Key K : analz (insert (Key KAB) (knows Spy evs)) =  \
   7.164 +\     (K = KAB | Key K : analz (knows Spy evs))";
   7.165  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   7.166  qed "analz_insert_freshK";
   7.167  
   7.168 @@ -174,7 +187,7 @@
   7.169  by (expand_case_tac "K = ?y" 1);
   7.170  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   7.171  (*...we assume X is a recent message, and handle this case by contradiction*)
   7.172 -by (blast_tac (claset() addSEs spies_partsEs) 1);
   7.173 +by (blast_tac (claset() addSEs knows_Spy_partsEs) 1);
   7.174  val lemma = result();
   7.175  
   7.176  Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}   : set evs; \ 
   7.177 @@ -193,9 +206,9 @@
   7.178  \           {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   7.179  \             Crypt (shrK B) {|NB, Key K|}|} : set evs -->         \
   7.180  \         Notes Spy {|NA, NB, Key K|} ~: set evs -->               \
   7.181 -\         Key K ~: analz (spies evs)";
   7.182 +\         Key K ~: analz (knows Spy evs)";
   7.183  by (etac otway.induct 1);
   7.184 -by analz_spies_tac;
   7.185 +by analz_knows_Spy_tac;
   7.186  by (ALLGOALS
   7.187      (asm_simp_tac (simpset() addcongs [conj_cong] 
   7.188                               addsimps [analz_insert_eq, analz_insert_freshK]
   7.189 @@ -215,7 +228,7 @@
   7.190  \               Crypt (shrK B) {|NB, Key K|}|} : set evs;        \
   7.191  \        Notes Spy {|NA, NB, Key K|} ~: set evs;                 \
   7.192  \        A ~: bad;  B ~: bad;  evs : otway |]                    \
   7.193 -\     ==> Key K ~: analz (spies evs)";
   7.194 +\     ==> Key K ~: analz (knows Spy evs)";
   7.195  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   7.196  by (blast_tac (claset() addSEs [lemma]) 1);
   7.197  qed "Spy_not_see_encrypted_key";
   7.198 @@ -227,7 +240,7 @@
   7.199    The premise A ~= B prevents OR2's similar-looking cryptogram from being
   7.200    picked up.  Original Otway-Rees doesn't need it.*)
   7.201  Goal "[| A ~: bad;  A ~= B;  evs : otway |]                \
   7.202 -\     ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
   7.203 +\     ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (knows Spy evs) --> \
   7.204  \         Says A B {|NA, Agent A, Agent B,                  \
   7.205  \                    Crypt (shrK A) {|NA, Agent A, Agent B|}|}  : set evs";
   7.206  by (parts_induct_tac 1);
   7.207 @@ -236,11 +249,12 @@
   7.208  
   7.209  
   7.210  (*Crucial property: If the encrypted message appears, and A has used NA
   7.211 -  to start a run, then it originated with the Server!*)
   7.212 +  to start a run, then it originated with the Server!
   7.213 +  The premise A ~= B allows use of Crypt_imp_OR1*)
   7.214  (*Only it is FALSE.  Somebody could make a fake message to Server
   7.215            substituting some other nonce NA' for NB.*)
   7.216 -Goal "[| A ~: bad;  evs : otway |]                                \
   7.217 -\     ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs) -->    \
   7.218 +Goal "[| A ~: bad;  A ~= B;  evs : otway |]                                \
   7.219 +\     ==> Crypt (shrK A) {|NA, Key K|} : parts (knows Spy evs) -->    \
   7.220  \         Says A B {|NA, Agent A, Agent B,                        \
   7.221  \                    Crypt (shrK A) {|NA, Agent A, Agent B|}|}    \
   7.222  \          : set evs -->                                          \
   7.223 @@ -261,7 +275,7 @@
   7.224  (*OR3*)  (** LEVEL 5 **)
   7.225  (*The hypotheses at this point suggest an attack in which nonce NB is used
   7.226    in two different roles:
   7.227 -          Says B' Server
   7.228 +          Gets Server
   7.229             {|Nonce NA, Agent Aa, Agent A,
   7.230               Crypt (shrK Aa) {|Nonce NA, Agent Aa, Agent A|}, Nonce NB,
   7.231               Crypt (shrK A) {|Nonce NA, Agent Aa, Agent A|}|}
     8.1 --- a/src/HOL/Auth/OtwayRees_Bad.thy	Mon Mar 08 13:49:53 1999 +0100
     8.2 +++ b/src/HOL/Auth/OtwayRees_Bad.thy	Tue Mar 09 11:01:39 1999 +0100
     8.3 @@ -22,9 +22,14 @@
     8.4           (*The spy MAY say anything he CAN say.  We do not expect him to
     8.5             invent new nonces here, but he can also use NS1.  Common to
     8.6             all similar protocols.*)
     8.7 -    Fake "[| evs: otway;  X: synth (analz (spies evs)) |]
     8.8 +    Fake "[| evs: otway;  X: synth (analz (knows Spy evs)) |]
     8.9            ==> Says Spy B X  # evs : otway"
    8.10  
    8.11 +         (*A message that has been sent can be received by the
    8.12 +           intended recipient.*)
    8.13 +    Reception "[| evsr: otway;  Says A B X : set evsr |]
    8.14 +               ==> Gets B X # evsr : otway"
    8.15 +
    8.16           (*Alice initiates a protocol run*)
    8.17      OR1  "[| evs1: otway;  Nonce NA ~: used evs1 |]
    8.18            ==> Says A B {|Nonce NA, Agent A, Agent B, 
    8.19 @@ -35,7 +40,7 @@
    8.20  	   the sender is, hence the A' in the sender field.
    8.21             We modify the published protocol by NOT encrypting NB.*)
    8.22      OR2  "[| evs2: otway;  Nonce NB ~: used evs2;
    8.23 -             Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |]
    8.24 +             Gets B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |]
    8.25            ==> Says B Server 
    8.26                    {|Nonce NA, Agent A, Agent B, X, Nonce NB,
    8.27                      Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
    8.28 @@ -45,7 +50,7 @@
    8.29             match.  Then he sends a new session key to Bob with a packet for
    8.30             forwarding to Alice.*)
    8.31      OR3  "[| evs3: otway;  Key KAB ~: used evs3;
    8.32 -             Says B' Server 
    8.33 +             Gets Server 
    8.34                    {|Nonce NA, Agent A, Agent B, 
    8.35                      Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, 
    8.36                      Nonce NB, 
    8.37 @@ -60,11 +65,11 @@
    8.38           (*Bob receives the Server's (?) message and compares the Nonces with
    8.39  	   those in the message he previously sent the Server.
    8.40             Need B ~= Server because we allow messages to self.*)
    8.41 -    OR4  "[| evs4: otway;  A ~= B;  B ~= Server;
    8.42 +    OR4  "[| evs4: otway;  B ~= Server;
    8.43               Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB,
    8.44                               Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
    8.45                 : set evs4;
    8.46 -             Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
    8.47 +             Gets B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
    8.48                 : set evs4 |]
    8.49            ==> Says B A {|Nonce NA, X|} # evs4 : otway"
    8.50  
     9.1 --- a/src/HOL/Auth/Public.ML	Mon Mar 08 13:49:53 1999 +0100
     9.2 +++ b/src/HOL/Auth/Public.ML	Tue Mar 09 11:01:39 1999 +0100
     9.3 @@ -72,7 +72,7 @@
     9.4  Goal "Key (pubK A) : spies evs";
     9.5  by (induct_tac "evs" 1);
     9.6  by (ALLGOALS (asm_simp_tac
     9.7 -	      (simpset() addsimps [imageI, spies_Cons]
     9.8 +	      (simpset() addsimps [imageI, knows_Cons]
     9.9  	                addsplits [expand_event_case])));
    9.10  qed_spec_mp "spies_pubK";
    9.11  
    9.12 @@ -80,7 +80,7 @@
    9.13  Goal "A: bad ==> Key (priK A) : spies evs";
    9.14  by (induct_tac "evs" 1);
    9.15  by (ALLGOALS (asm_simp_tac
    9.16 -	      (simpset() addsimps [imageI, spies_Cons]
    9.17 +	      (simpset() addsimps [imageI, knows_Cons]
    9.18  	                addsplits [expand_event_case])));
    9.19  qed "Spy_spies_bad";
    9.20  
    10.1 --- a/src/HOL/Auth/Shared.ML	Mon Mar 08 13:49:53 1999 +0100
    10.2 +++ b/src/HOL/Auth/Shared.ML	Tue Mar 09 11:01:39 1999 +0100
    10.3 @@ -28,11 +28,11 @@
    10.4  (*Specialized to shared-key model: no need for addss in protocol proofs*)
    10.5  Goal "[| K: keysFor (parts (insert X H));  X : synth (analz H) |] \
    10.6  \              ==> K : keysFor (parts H) | Key K : parts H";
    10.7 -by (fast_tac
    10.8 +by (force_tac
    10.9        (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   10.10  			impOfSubs (analz_subset_parts RS keysFor_mono)]
   10.11 -		addIs  [impOfSubs analz_subset_parts]
   10.12 -                addss  (simpset())) 1);
   10.13 +		addIs  [impOfSubs analz_subset_parts],
   10.14 +       simpset()) 1);
   10.15  qed "keysFor_parts_insert";
   10.16  
   10.17  Goal "Crypt K X : H ==> K : keysFor H";
   10.18 @@ -41,22 +41,21 @@
   10.19  qed "Crypt_imp_keysFor";
   10.20  
   10.21  
   10.22 -(*** Function "spies" ***)
   10.23 +(*** Function "knows" ***)
   10.24  
   10.25  (*Spy sees shared keys of agents!*)
   10.26 -Goal "A: bad ==> Key (shrK A) : spies evs";
   10.27 +Goal "A: bad ==> Key (shrK A) : knows Spy evs";
   10.28  by (induct_tac "evs" 1);
   10.29  by (ALLGOALS (asm_simp_tac
   10.30 -	      (simpset() addsimps [imageI, spies_Cons]
   10.31 +	      (simpset() addsimps [imageI, knows_Cons]
   10.32  	                addsplits [expand_event_case])));
   10.33 -qed "Spy_spies_bad";
   10.34 -
   10.35 -AddSIs [Spy_spies_bad];
   10.36 +qed "Spy_knows_Spy_bad";
   10.37 +AddSIs [Spy_knows_Spy_bad];
   10.38  
   10.39  (*For not_bad_tac*)
   10.40 -Goal "[| Crypt (shrK A) X : analz (spies evs);  A: bad |] \
   10.41 -\              ==> X : analz (spies evs)";
   10.42 -by (fast_tac (claset() addSDs [analz.Decrypt] addss (simpset())) 1);
   10.43 +Goal "[| Crypt (shrK A) X : analz (knows Spy evs);  A: bad |] \
   10.44 +\              ==> X : analz (knows Spy evs)";
   10.45 +by (force_tac (claset() addSDs [analz.Decrypt], simpset()) 1);
   10.46  qed "Crypt_Spy_analz_bad";
   10.47  
   10.48  (*Prove that the agent is uncompromised by the confidentiality of 
   10.49 @@ -202,7 +201,8 @@
   10.50      such as  Nonce ?N ~: used evs that match Nonce_supply*)
   10.51  fun possibility_tac st = st |>
   10.52     (REPEAT 
   10.53 -    (ALLGOALS (simp_tac (simpset() delsimps [used_Says] setSolver safe_solver))
   10.54 +    (ALLGOALS (simp_tac (simpset() delsimps [used_Says, used_Notes, used_Gets] 
   10.55 +                         setSolver safe_solver))
   10.56       THEN
   10.57       REPEAT_FIRST (eq_assume_tac ORELSE' 
   10.58                     resolve_tac [refl, conjI, Nonce_supply, Key_supply])));
    11.1 --- a/src/HOL/Auth/TLS.ML	Mon Mar 08 13:49:53 1999 +0100
    11.2 +++ b/src/HOL/Auth/TLS.ML	Tue Mar 09 11:01:39 1999 +0100
    11.3 @@ -480,7 +480,7 @@
    11.4  (*ClientAccepts and ServerAccepts: because PMS was already visible*)
    11.5  by (REPEAT (blast_tac (claset() addDs [Spy_not_see_PMS, 
    11.6  				       Says_imp_spies RS analz.Inj,
    11.7 -				       Notes_imp_spies RS analz.Inj]) 6));
    11.8 +				       Notes_imp_knows_Spy RS analz.Inj]) 6));
    11.9  (*ClientHello*)
   11.10  by (Blast_tac 3);
   11.11  (*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)