converting more HOL-Auth to new-style theories
authorpaulson
Sat Apr 26 12:38:42 2003 +0200 (2003-04-26)
changeset 139266e62e5357a10
parent 13925 761af5c2fd59
child 13927 6643b8808812
converting more HOL-Auth to new-style theories
src/HOL/Auth/CertifiedEmail.thy
src/HOL/Auth/Event.thy
src/HOL/Auth/Event_lemmas.ML
src/HOL/Auth/KerberosIV.ML
src/HOL/Auth/Kerberos_BAN.ML
src/HOL/Auth/Kerberos_BAN.thy
src/HOL/Auth/Message.thy
src/HOL/Auth/Message_lemmas.ML
src/HOL/Auth/NS_Public.thy
src/HOL/Auth/NS_Shared.thy
src/HOL/Auth/Public.thy
src/HOL/Auth/Shared.thy
src/HOL/Auth/Yahalom.thy
src/HOL/Auth/Yahalom2.thy
src/HOL/Auth/Yahalom_Bad.thy
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/Auth/CertifiedEmail.thy	Sat Apr 26 12:38:17 2003 +0200
     1.2 +++ b/src/HOL/Auth/CertifiedEmail.thy	Sat Apr 26 12:38:42 2003 +0200
     1.3 @@ -16,8 +16,8 @@
     1.4    TTPVerKey  :: key
     1.5  
     1.6  translations
     1.7 -  "TTP"   == "Server"
     1.8 -  "RPwd"  == "shrK"
     1.9 +  "TTP"   == "Server "
    1.10 +  "RPwd"  == "shrK "
    1.11    "TTPDecKey" == "priEK Server"
    1.12    "TTPEncKey" == "pubEK Server" 
    1.13    "TTPSigKey" == "priSK Server"
    1.14 @@ -89,6 +89,7 @@
    1.15      TTP \<noteq> R';  hs' = hr';  k' \<in> symKeys|]
    1.16   ==> 
    1.17    Notes R' {|Agent TTP, Agent R', Key k', hr'|} # 
    1.18 +  Gets S (Crypt TTPSigKey S2TTP'') # 
    1.19    Says TTP S (Crypt TTPSigKey S2TTP'') # evs3 \<in> certified_mail"
    1.20  
    1.21  Reception:
    1.22 @@ -96,20 +97,6 @@
    1.23    ==> Gets B X#evsr \<in> certified_mail"
    1.24  
    1.25  
    1.26 -axioms
    1.27 -  (*Unlike the corresponding property of nonces, this cannot be proved.
    1.28 -    We have infinitely many agents and there is nothing to stop their
    1.29 -    long-term keys from exhausting all the natural numbers.  The axiom
    1.30 -    assumes that their keys are dispersed so as to leave room for infinitely
    1.31 -    many fresh session keys.  We could, alternatively, restrict agents to
    1.32 -    an unspecified finite number.  TOO STRONG.  REPLACE "used evs" BY
    1.33 -    used []*)
    1.34 -  Key_supply_ax:  "finite KK ==> \<exists>K\<in>symKeys. K \<notin> KK & Key K \<notin> used evs"
    1.35 -
    1.36 -
    1.37 -lemma Key_supply1: "\<exists>K\<in>symKeys. Key K \<notin> used evs"
    1.38 -by (rule Finites.emptyI [THEN Key_supply_ax, THEN bexE], blast)
    1.39 -
    1.40  (*A "possibility property": there are traces that reach the end*)
    1.41  lemma "\<exists>S2TTP. \<exists>evs \<in> certified_mail.
    1.42             Says TTP S (Crypt TTPSigKey S2TTP) \<in> set evs"
    1.43 @@ -374,7 +361,7 @@
    1.44  
    1.45  
    1.46  text{*Less easy to prove @{term "m'=m"}.  Maybe needs a separate unicity
    1.47 -theorem fror ciphertexts of the form @{term "Crypt K (Number m)"}, 
    1.48 +theorem for ciphertexts of the form @{term "Crypt K (Number m)"}, 
    1.49  where @{term K} is secure.*}
    1.50  lemma Key_unique_lemma [rule_format]:
    1.51       "evs \<in> certified_mail ==>
    1.52 @@ -399,7 +386,7 @@
    1.53  done
    1.54  
    1.55  text{*The key determines the sender, recipient and protocol options.*}
    1.56 -theorem Key_unique:
    1.57 +lemma Key_unique:
    1.58        "[|Says S R
    1.59             {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
    1.60               Number cleartext, Nonce q,
    1.61 @@ -415,9 +402,11 @@
    1.62         ==> R' = R & S' = S & AO' = AO & hs' = hs"
    1.63  by (rule Key_unique_lemma, assumption+)
    1.64  
    1.65 +subsection{*The Guarantees for Sender and Recipient*}
    1.66 +
    1.67  text{*If Spy gets the key then @{term R} is bad and also @{term S} at least
    1.68        gets his return receipt (and therefore has no grounds for complaint).*}
    1.69 -lemma Spy_see_encrypted_key_imp:
    1.70 +theorem Spy_see_encrypted_key_imp:
    1.71        "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO, 
    1.72                       Number cleartext, Nonce q, S2TTP|} \<in> set evs;
    1.73           Key K \<in> analz(knows Spy evs);
    1.74 @@ -455,8 +444,6 @@
    1.75  by (blast dest: Spy_see_encrypted_key_imp) 
    1.76  
    1.77  
    1.78 -subsection{*The Guarantees for Sender and Recipient*}
    1.79 -
    1.80  text{*Agent @{term R}, who may be the Spy, doesn't receive the key
    1.81   until @{term S} has access to the return receipt.*} 
    1.82  theorem S_guarantee:
     2.1 --- a/src/HOL/Auth/Event.thy	Sat Apr 26 12:38:17 2003 +0200
     2.2 +++ b/src/HOL/Auth/Event.thy	Sat Apr 26 12:38:42 2003 +0200
     2.3 @@ -11,8 +11,7 @@
     2.4      stores are visible to him
     2.5  *)
     2.6  
     2.7 -theory Event = Message
     2.8 -files ("Event_lemmas.ML"):
     2.9 +theory Event = Message:
    2.10  
    2.11  consts  (*Initial states of agents -- parameter of the construction*)
    2.12    initState :: "agent => msg set"
    2.13 @@ -74,43 +73,234 @@
    2.14    used_Nil:   "used []         = (UN B. parts (initState B))"
    2.15    used_Cons:  "used (ev # evs) =
    2.16  		     (case ev of
    2.17 -			Says A B X => parts {X} Un (used evs)
    2.18 +			Says A B X => parts {X} \<union> (used evs)
    2.19  		      | Gets A X   => used evs
    2.20 -		      | Notes A X  => parts {X} Un (used evs))"
    2.21 +		      | Notes A X  => parts {X} \<union> (used evs))"
    2.22  
    2.23  
    2.24 -lemma Notes_imp_used [rule_format]: "Notes A X : set evs --> X : used evs"
    2.25 -apply (induct_tac evs);
    2.26 +lemma Notes_imp_used [rule_format]: "Notes A X \<in> set evs --> X \<in> used evs"
    2.27 +apply (induct_tac evs)
    2.28  apply (auto split: event.split) 
    2.29  done
    2.30  
    2.31 -lemma Says_imp_used [rule_format]: "Says A B X : set evs --> X : used evs"
    2.32 -apply (induct_tac evs);
    2.33 +lemma Says_imp_used [rule_format]: "Says A B X \<in> set evs --> X \<in> used evs"
    2.34 +apply (induct_tac evs)
    2.35  apply (auto split: event.split) 
    2.36  done
    2.37  
    2.38  lemma MPair_used [rule_format]:
    2.39 -     "MPair X Y : used evs --> X : used evs & Y : used evs"
    2.40 -apply (induct_tac evs);
    2.41 +     "MPair X Y \<in> used evs --> X \<in> used evs & Y \<in> used evs"
    2.42 +apply (induct_tac evs)
    2.43  apply (auto split: event.split) 
    2.44  done
    2.45  
    2.46 -use "Event_lemmas.ML"
    2.47 +
    2.48 +subsection{*Function @{term knows}*}
    2.49 +
    2.50 +text{*Simplifying   @term{"parts (insert X (knows Spy evs))
    2.51 +      = parts {X} \<union> parts (knows Spy evs)"}.  The general case loops.*)
    2.52 +
    2.53 +text{*This version won't loop with the simplifier.*}
    2.54 +lemmas parts_insert_knows_Spy = parts_insert [of _ "knows Spy evs", standard]
    2.55 +
    2.56 +lemma knows_Spy_Says [simp]:
    2.57 +     "knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
    2.58 +by simp
    2.59 +
    2.60 +text{*The point of letting the Spy see "bad" agents' notes is to prevent
    2.61 +  redundant case-splits on whether A=Spy and whether A:bad*}
    2.62 +lemma knows_Spy_Notes [simp]:
    2.63 +     "knows Spy (Notes A X # evs) =  
    2.64 +          (if A:bad then insert X (knows Spy evs) else knows Spy evs)"
    2.65 +by simp
    2.66 +
    2.67 +lemma knows_Spy_Gets [simp]: "knows Spy (Gets A X # evs) = knows Spy evs"
    2.68 +by simp
    2.69 +
    2.70 +lemma knows_Spy_subset_knows_Spy_Says:
    2.71 +     "knows Spy evs <= knows Spy (Says A B X # evs)"
    2.72 +by (simp add: subset_insertI)
    2.73 +
    2.74 +lemma knows_Spy_subset_knows_Spy_Notes:
    2.75 +     "knows Spy evs <= knows Spy (Notes A X # evs)"
    2.76 +by force
    2.77 +
    2.78 +lemma knows_Spy_subset_knows_Spy_Gets:
    2.79 +     "knows Spy evs <= knows Spy (Gets A X # evs)"
    2.80 +by (simp add: subset_insertI)
    2.81 +
    2.82 +text{*Spy sees what is sent on the traffic*}
    2.83 +lemma Says_imp_knows_Spy [rule_format]:
    2.84 +     "Says A B X \<in> set evs --> X \<in> knows Spy evs"
    2.85 +apply (induct_tac "evs")
    2.86 +apply (simp_all (no_asm_simp) split add: event.split)
    2.87 +done
    2.88 +
    2.89 +lemma Notes_imp_knows_Spy [rule_format]:
    2.90 +     "Notes A X \<in> set evs --> A: bad --> X \<in> knows Spy evs"
    2.91 +apply (induct_tac "evs")
    2.92 +apply (simp_all (no_asm_simp) split add: event.split)
    2.93 +done
    2.94 +
    2.95 +
    2.96 +text{*Elimination rules: derive contradictions from old Says events containing
    2.97 +  items known to be fresh*}
    2.98 +lemmas knows_Spy_partsEs =
    2.99 +     Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard] 
   2.100 +     parts.Body [THEN revcut_rl, standard]
   2.101 +
   2.102 +text{*Compatibility for the old "spies" function*}
   2.103 +lemmas spies_partsEs = knows_Spy_partsEs
   2.104 +lemmas Says_imp_spies = Says_imp_knows_Spy
   2.105 +lemmas parts_insert_spies = parts_insert_knows_Spy
   2.106 +
   2.107 +
   2.108 +subsection{*Knowledge of Agents*}
   2.109 +
   2.110 +lemma knows_Says: "knows A (Says A B X # evs) = insert X (knows A evs)"
   2.111 +by simp
   2.112 +
   2.113 +lemma knows_Notes: "knows A (Notes A X # evs) = insert X (knows A evs)"
   2.114 +by simp
   2.115 +
   2.116 +lemma knows_Gets:
   2.117 +     "A \<noteq> Spy --> knows A (Gets A X # evs) = insert X (knows A evs)"
   2.118 +by simp
   2.119 +
   2.120 +
   2.121 +lemma knows_subset_knows_Says: "knows A evs <= knows A (Says A' B X # evs)"
   2.122 +apply (simp add: subset_insertI)
   2.123 +done
   2.124 +
   2.125 +lemma knows_subset_knows_Notes: "knows A evs <= knows A (Notes A' X # evs)"
   2.126 +apply (simp add: subset_insertI)
   2.127 +done
   2.128 +
   2.129 +lemma knows_subset_knows_Gets: "knows A evs <= knows A (Gets A' X # evs)"
   2.130 +apply (simp add: subset_insertI)
   2.131 +done
   2.132 +
   2.133 +text{*Agents know what they say*}
   2.134 +lemma Says_imp_knows [rule_format]: "Says A B X \<in> set evs --> X \<in> knows A evs"
   2.135 +apply (induct_tac "evs")
   2.136 +apply (simp_all (no_asm_simp) split add: event.split)
   2.137 +apply blast
   2.138 +done
   2.139 +
   2.140 +text{*Agents know what they note*}
   2.141 +lemma Notes_imp_knows [rule_format]: "Notes A X \<in> set evs --> X \<in> knows A evs"
   2.142 +apply (induct_tac "evs")
   2.143 +apply (simp_all (no_asm_simp) split add: event.split)
   2.144 +apply blast
   2.145 +done
   2.146 +
   2.147 +text{*Agents know what they receive*}
   2.148 +lemma Gets_imp_knows_agents [rule_format]:
   2.149 +     "A \<noteq> Spy --> Gets A X \<in> set evs --> X \<in> knows A evs"
   2.150 +apply (induct_tac "evs")
   2.151 +apply (simp_all (no_asm_simp) split add: event.split)
   2.152 +done
   2.153 +
   2.154 +
   2.155 +text{*What agents DIFFERENT FROM Spy know 
   2.156 +  was either said, or noted, or got, or known initially*}
   2.157 +lemma knows_imp_Says_Gets_Notes_initState [rule_format]:
   2.158 +     "[| X \<in> knows A evs; A \<noteq> Spy |] ==> EX B.  
   2.159 +  Says A B X \<in> set evs | Gets A X \<in> set evs | Notes A X \<in> set evs | X \<in> initState A"
   2.160 +apply (erule rev_mp)
   2.161 +apply (induct_tac "evs")
   2.162 +apply (simp_all (no_asm_simp) split add: event.split)
   2.163 +apply blast
   2.164 +done
   2.165 +
   2.166 +text{*What the Spy knows -- for the time being --
   2.167 +  was either said or noted, or known initially*}
   2.168 +lemma knows_Spy_imp_Says_Notes_initState [rule_format]:
   2.169 +     "[| X \<in> knows Spy evs |] ==> EX A B.  
   2.170 +  Says A B X \<in> set evs | Notes A X \<in> set evs | X \<in> initState Spy"
   2.171 +apply (erule rev_mp)
   2.172 +apply (induct_tac "evs")
   2.173 +apply (simp_all (no_asm_simp) split add: event.split)
   2.174 +apply blast
   2.175 +done
   2.176 +
   2.177 +
   2.178 +
   2.179 +
   2.180 +text{*NOTE REMOVAL--laws above are cleaner, as they don't involve "case"*}
   2.181 +declare knows_Cons [simp del]
   2.182 +
   2.183 +
   2.184 +subsection{*Fresh Nonces*}
   2.185 +
   2.186 +lemma parts_knows_Spy_subset_used: "parts (knows Spy evs) <= used evs"
   2.187 +apply (induct_tac "evs")
   2.188 +apply (simp_all (no_asm_simp) add: parts_insert_knows_Spy split add: event.split)
   2.189 +apply blast+
   2.190 +done
   2.191 +
   2.192 +lemmas usedI = parts_knows_Spy_subset_used [THEN subsetD, intro]
   2.193 +
   2.194 +lemma initState_into_used: "X \<in> parts (initState B) ==> X \<in> used evs"
   2.195 +apply (induct_tac "evs")
   2.196 +apply (simp_all (no_asm_simp) add: parts_insert_knows_Spy split add: event.split)
   2.197 +apply blast
   2.198 +done
   2.199 +
   2.200 +lemma used_Says [simp]: "used (Says A B X # evs) = parts{X} \<union> used evs"
   2.201 +by simp
   2.202 +
   2.203 +lemma used_Notes [simp]: "used (Notes A X # evs) = parts{X} \<union> used evs"
   2.204 +by simp
   2.205 +
   2.206 +lemma used_Gets [simp]: "used (Gets A X # evs) = used evs"
   2.207 +by simp
   2.208 +
   2.209 +lemma used_nil_subset: "used [] <= used evs"
   2.210 +apply (simp)
   2.211 +apply (blast intro: initState_into_used)
   2.212 +done
   2.213 +
   2.214 +text{*NOTE REMOVAL--laws above are cleaner, as they don't involve "case"*}
   2.215 +declare used_Nil [simp del] used_Cons [simp del]
   2.216 +
   2.217 +
   2.218 +text{*For proving theorems of the form @{term "X \<notin> analz (knows Spy evs) --> P"}
   2.219 +  New events added by induction to "evs" are discarded.  Provided 
   2.220 +  this information isn't needed, the proof will be much shorter, since
   2.221 +  it will omit complicated reasoning about @{term analz}.*}
   2.222 +
   2.223 +lemmas analz_mono_contra =
   2.224 +       knows_Spy_subset_knows_Spy_Says [THEN analz_mono, THEN contra_subsetD]
   2.225 +       knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD]
   2.226 +       knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD]
   2.227 +
   2.228 +ML
   2.229 +{*
   2.230 +val analz_mono_contra_tac = 
   2.231 +  let val analz_impI = inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
   2.232 +  in
   2.233 +    rtac analz_impI THEN' 
   2.234 +    REPEAT1 o 
   2.235 +      (dresolve_tac (thms"analz_mono_contra"))
   2.236 +    THEN' mp_tac
   2.237 +  end
   2.238 +*}
   2.239 +
   2.240  
   2.241  lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
   2.242  by (induct e, auto simp: knows_Cons)
   2.243  
   2.244  lemma initState_subset_knows: "initState A <= knows A evs"
   2.245 -apply (induct_tac evs)
   2.246 -apply (simp add: ); 
   2.247 +apply (induct_tac evs, simp) 
   2.248  apply (blast intro: knows_subset_knows_Cons [THEN subsetD])
   2.249  done
   2.250  
   2.251  
   2.252 -(*For proving new_keys_not_used*)
   2.253 +text{*For proving @{text new_keys_not_used}*}
   2.254  lemma keysFor_parts_insert:
   2.255 -     "[| K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) |] \
   2.256 -\     ==> K \<in> keysFor (parts (G Un H)) | Key (invKey K) \<in> parts H"; 
   2.257 +     "[| K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) |] 
   2.258 +      ==> K \<in> keysFor (parts (G \<union> H)) | Key (invKey K) \<in> parts H"; 
   2.259  by (force 
   2.260      dest!: parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD]
   2.261             analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD]
   2.262 @@ -125,10 +315,54 @@
   2.263  
   2.264  ML
   2.265  {*
   2.266 +val knows_Cons     = thm "knows_Cons"
   2.267 +val used_Nil       = thm "used_Nil"
   2.268 +val used_Cons      = thm "used_Cons"
   2.269 +
   2.270 +val Notes_imp_used = thm "Notes_imp_used";
   2.271 +val Says_imp_used = thm "Says_imp_used";
   2.272 +val MPair_used = thm "MPair_used";
   2.273 +val parts_insert_knows_Spy = thm "parts_insert_knows_Spy";
   2.274 +val knows_Spy_Says = thm "knows_Spy_Says";
   2.275 +val knows_Spy_Notes = thm "knows_Spy_Notes";
   2.276 +val knows_Spy_Gets = thm "knows_Spy_Gets";
   2.277 +val knows_Spy_subset_knows_Spy_Says = thm "knows_Spy_subset_knows_Spy_Says";
   2.278 +val knows_Spy_subset_knows_Spy_Notes = thm "knows_Spy_subset_knows_Spy_Notes";
   2.279 +val knows_Spy_subset_knows_Spy_Gets = thm "knows_Spy_subset_knows_Spy_Gets";
   2.280 +val Says_imp_knows_Spy = thm "Says_imp_knows_Spy";
   2.281 +val Notes_imp_knows_Spy = thm "Notes_imp_knows_Spy";
   2.282 +val knows_Spy_partsEs = thms "knows_Spy_partsEs";
   2.283 +val spies_partsEs = thms "spies_partsEs";
   2.284 +val Says_imp_spies = thm "Says_imp_spies";
   2.285 +val parts_insert_spies = thm "parts_insert_spies";
   2.286 +val knows_Says = thm "knows_Says";
   2.287 +val knows_Notes = thm "knows_Notes";
   2.288 +val knows_Gets = thm "knows_Gets";
   2.289 +val knows_subset_knows_Says = thm "knows_subset_knows_Says";
   2.290 +val knows_subset_knows_Notes = thm "knows_subset_knows_Notes";
   2.291 +val knows_subset_knows_Gets = thm "knows_subset_knows_Gets";
   2.292 +val Says_imp_knows = thm "Says_imp_knows";
   2.293 +val Notes_imp_knows = thm "Notes_imp_knows";
   2.294 +val Gets_imp_knows_agents = thm "Gets_imp_knows_agents";
   2.295 +val knows_imp_Says_Gets_Notes_initState = thm "knows_imp_Says_Gets_Notes_initState";
   2.296 +val knows_Spy_imp_Says_Notes_initState = thm "knows_Spy_imp_Says_Notes_initState";
   2.297 +val parts_knows_Spy_subset_used = thm "parts_knows_Spy_subset_used";
   2.298 +val usedI = thm "usedI";
   2.299 +val initState_into_used = thm "initState_into_used";
   2.300 +val used_Says = thm "used_Says";
   2.301 +val used_Notes = thm "used_Notes";
   2.302 +val used_Gets = thm "used_Gets";
   2.303 +val used_nil_subset = thm "used_nil_subset";
   2.304 +val analz_mono_contra = thms "analz_mono_contra";
   2.305 +val knows_subset_knows_Cons = thm "knows_subset_knows_Cons";
   2.306 +val initState_subset_knows = thm "initState_subset_knows";
   2.307 +val keysFor_parts_insert = thm "keysFor_parts_insert";
   2.308 +
   2.309 +
   2.310  val synth_analz_mono = thm "synth_analz_mono";
   2.311  
   2.312  val synth_analz_mono_contra_tac = 
   2.313 -  let val syan_impI = inst "P" "?Y ~: synth (analz (knows Spy ?evs))" impI
   2.314 +  let val syan_impI = inst "P" "?Y \<notin> synth (analz (knows Spy ?evs))" impI
   2.315    in
   2.316      rtac syan_impI THEN' 
   2.317      REPEAT1 o 
     3.1 --- a/src/HOL/Auth/Event_lemmas.ML	Sat Apr 26 12:38:17 2003 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,232 +0,0 @@
     3.4 -(*  Title:      HOL/Auth/Event_lemmas
     3.5 -    ID:         $Id$
     3.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 -    Copyright   1996  University of Cambridge
     3.8 -*)
     3.9 -
    3.10 -
    3.11 -val knows_Cons     = thm "knows_Cons";
    3.12 -val used_Nil       = thm "used_Nil";
    3.13 -val used_Cons      = thm "used_Cons";
    3.14 -
    3.15 -
    3.16 -(*Inserted by default but later removed.  This declaration lets the file
    3.17 -  be re-loaded.*)
    3.18 -Addsimps [knows_Cons, used_Nil, used_Cons];
    3.19 -
    3.20 -(**** Function "knows" ****)
    3.21 -
    3.22 -(** Simplifying   parts (insert X (knows Spy evs))
    3.23 -      = parts {X} Un parts (knows Spy evs) -- since general case loops*)
    3.24 -
    3.25 -bind_thm ("parts_insert_knows_Spy",
    3.26 -	  inst "H" "knows Spy evs" parts_insert);
    3.27 -
    3.28 -
    3.29 -val expand_event_case = thm "event.split";
    3.30 -
    3.31 -Goal "knows Spy (Says A B X # evs) = insert X (knows Spy evs)";
    3.32 -by (Simp_tac 1);
    3.33 -qed "knows_Spy_Says";
    3.34 -
    3.35 -(*The point of letting the Spy see "bad" agents' notes is to prevent
    3.36 -  redundant case-splits on whether A=Spy and whether A:bad*)
    3.37 -Goal "knows Spy (Notes A X # evs) = \
    3.38 -\         (if A:bad then insert X (knows Spy evs) else knows Spy evs)";
    3.39 -by (Simp_tac 1);
    3.40 -qed "knows_Spy_Notes";
    3.41 -
    3.42 -Goal "knows Spy (Gets A X # evs) = knows Spy evs";
    3.43 -by (Simp_tac 1);
    3.44 -qed "knows_Spy_Gets";
    3.45 -
    3.46 -Goal "knows Spy evs <= knows Spy (Says A B X # evs)";
    3.47 -by (simp_tac (simpset() addsimps [subset_insertI]) 1);
    3.48 -qed "knows_Spy_subset_knows_Spy_Says";
    3.49 -
    3.50 -Goal "knows Spy evs <= knows Spy (Notes A X # evs)";
    3.51 -by (Simp_tac 1);
    3.52 -by (Fast_tac 1);
    3.53 -qed "knows_Spy_subset_knows_Spy_Notes";
    3.54 -
    3.55 -Goal "knows Spy evs <= knows Spy (Gets A X # evs)";
    3.56 -by (simp_tac (simpset() addsimps [subset_insertI]) 1);
    3.57 -qed "knows_Spy_subset_knows_Spy_Gets";
    3.58 -
    3.59 -(*Spy sees what is sent on the traffic*)
    3.60 -Goal "Says A B X : set evs --> X : knows Spy evs";
    3.61 -by (induct_tac "evs" 1);
    3.62 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
    3.63 -qed_spec_mp "Says_imp_knows_Spy";
    3.64 -
    3.65 -Goal "Notes A X : set evs --> A: bad --> X : knows Spy evs";
    3.66 -by (induct_tac "evs" 1);
    3.67 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
    3.68 -qed_spec_mp "Notes_imp_knows_Spy";
    3.69 -
    3.70 -
    3.71 -(*Use with addSEs to derive contradictions from old Says events containing
    3.72 -  items known to be fresh*)
    3.73 -bind_thms ("knows_Spy_partsEs", 
    3.74 -           map make_elim [Says_imp_knows_Spy RS parts.Inj, parts.Body]);
    3.75 -
    3.76 -Addsimps [knows_Spy_Says, knows_Spy_Notes, knows_Spy_Gets];
    3.77 -
    3.78 -
    3.79 -(*Begin lemmas about agents' knowledge*)
    3.80 -
    3.81 -Goal "knows A (Says A B X # evs) = insert X (knows A evs)";
    3.82 -by (Simp_tac 1);
    3.83 -qed "knows_Says";
    3.84 -
    3.85 -Goal "knows A (Notes A X # evs) = insert X (knows A evs)";
    3.86 -by (Simp_tac 1);
    3.87 -qed "knows_Notes";
    3.88 -
    3.89 -Goal "A ~= Spy --> knows A (Gets A X # evs) = insert X (knows A evs)";
    3.90 -by (Simp_tac 1);
    3.91 -qed "knows_Gets";
    3.92 -
    3.93 -
    3.94 -Goal "knows A evs <= knows A (Says A' B X # evs)";
    3.95 -by (simp_tac (simpset() addsimps [subset_insertI]) 1);
    3.96 -qed "knows_subset_knows_Says";
    3.97 -
    3.98 -Goal "knows A evs <= knows A (Notes A' X # evs)";
    3.99 -by (simp_tac (simpset() addsimps [subset_insertI]) 1);
   3.100 -qed "knows_subset_knows_Notes";
   3.101 -
   3.102 -Goal "knows A evs <= knows A (Gets A' X # evs)";
   3.103 -by (simp_tac (simpset() addsimps [subset_insertI]) 1);
   3.104 -qed "knows_subset_knows_Gets";
   3.105 -
   3.106 -(*Agents know what they say*)
   3.107 -Goal "Says A B X : set evs --> X : knows A evs";
   3.108 -by (induct_tac "evs" 1);
   3.109 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
   3.110 -by (Blast_tac 1);
   3.111 -qed_spec_mp "Says_imp_knows";
   3.112 -
   3.113 -(*Agents know what they note*)
   3.114 -Goal "Notes A X : set evs --> X : knows A evs";
   3.115 -by (induct_tac "evs" 1);
   3.116 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
   3.117 -by (Blast_tac 1);
   3.118 -qed_spec_mp "Notes_imp_knows";
   3.119 -
   3.120 -(*Agents know what they receive*)
   3.121 -Goal "A ~= Spy --> Gets A X : set evs --> X : knows A evs";
   3.122 -by (induct_tac "evs" 1);
   3.123 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
   3.124 -qed_spec_mp "Gets_imp_knows_agents";
   3.125 -
   3.126 -
   3.127 -(*What agents DIFFERENT FROM Spy know 
   3.128 -  was either said, or noted, or got, or known initially*)
   3.129 -Goal "[| X : knows A evs; A ~= Spy |] ==> EX B. \
   3.130 -\ Says A B X : set evs | Gets A X : set evs | Notes A X : set evs | X : initState A";
   3.131 -by (etac rev_mp 1);
   3.132 -by (induct_tac "evs" 1);
   3.133 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
   3.134 -by (Blast_tac 1);
   3.135 -qed_spec_mp "knows_imp_Says_Gets_Notes_initState";
   3.136 -
   3.137 -(*What the Spy knows -- for the time being --
   3.138 -  was either said or noted, or known initially*)
   3.139 -Goal "[| X : knows Spy evs |] ==> EX A B. \
   3.140 -\ Says A B X : set evs | Notes A X : set evs | X : initState Spy";
   3.141 -by (etac rev_mp 1);
   3.142 -by (induct_tac "evs" 1);
   3.143 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
   3.144 -by (Blast_tac 1);
   3.145 -qed_spec_mp "knows_Spy_imp_Says_Notes_initState";
   3.146 -
   3.147 -(*END lemmas about agents' knowledge*)
   3.148 -
   3.149 -
   3.150 -
   3.151 -(**** NOTE REMOVAL--laws above are cleaner, as they don't involve "case" ****)
   3.152 -Delsimps [knows_Cons];   
   3.153 -
   3.154 -
   3.155 -(*** Fresh nonces ***)
   3.156 -
   3.157 -Goal "parts (knows Spy evs) <= used evs";
   3.158 -by (induct_tac "evs" 1);
   3.159 -by (ALLGOALS (asm_simp_tac
   3.160 -	      (simpset() addsimps [parts_insert_knows_Spy]
   3.161 -	                addsplits [expand_event_case])));
   3.162 -by (ALLGOALS Blast_tac);
   3.163 -qed "parts_knows_Spy_subset_used";
   3.164 -
   3.165 -bind_thm ("usedI", impOfSubs parts_knows_Spy_subset_used);
   3.166 -AddIs [usedI];
   3.167 -
   3.168 -Goal "parts (initState B) <= used evs";
   3.169 -by (induct_tac "evs" 1);
   3.170 -by (ALLGOALS (asm_simp_tac
   3.171 -	      (simpset() addsimps [parts_insert_knows_Spy]
   3.172 -	                addsplits [expand_event_case])));
   3.173 -by (ALLGOALS Blast_tac);
   3.174 -bind_thm ("initState_into_used", impOfSubs (result()));
   3.175 -
   3.176 -Goal "used (Says A B X # evs) = parts{X} Un used evs";
   3.177 -by (Simp_tac 1);
   3.178 -qed "used_Says";
   3.179 -Addsimps [used_Says];
   3.180 -
   3.181 -Goal "used (Notes A X # evs) = parts{X} Un used evs";
   3.182 -by (Simp_tac 1);
   3.183 -qed "used_Notes";
   3.184 -Addsimps [used_Notes];
   3.185 -
   3.186 -Goal "used (Gets A X # evs) = used evs";
   3.187 -by (Simp_tac 1);
   3.188 -qed "used_Gets";
   3.189 -Addsimps [used_Gets];
   3.190 -
   3.191 -Goal "used [] <= used evs";
   3.192 -by (Simp_tac 1);
   3.193 -by (blast_tac (claset() addIs [initState_into_used]) 1);
   3.194 -qed "used_nil_subset";
   3.195 -
   3.196 -(**** NOTE REMOVAL--laws above are cleaner, as they don't involve "case" ****)
   3.197 -Delsimps [used_Nil, used_Cons];   
   3.198 -
   3.199 -
   3.200 -(*For proving theorems of the form X ~: analz (knows Spy evs) --> P
   3.201 -  New events added by induction to "evs" are discarded.  Provided 
   3.202 -  this information isn't needed, the proof will be much shorter, since
   3.203 -  it will omit complicated reasoning about analz.*)
   3.204 -
   3.205 -bind_thms ("analz_mono_contra",
   3.206 -       [knows_Spy_subset_knows_Spy_Says RS analz_mono RS contra_subsetD,
   3.207 -        knows_Spy_subset_knows_Spy_Notes RS analz_mono RS contra_subsetD,
   3.208 -	knows_Spy_subset_knows_Spy_Gets RS analz_mono RS contra_subsetD]);
   3.209 -
   3.210 -val analz_mono_contra_tac = 
   3.211 -  let val analz_impI = inst "P" "?Y ~: analz (knows Spy ?evs)" impI
   3.212 -  in
   3.213 -    rtac analz_impI THEN' 
   3.214 -    REPEAT1 o 
   3.215 -      (dresolve_tac 
   3.216 -       [knows_Spy_subset_knows_Spy_Says RS analz_mono RS contra_subsetD,
   3.217 -        knows_Spy_subset_knows_Spy_Notes RS analz_mono RS contra_subsetD,
   3.218 -	knows_Spy_subset_knows_Spy_Gets RS analz_mono RS contra_subsetD])
   3.219 -    THEN'
   3.220 -    mp_tac
   3.221 -  end;
   3.222 -
   3.223 -fun Reception_tac i =
   3.224 -    blast_tac (claset() addDs [Says_imp_knows_Spy RS parts.Inj, 
   3.225 -                               impOfSubs (parts_insert RS equalityD1), 
   3.226 -			       parts_trans,
   3.227 -                               Says_imp_knows_Spy RS analz.Inj,
   3.228 -                               impOfSubs analz_mono, analz_cut] 
   3.229 -                        addIs [less_SucI]) i;
   3.230 -
   3.231 -
   3.232 -(*Compatibility for the old "spies" function*)
   3.233 -bind_thms ("spies_partsEs", knows_Spy_partsEs);
   3.234 -bind_thm ("Says_imp_spies", Says_imp_knows_Spy);
   3.235 -bind_thm ("parts_insert_spies", parts_insert_knows_Spy);
     4.1 --- a/src/HOL/Auth/KerberosIV.ML	Sat Apr 26 12:38:17 2003 +0200
     4.2 +++ b/src/HOL/Auth/KerberosIV.ML	Sat Apr 26 12:38:42 2003 +0200
     4.3 @@ -177,7 +177,7 @@
     4.4  \     Key K \\<notin> used evs --> K \\<notin> keysFor (parts (spies evs))";
     4.5  by (parts_induct_tac 1);
     4.6  (*Fake*)
     4.7 -by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
     4.8 +by (force_tac (claset() addSDs [keysFor_parts_insert], simpset()) 1);
     4.9  (*Others*)
    4.10  by (ALLGOALS Blast_tac);
    4.11  qed_spec_mp "new_keys_not_used";
     5.1 --- a/src/HOL/Auth/Kerberos_BAN.ML	Sat Apr 26 12:38:17 2003 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,359 +0,0 @@
     5.4 -(*  Title:      HOL/Auth/Kerberos_BAN
     5.5 -    ID:         $Id$
     5.6 -    Author:     Giampaolo Bella, Cambridge University Computer Laboratory
     5.7 -    Copyright   1998  University of Cambridge
     5.8 -
     5.9 -The Kerberos protocol, BAN version.
    5.10 -
    5.11 -From page 251 of
    5.12 -  Burrows, Abadi and Needham.  A Logic of Authentication.
    5.13 -  Proc. Royal Soc. 426 (1989)
    5.14 -
    5.15 -  Confidentiality (secrecy) and authentication properties rely on 
    5.16 -  temporal checks: strong guarantees in a little abstracted - but
    5.17 -  very realistic - model (see .thy).
    5.18 -
    5.19 -Tidied by lcp.
    5.20 -*)
    5.21 -
    5.22 -AddDs  [Says_imp_knows_Spy RS parts.Inj, parts.Body];
    5.23 -AddDs  [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert];
    5.24 -
    5.25 -AddIffs [SesKeyLife_LB, AutLife_LB];
    5.26 -
    5.27 -
    5.28 -(*A "possibility property": there are traces that reach the end.*)
    5.29 -Goal "\\<exists>Timestamp K. \\<exists>evs \\<in> kerberos_ban.    \
    5.30 -\            Says B A (Crypt K (Number Timestamp)) \
    5.31 -\                 \\<in> set evs";
    5.32 -by (cut_facts_tac [SesKeyLife_LB] 1);
    5.33 -by (REPEAT (resolve_tac [exI,bexI] 1));
    5.34 -by (rtac (kerberos_ban.Nil RS kerberos_ban.Kb1 RS kerberos_ban.Kb2 RS 
    5.35 -          kerberos_ban.Kb3 RS kerberos_ban.Kb4) 2);
    5.36 -by possibility_tac;
    5.37 -by (ALLGOALS Asm_simp_tac);
    5.38 -result();
    5.39 -
    5.40 -
    5.41 -
    5.42 -(**** Inductive proofs about kerberos_ban ****)
    5.43 -
    5.44 -(*Forwarding Lemma for reasoning about the encrypted portion of message Kb3*)
    5.45 -Goal "Says S A (Crypt KA {|Timestamp, B, K, X|}) \\<in> set evs \
    5.46 -\             ==> X \\<in> parts (spies evs)";
    5.47 -by (Blast_tac 1);
    5.48 -qed "Kb3_msg_in_parts_spies";
    5.49 -                              
    5.50 -Goal "Says Server A (Crypt (shrK A) {|Timestamp, B, K, X|}) \\<in> set evs \
    5.51 -\        ==> K \\<in> parts (spies evs)";
    5.52 -by (Blast_tac 1);
    5.53 -qed "Oops_parts_spies";
    5.54 -
    5.55 -(*For proving the easier theorems about X \\<notin> parts (spies evs).*)
    5.56 -fun parts_induct_tac i = 
    5.57 -    etac kerberos_ban.induct i  THEN 
    5.58 -    ftac Oops_parts_spies (i+6)  THEN
    5.59 -    ftac Kb3_msg_in_parts_spies (i+4)     THEN
    5.60 -    prove_simple_subgoals_tac i;
    5.61 -
    5.62 -
    5.63 -(*Spy never sees another agent's shared key! (unless it's bad at start)*)
    5.64 -Goal "evs \\<in> kerberos_ban ==> (Key (shrK A) \\<in> parts (spies evs)) = (A \\<in> bad)";
    5.65 -by (parts_induct_tac 1);
    5.66 -by (ALLGOALS Blast_tac);
    5.67 -qed "Spy_see_shrK";
    5.68 -Addsimps [Spy_see_shrK];
    5.69 -
    5.70 -
    5.71 -Goal "evs \\<in> kerberos_ban ==> (Key (shrK A) \\<in> analz (spies evs)) = (A \\<in> bad)";
    5.72 -by Auto_tac;
    5.73 -qed "Spy_analz_shrK";
    5.74 -Addsimps [Spy_analz_shrK];
    5.75 -
    5.76 -Goal  "[| Key (shrK A) \\<in> parts (spies evs);       \
    5.77 -\               evs \\<in> kerberos_ban |] ==> A:bad";
    5.78 -by (blast_tac (claset() addDs [Spy_see_shrK]) 1);
    5.79 -qed "Spy_see_shrK_D";
    5.80 -
    5.81 -bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
    5.82 -AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
    5.83 -
    5.84 -
    5.85 -(*Nobody can have used non-existent keys!*)
    5.86 -Goal "evs \\<in> kerberos_ban ==>      \
    5.87 -\      Key K \\<notin> used evs --> K \\<notin> keysFor (parts (spies evs))";
    5.88 -by (parts_induct_tac 1);
    5.89 -(*Fake*)
    5.90 -by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
    5.91 -(*Kb2, Kb3, Kb4*)
    5.92 -by (ALLGOALS Blast_tac);
    5.93 -qed_spec_mp "new_keys_not_used";
    5.94 -Addsimps [new_keys_not_used];
    5.95 -
    5.96 -(** Lemmas concerning the form of items passed in messages **)
    5.97 -
    5.98 -(*Describes the form of K, X and K' when the Server sends this message.*)
    5.99 -Goal "[| Says Server A (Crypt K' {|Number Ts, Agent B, Key K, X|})  \
   5.100 -\        \\<in> set evs; evs \\<in> kerberos_ban |]                           \
   5.101 -\     ==> K \\<notin> range shrK &                                         \
   5.102 -\         X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}) &      \
   5.103 -\         K' = shrK A";
   5.104 -by (etac rev_mp 1);
   5.105 -by (etac kerberos_ban.induct 1);
   5.106 -by Auto_tac;
   5.107 -qed "Says_Server_message_form";
   5.108 -
   5.109 -
   5.110 -(*If the encrypted message appears then it originated with the Server
   5.111 -  PROVIDED that A is NOT compromised!
   5.112 -
   5.113 -  This shows implicitly the FRESHNESS OF THE SESSION KEY to A
   5.114 -*)
   5.115 -Goal "[| Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} \
   5.116 -\          \\<in> parts (spies evs);                          \
   5.117 -\        A \\<notin> bad;  evs \\<in> kerberos_ban |]                \
   5.118 -\      ==> Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \
   5.119 -\            \\<in> set evs";
   5.120 -by (etac rev_mp 1);
   5.121 -by (parts_induct_tac 1);
   5.122 -by (Blast_tac 1);
   5.123 -qed "A_trusts_K_by_Kb2";
   5.124 -
   5.125 -
   5.126 -(*If the TICKET appears then it originated with the Server*)
   5.127 -(*FRESHNESS OF THE SESSION KEY to B*)
   5.128 -Goal "[| Crypt (shrK B) {|Number Ts, Agent A, Key K|} \\<in> parts (spies evs); \
   5.129 -\        B \\<notin> bad;  evs \\<in> kerberos_ban |]                        \
   5.130 -\      ==> Says Server A                                         \
   5.131 -\           (Crypt (shrK A) {|Number Ts, Agent B, Key K,                   \
   5.132 -\                         Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})  \
   5.133 -\          \\<in> set evs";
   5.134 -by (etac rev_mp 1);
   5.135 -by (parts_induct_tac 1);
   5.136 -by (Blast_tac 1);
   5.137 -qed "B_trusts_K_by_Kb3";
   5.138 -
   5.139 -
   5.140 -(*EITHER describes the form of X when the following message is sent, 
   5.141 -  OR     reduces it to the Fake case.
   5.142 -  Use Says_Server_message_form if applicable.*)
   5.143 -Goal "[| Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})     \
   5.144 -\           \\<in> set evs;                                                  \
   5.145 -\        evs \\<in> kerberos_ban |]                                          \
   5.146 -\==> (K \\<notin> range shrK & X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}))\
   5.147 -\         | X \\<in> analz (spies evs)";
   5.148 -by (case_tac "A \\<in> bad" 1);
   5.149 -by (fast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]
   5.150 -                      addss (simpset())) 1);
   5.151 -by (forward_tac [Says_imp_spies RS parts.Inj] 1);
   5.152 -by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2, 
   5.153 -				Says_Server_message_form]) 1);
   5.154 -qed "Says_S_message_form";
   5.155 -
   5.156 -
   5.157 -(*For proofs involving analz.*)
   5.158 -val analz_spies_tac = 
   5.159 -    ftac Says_Server_message_form 7 THEN
   5.160 -    ftac Says_S_message_form 5 THEN 
   5.161 -    REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac);
   5.162 -
   5.163 -
   5.164 -(****
   5.165 - The following is to prove theorems of the form
   5.166 -
   5.167 -  Key K \\<in> analz (insert (Key KAB) (spies evs)) ==>
   5.168 -  Key K \\<in> analz (spies evs)
   5.169 -
   5.170 - A more general formula must be proved inductively.
   5.171 -
   5.172 -****)
   5.173 -
   5.174 -
   5.175 -(** Session keys are not used to encrypt other session keys **)
   5.176 -
   5.177 -Goal "evs \\<in> kerberos_ban ==>                          \
   5.178 -\  \\<forall>K KK. KK <= - (range shrK) -->                 \
   5.179 -\         (Key K \\<in> analz (Key`KK Un (spies evs))) =  \
   5.180 -\         (K \\<in> KK | Key K \\<in> analz (spies evs))";
   5.181 -by (etac kerberos_ban.induct 1);
   5.182 -by analz_spies_tac;
   5.183 -by (REPEAT_FIRST (resolve_tac [allI, impI]));
   5.184 -by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
   5.185 -(*Takes 5 secs*)
   5.186 -by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   5.187 -(*Fake*) 
   5.188 -by (spy_analz_tac 1);
   5.189 -qed_spec_mp "analz_image_freshK";
   5.190 -
   5.191 -
   5.192 -Goal "[| evs \\<in> kerberos_ban;  KAB \\<notin> range shrK |] ==>     \
   5.193 -\     (Key K \\<in> analz (insert (Key KAB) (spies evs))) =       \
   5.194 -\     (K = KAB | Key K \\<in> analz (spies evs))";
   5.195 -by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   5.196 -qed "analz_insert_freshK";
   5.197 -
   5.198 -
   5.199 -(** The session key K uniquely identifies the message **)
   5.200 -
   5.201 -Goal "[| Says Server A                                    \
   5.202 -\          (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \\<in> set evs; \ 
   5.203 -\        Says Server A'                                   \
   5.204 -\         (Crypt (shrK A') {|Number Ts', Agent B', Key K, X'|}) \\<in> set evs;\
   5.205 -\        evs \\<in> kerberos_ban |] ==> A=A' & Ts=Ts' & B=B' & X = X'";
   5.206 -by (etac rev_mp 1);
   5.207 -by (etac rev_mp 1);
   5.208 -by (parts_induct_tac 1);
   5.209 -(*Kb2: it can't be a new key*)
   5.210 -by (Blast_tac 1);
   5.211 -qed "unique_session_keys";
   5.212 -
   5.213 -
   5.214 -(** Lemma: the session key sent in msg Kb2 would be EXPIRED
   5.215 -    if the spy could see it!
   5.216 -**)
   5.217 -
   5.218 -Goal "[| A \\<notin> bad;  B \\<notin> bad;  evs \\<in> kerberos_ban |]           \
   5.219 -\ ==> Says Server A                                            \
   5.220 -\         (Crypt (shrK A) {|Number Ts, Agent B, Key K,         \
   5.221 -\                           Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})\
   5.222 -\        \\<in> set evs -->                                         \
   5.223 -\     Key K \\<in> analz (spies evs) --> Expired Ts evs"; 
   5.224 -by (etac kerberos_ban.induct 1);
   5.225 -by analz_spies_tac;
   5.226 -by (ALLGOALS
   5.227 -    (asm_simp_tac (simpset() addsimps [less_SucI, analz_insert_eq, 
   5.228 -				       analz_insert_freshK] @ pushes)));
   5.229 -(*Oops: PROOF FAILED if addIs below*)
   5.230 -by (blast_tac (claset() addDs [unique_session_keys] addSIs [less_SucI]) 4);
   5.231 -(*Kb2*)
   5.232 -by (blast_tac (claset() addIs [parts_insertI, less_SucI]) 2);
   5.233 -(*Fake*) 
   5.234 -by (spy_analz_tac 1);
   5.235 -(**LEVEL 6 **)
   5.236 -(*Kb3*)
   5.237 -by (case_tac "Aa \\<in> bad" 1);
   5.238 -by (blast_tac (claset() addDs [A_trusts_K_by_Kb2, unique_session_keys]) 2);
   5.239 -by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj,
   5.240 -                               Crypt_Spy_analz_bad, analz.Fst, analz.Snd]
   5.241 -                        addIs [less_SucI]) 1);
   5.242 -qed_spec_mp "lemma2";
   5.243 -
   5.244 -
   5.245 -(** CONFIDENTIALITY for the SERVER:
   5.246 -                     Spy does not see the keys sent in msg Kb2 
   5.247 -                     as long as they have NOT EXPIRED
   5.248 -**)
   5.249 -Goal "[| Says Server A                                           \
   5.250 -\         (Crypt K' {|Number T, Agent B, Key K, X|}) \\<in> set evs;  \
   5.251 -\        ~ Expired T evs;                                        \
   5.252 -\        A \\<notin> bad;  B \\<notin> bad;  evs \\<in> kerberos_ban                \
   5.253 -\     |] ==> Key K \\<notin> analz (spies evs)";
   5.254 -by (ftac Says_Server_message_form 1 THEN assume_tac 1);
   5.255 -by (blast_tac (claset() addIs [lemma2]) 1);
   5.256 -qed "Confidentiality_S";
   5.257 -
   5.258 -(**** THE COUNTERPART OF CONFIDENTIALITY 
   5.259 -      [|...; Expired Ts evs; ...|] ==> Key K \\<in> analz (spies evs)
   5.260 -      WOULD HOLD ONLY IF AN OOPS OCCURRED! ---> Nothing to prove!   ****)
   5.261 -
   5.262 -
   5.263 -(** CONFIDENTIALITY for ALICE: **)
   5.264 -(** Also A_trusts_K_by_Kb2 RS Confidentiality_S **)
   5.265 -Goal "[| Crypt (shrK A) {|Number T, Agent B, Key K, X|} \\<in> parts (spies evs);\
   5.266 -\        ~ Expired T evs;          \
   5.267 -\        A \\<notin> bad;  B \\<notin> bad;  evs \\<in> kerberos_ban                \
   5.268 -\     |] ==> Key K \\<notin> analz (spies evs)";
   5.269 -by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2, Confidentiality_S]) 1);
   5.270 -qed "Confidentiality_A";
   5.271 -
   5.272 -
   5.273 -(** CONFIDENTIALITY for BOB: **)
   5.274 -(** Also B_trusts_K_by_Kb3 RS Confidentiality_S **)
   5.275 -Goal "[| Crypt (shrK B) {|Number Tk, Agent A, Key K|} \
   5.276 -\         \\<in> parts (spies evs);              \
   5.277 -\       ~ Expired Tk evs;          \
   5.278 -\       A \\<notin> bad;  B \\<notin> bad;  evs \\<in> kerberos_ban                \
   5.279 -\     |] ==> Key K \\<notin> analz (spies evs)";             
   5.280 -by (blast_tac (claset() addSDs [B_trusts_K_by_Kb3, 
   5.281 -                                Confidentiality_S]) 1);
   5.282 -qed "Confidentiality_B";
   5.283 -
   5.284 -
   5.285 -Goal "[| B \\<notin> bad;  evs \\<in> kerberos_ban |]                        \
   5.286 -\     ==> Key K \\<notin> analz (spies evs) -->                    \
   5.287 -\         Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \
   5.288 -\         \\<in> set evs -->                                             \
   5.289 -\         Crypt K (Number Ta) \\<in> parts (spies evs) -->        \
   5.290 -\         Says B A (Crypt K (Number Ta)) \\<in> set evs";
   5.291 -by (etac kerberos_ban.induct 1);
   5.292 -by (ftac Says_S_message_form 5 THEN assume_tac 5);     
   5.293 -by (dtac Kb3_msg_in_parts_spies 5);
   5.294 -by (ftac Oops_parts_spies 7);
   5.295 -by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
   5.296 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
   5.297 -(**LEVEL 6**)
   5.298 -by (Blast_tac 1);
   5.299 -by (Clarify_tac 1);
   5.300 -(*
   5.301 -Subgoal 1: contradiction from the assumptions  
   5.302 -Key K \\<notin> used evs2  and Crypt K (Number Ta) \\<in> parts (spies evs2)
   5.303 -*)
   5.304 -by (dtac Crypt_imp_invKey_keysFor 1);
   5.305 -by (Asm_full_simp_tac 1);
   5.306 -(* the two tactics above detect the contradiction*)
   5.307 -by (case_tac "Ba \\<in> bad" 1);  (*splits up the subgoal by the stated case*)
   5.308 -by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS 
   5.309 -                              B_trusts_K_by_Kb3, 
   5.310 -			      unique_session_keys]) 2);
   5.311 -by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS analz.Fst RS 
   5.312 -			      Crypt_Spy_analz_bad]) 1);
   5.313 -val lemma_B = result();
   5.314 -
   5.315 -
   5.316 -(*AUTHENTICATION OF B TO A*)
   5.317 -Goal "[| Crypt K (Number Ta) \\<in> parts (spies evs);           \
   5.318 -\        Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}    \
   5.319 -\        \\<in> parts (spies evs);                               \
   5.320 -\        ~ Expired Ts evs;                                  \
   5.321 -\        A \\<notin> bad;  B \\<notin> bad;  evs \\<in> kerberos_ban |]        \
   5.322 -\     ==> Says B A (Crypt K (Number Ta)) \\<in> set evs";
   5.323 -by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2]
   5.324 -                        addSIs [lemma_B RS mp RS mp RS mp]
   5.325 -                        addSEs [Confidentiality_S RSN (2,rev_notE)]) 1);
   5.326 -qed "Authentication_B";
   5.327 -
   5.328 -
   5.329 -Goal "[| A \\<notin> bad; B \\<notin> bad; evs \\<in> kerberos_ban |]      ==>         \ 
   5.330 -\        Key K \\<notin> analz (spies evs) -->         \
   5.331 -\        Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})  \
   5.332 -\        \\<in> set evs -->  \
   5.333 -\         Crypt K {|Agent A, Number Ta|} \\<in> parts (spies evs) -->\
   5.334 -\        Says A B {|X, Crypt K {|Agent A, Number Ta|}|}  \
   5.335 -\            \\<in> set evs";
   5.336 -by (etac kerberos_ban.induct 1);
   5.337 -by (ftac Says_S_message_form 5 THEN assume_tac 5);     
   5.338 -by (ftac Kb3_msg_in_parts_spies 5);
   5.339 -by (ftac Oops_parts_spies 7);
   5.340 -by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
   5.341 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
   5.342 -(**LEVEL 6**)
   5.343 -by (Blast_tac 1);
   5.344 -by (Clarify_tac 1);
   5.345 -by (dtac Crypt_imp_invKey_keysFor 1);
   5.346 -by (Asm_full_simp_tac 1);
   5.347 -by (blast_tac (claset() addDs [A_trusts_K_by_Kb2, unique_session_keys]) 1);
   5.348 -val lemma_A = result();
   5.349 -
   5.350 -
   5.351 -(*AUTHENTICATION OF A TO B*)
   5.352 -Goal "[| Crypt K {|Agent A, Number Ta|} \\<in> parts (spies evs);  \
   5.353 -\        Crypt (shrK B) {|Number Ts, Agent A, Key K|}         \
   5.354 -\        \\<in> parts (spies evs);                                 \
   5.355 -\        ~ Expired Ts evs;                                    \
   5.356 -\        A \\<notin> bad;  B \\<notin> bad;  evs \\<in> kerberos_ban |]          \
   5.357 -\     ==> Says A B {|Crypt (shrK B) {|Number Ts, Agent A, Key K|}, \    
   5.358 -\                    Crypt K {|Agent A, Number Ta|}|} \\<in> set evs";
   5.359 -by (blast_tac (claset() addSDs [B_trusts_K_by_Kb3]
   5.360 -                        addSIs [lemma_A RS mp RS mp RS mp]
   5.361 -                        addSEs [Confidentiality_S RSN (2,rev_notE)]) 1);
   5.362 -qed "Authentication_A";
     6.1 --- a/src/HOL/Auth/Kerberos_BAN.thy	Sat Apr 26 12:38:17 2003 +0200
     6.2 +++ b/src/HOL/Auth/Kerberos_BAN.thy	Sat Apr 26 12:38:42 2003 +0200
     6.3 @@ -8,17 +8,23 @@
     6.4  From page 251 of
     6.5    Burrows, Abadi and Needham.  A Logic of Authentication.
     6.6    Proc. Royal Soc. 426 (1989)
     6.7 +
     6.8 +  Confidentiality (secrecy) and authentication properties rely on 
     6.9 +  temporal checks: strong guarantees in a little abstracted - but
    6.10 +  very realistic - model (see .thy).
    6.11 +
    6.12 +Tidied and converted to Isar by lcp.
    6.13  *)
    6.14  
    6.15 -Kerberos_BAN = Shared + 
    6.16 +theory Kerberos_BAN = Shared:
    6.17  
    6.18  (* Temporal modelization: session keys can be leaked 
    6.19                            ONLY when they have expired *)
    6.20  
    6.21  syntax
    6.22 -    CT :: event list=>nat
    6.23 -    Expired :: [nat, event list] => bool
    6.24 -    RecentAuth :: [nat, event list] => bool
    6.25 +    CT :: "event list=>nat"
    6.26 +    Expired :: "[nat, event list] => bool"
    6.27 +    RecentAuth :: "[nat, event list] => bool"
    6.28  
    6.29  consts
    6.30  
    6.31 @@ -28,12 +34,12 @@
    6.32      (*Duration of the authenticator*)
    6.33      AutLife :: nat
    6.34  
    6.35 -rules
    6.36 +axioms
    6.37      (*The ticket should remain fresh for two journeys on the network at least*)
    6.38 -    SesKeyLife_LB "2 <= SesKeyLife"
    6.39 +    SesKeyLife_LB: "2 <= SesKeyLife"
    6.40  
    6.41      (*The authenticator only for one journey*)
    6.42 -    AutLife_LB    "Suc 0 <= AutLife"
    6.43 +    AutLife_LB:    "Suc 0 <= AutLife"
    6.44  
    6.45  translations
    6.46     "CT" == "length"
    6.47 @@ -42,51 +48,382 @@
    6.48  
    6.49     "RecentAuth T evs" == "CT evs <= AutLife + T"
    6.50  
    6.51 -consts  kerberos_ban   :: event list set
    6.52 +consts  kerberos_ban   :: "event list set"
    6.53  inductive "kerberos_ban"
    6.54 -  intrs 
    6.55 + intros 
    6.56 +
    6.57 +   Nil:  "[] \<in> kerberos_ban"
    6.58 +
    6.59 +   Fake: "[| evsf \<in> kerberos_ban;  X \<in> synth (analz (spies evsf)) |]
    6.60 +	  ==> Says Spy B X # evsf \<in> kerberos_ban"
    6.61 +
    6.62 +
    6.63 +   Kb1:  "[| evs1 \<in> kerberos_ban |]
    6.64 +	  ==> Says A Server {|Agent A, Agent B|} # evs1
    6.65 +		\<in>  kerberos_ban"
    6.66 +
    6.67 +
    6.68 +   Kb2:  "[| evs2 \<in> kerberos_ban;  Key KAB \<notin> used evs2;
    6.69 +	     Says A' Server {|Agent A, Agent B|} \<in> set evs2 |]
    6.70 +	  ==> Says Server A 
    6.71 +		(Crypt (shrK A)
    6.72 +		   {|Number (CT evs2), Agent B, Key KAB,  
    6.73 +		    (Crypt (shrK B) {|Number (CT evs2), Agent A, Key KAB|})|}) 
    6.74 +		# evs2 \<in> kerberos_ban"
    6.75 +
    6.76 +
    6.77 +   Kb3:  "[| evs3 \<in> kerberos_ban;  
    6.78 +	     Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) 
    6.79 +	       \<in> set evs3;
    6.80 +	     Says A Server {|Agent A, Agent B|} \<in> set evs3;
    6.81 +	     ~ Expired Ts evs3 |]
    6.82 +	  ==> Says A B {|X, Crypt K {|Agent A, Number (CT evs3)|} |} 
    6.83 +	       # evs3 \<in> kerberos_ban"
    6.84 +
    6.85 +
    6.86 +   Kb4:  "[| evs4 \<in> kerberos_ban;  
    6.87 +	     Says A' B {|(Crypt (shrK B) {|Number Ts, Agent A, Key K|}), 
    6.88 +			 (Crypt K {|Agent A, Number Ta|}) |}: set evs4;
    6.89 +	     ~ Expired Ts evs4;  RecentAuth Ta evs4 |]
    6.90 +	  ==> Says B A (Crypt K (Number Ta)) # evs4
    6.91 +		\<in> kerberos_ban"
    6.92  
    6.93 -    Nil  "[] \\<in> kerberos_ban"
    6.94 +	(*Old session keys may become compromised*)
    6.95 +   Oops: "[| evso \<in> kerberos_ban;  
    6.96 +	     Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
    6.97 +	       \<in> set evso;
    6.98 +	     Expired Ts evso |]
    6.99 +	  ==> Notes Spy {|Number Ts, Key K|} # evso \<in> kerberos_ban"
   6.100 +
   6.101 +
   6.102 +declare Says_imp_knows_Spy [THEN parts.Inj, dest] parts.Body [dest]
   6.103 +declare analz_subset_parts [THEN subsetD, dest]
   6.104 +declare Fake_parts_insert [THEN subsetD, dest]
   6.105 +
   6.106 +declare SesKeyLife_LB [iff] AutLife_LB [iff]
   6.107 +
   6.108  
   6.109 -    Fake "[| evsf \\<in> kerberos_ban;  X \\<in> synth (analz (spies evsf)) |]
   6.110 -          ==> Says Spy B X # evsf \\<in> kerberos_ban"
   6.111 +(*A "possibility property": there are traces that reach the end.*)
   6.112 +lemma "\<exists>Timestamp K. \<exists>evs \<in> kerberos_ban.     
   6.113 +             Says B A (Crypt K (Number Timestamp))  
   6.114 +                  \<in> set evs"
   6.115 +apply (cut_tac SesKeyLife_LB)
   6.116 +apply (intro exI bexI)
   6.117 +apply (rule_tac [2] 
   6.118 +           kerberos_ban.Nil [THEN kerberos_ban.Kb1, THEN kerberos_ban.Kb2, 
   6.119 +                             THEN kerberos_ban.Kb3, THEN kerberos_ban.Kb4], possibility)
   6.120 +apply (simp_all (no_asm_simp))
   6.121 +done
   6.122 +
   6.123 +
   6.124 +(**** Inductive proofs about kerberos_ban ****)
   6.125 +
   6.126 +(*Forwarding Lemma for reasoning about the encrypted portion of message Kb3*)
   6.127 +lemma Kb3_msg_in_parts_spies:
   6.128 +     "Says S A (Crypt KA {|Timestamp, B, K, X|}) \<in> set evs  
   6.129 +      ==> X \<in> parts (spies evs)"
   6.130 +by blast
   6.131 +                              
   6.132 +lemma Oops_parts_spies:
   6.133 +     "Says Server A (Crypt (shrK A) {|Timestamp, B, K, X|}) \<in> set evs  
   6.134 +      ==> K \<in> parts (spies evs)"
   6.135 +by blast
   6.136 +
   6.137 +
   6.138 +(*Spy never sees another agent's shared key! (unless it's bad at start)*)
   6.139 +lemma Spy_see_shrK [simp]:
   6.140 +     "evs \<in> kerberos_ban ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
   6.141 +apply (erule kerberos_ban.induct) 
   6.142 +apply (frule_tac [7] Oops_parts_spies) 
   6.143 +apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all)  
   6.144 +apply blast+
   6.145 +done
   6.146  
   6.147  
   6.148 -    Kb1  "[| evs1 \\<in> kerberos_ban |]
   6.149 -          ==> Says A Server {|Agent A, Agent B|} # evs1
   6.150 -                \\<in>  kerberos_ban"
   6.151 +lemma Spy_analz_shrK [simp]:
   6.152 +     "evs \<in> kerberos_ban ==> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
   6.153 +apply auto
   6.154 +done
   6.155 +
   6.156 +
   6.157 +lemma Spy_see_shrK_D [dest!]:
   6.158 +     "[| Key (shrK A) \<in> parts (spies evs);        
   6.159 +                evs \<in> kerberos_ban |] ==> A:bad"
   6.160 +apply (blast dest: Spy_see_shrK)
   6.161 +done
   6.162 +
   6.163 +lemmas Spy_analz_shrK_D = analz_subset_parts [THEN subsetD, THEN Spy_see_shrK_D,  dest!]
   6.164 +
   6.165 +
   6.166 +(*Nobody can have used non-existent keys!*)
   6.167 +lemma new_keys_not_used [rule_format, simp]:
   6.168 +     "evs \<in> kerberos_ban ==>       
   6.169 +       Key K \<notin> used evs --> K \<notin> keysFor (parts (spies evs))"
   6.170 +apply (erule kerberos_ban.induct) 
   6.171 +apply (frule_tac [7] Oops_parts_spies) 
   6.172 +apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all)  
   6.173 +(*Fake*)
   6.174 +apply (force dest!: keysFor_parts_insert)
   6.175 +(*Kb2, Kb3, Kb4*)
   6.176 +apply blast+
   6.177 +done
   6.178 +
   6.179 +(** Lemmas concerning the form of items passed in messages **)
   6.180 +
   6.181 +(*Describes the form of K, X and K' when the Server sends this message.*)
   6.182 +lemma Says_Server_message_form:
   6.183 +     "[| Says Server A (Crypt K' {|Number Ts, Agent B, Key K, X|})   
   6.184 +         \<in> set evs; evs \<in> kerberos_ban |]                            
   6.185 +      ==> K \<notin> range shrK &                                          
   6.186 +          X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}) &       
   6.187 +          K' = shrK A"
   6.188 +apply (erule rev_mp)
   6.189 +apply (erule kerberos_ban.induct, auto)
   6.190 +done
   6.191  
   6.192  
   6.193 -    Kb2  "[| evs2 \\<in> kerberos_ban;  Key KAB \\<notin> used evs2;
   6.194 -             Says A' Server {|Agent A, Agent B|} \\<in> set evs2 |]
   6.195 -          ==> Says Server A 
   6.196 -                (Crypt (shrK A)
   6.197 -                   {|Number (CT evs2), Agent B, Key KAB,  
   6.198 -                    (Crypt (shrK B) {|Number (CT evs2), Agent A, Key KAB|})|}) 
   6.199 -                # evs2 \\<in> kerberos_ban"
   6.200 +(*If the encrypted message appears then it originated with the Server
   6.201 +  PROVIDED that A is NOT compromised!
   6.202 +
   6.203 +  This shows implicitly the FRESHNESS OF THE SESSION KEY to A
   6.204 +*)
   6.205 +lemma A_trusts_K_by_Kb2:
   6.206 +     "[| Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}  
   6.207 +           \<in> parts (spies evs);                           
   6.208 +         A \<notin> bad;  evs \<in> kerberos_ban |]                 
   6.209 +       ==> Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})  
   6.210 +             \<in> set evs"
   6.211 +apply (erule rev_mp)
   6.212 +apply (erule kerberos_ban.induct) 
   6.213 +apply (frule_tac [7] Oops_parts_spies) 
   6.214 +apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all)  
   6.215 +apply blast
   6.216 +done
   6.217 +
   6.218 +
   6.219 +(*If the TICKET appears then it originated with the Server*)
   6.220 +(*FRESHNESS OF THE SESSION KEY to B*)
   6.221 +lemma B_trusts_K_by_Kb3:
   6.222 +     "[| Crypt (shrK B) {|Number Ts, Agent A, Key K|} \<in> parts (spies evs);  
   6.223 +         B \<notin> bad;  evs \<in> kerberos_ban |]                         
   6.224 +       ==> Says Server A                                          
   6.225 +            (Crypt (shrK A) {|Number Ts, Agent B, Key K,                    
   6.226 +                          Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})   
   6.227 +           \<in> set evs"
   6.228 +apply (erule rev_mp)
   6.229 +apply (erule kerberos_ban.induct) 
   6.230 +apply (frule_tac [7] Oops_parts_spies) 
   6.231 +apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all)  
   6.232 +apply blast
   6.233 +done
   6.234 +
   6.235 +
   6.236 +(*EITHER describes the form of X when the following message is sent, 
   6.237 +  OR     reduces it to the Fake case.
   6.238 +  Use Says_Server_message_form if applicable.*)
   6.239 +lemma Says_S_message_form:
   6.240 +     "[| Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})      
   6.241 +            \<in> set evs;                                                   
   6.242 +         evs \<in> kerberos_ban |]                                           
   6.243 + ==> (K \<notin> range shrK & X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|})) 
   6.244 +          | X \<in> analz (spies evs)"
   6.245 +apply (case_tac "A \<in> bad")
   6.246 +apply (force dest!: Says_imp_spies [THEN analz.Inj])
   6.247 +apply (frule Says_imp_spies [THEN parts.Inj])
   6.248 +apply (blast dest!: A_trusts_K_by_Kb2 Says_Server_message_form)
   6.249 +done
   6.250 +
   6.251  
   6.252  
   6.253 -    Kb3  "[| evs3 \\<in> kerberos_ban;  
   6.254 -             Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) 
   6.255 -               \\<in> set evs3;
   6.256 -             Says A Server {|Agent A, Agent B|} \\<in> set evs3;
   6.257 -             ~ Expired Ts evs3 |]
   6.258 -          ==> Says A B {|X, Crypt K {|Agent A, Number (CT evs3)|} |} 
   6.259 -               # evs3 \\<in> kerberos_ban"
   6.260 +(****
   6.261 + The following is to prove theorems of the form
   6.262 +
   6.263 +  Key K \<in> analz (insert (Key KAB) (spies evs)) ==>
   6.264 +  Key K \<in> analz (spies evs)
   6.265 +
   6.266 + A more general formula must be proved inductively.
   6.267 +
   6.268 +****)
   6.269 +
   6.270 +
   6.271 +(** Session keys are not used to encrypt other session keys **)
   6.272 +
   6.273 +lemma analz_image_freshK [rule_format (no_asm)]:
   6.274 +     "evs \<in> kerberos_ban ==>                           
   6.275 +   \<forall>K KK. KK <= - (range shrK) -->                  
   6.276 +          (Key K \<in> analz (Key`KK Un (spies evs))) =   
   6.277 +          (K \<in> KK | Key K \<in> analz (spies evs))"
   6.278 +apply (erule kerberos_ban.induct)
   6.279 +apply (drule_tac [7] Says_Server_message_form)
   6.280 +apply (erule_tac [5] Says_S_message_form [THEN disjE], analz_freshK, spy_analz)
   6.281 +done
   6.282 +
   6.283 +
   6.284 +
   6.285 +lemma analz_insert_freshK:
   6.286 +     "[| evs \<in> kerberos_ban;  KAB \<notin> range shrK |] ==>      
   6.287 +      (Key K \<in> analz (insert (Key KAB) (spies evs))) =        
   6.288 +      (K = KAB | Key K \<in> analz (spies evs))"
   6.289 +by (simp only: analz_image_freshK analz_image_freshK_simps)
   6.290 +
   6.291 +
   6.292 +(** The session key K uniquely identifies the message **)
   6.293 +
   6.294 +lemma unique_session_keys:
   6.295 +     "[| Says Server A                                     
   6.296 +           (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \<in> set evs;   
   6.297 +         Says Server A'                                    
   6.298 +          (Crypt (shrK A') {|Number Ts', Agent B', Key K, X'|}) \<in> set evs; 
   6.299 +         evs \<in> kerberos_ban |] ==> A=A' & Ts=Ts' & B=B' & X = X'"
   6.300 +apply (erule rev_mp)
   6.301 +apply (erule rev_mp)
   6.302 +apply (erule kerberos_ban.induct) 
   6.303 +apply (frule_tac [7] Oops_parts_spies) 
   6.304 +apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all)  
   6.305 +(*Kb2: it can't be a new key*)
   6.306 +apply blast
   6.307 +done
   6.308 +
   6.309 +
   6.310 +(** Lemma: the session key sent in msg Kb2 would be EXPIRED
   6.311 +    if the spy could see it!
   6.312 +**)
   6.313 +
   6.314 +lemma lemma2 [rule_format (no_asm)]:
   6.315 +     "[| A \<notin> bad;  B \<notin> bad;  evs \<in> kerberos_ban |]            
   6.316 +  ==> Says Server A                                             
   6.317 +          (Crypt (shrK A) {|Number Ts, Agent B, Key K,          
   6.318 +                            Crypt (shrK B) {|Number Ts, Agent A, Key K|}|}) 
   6.319 +         \<in> set evs -->                                          
   6.320 +      Key K \<in> analz (spies evs) --> Expired Ts evs"
   6.321 +apply (erule kerberos_ban.induct)
   6.322 +apply (frule_tac [7] Says_Server_message_form)
   6.323 +apply (frule_tac [5] Says_S_message_form [THEN disjE])
   6.324 +apply (simp_all (no_asm_simp) add: less_SucI analz_insert_eq analz_insert_freshK pushes)
   6.325 +txt{*Fake*}
   6.326 +apply spy_analz
   6.327 +txt{*Kb2*}
   6.328 +apply (blast intro: parts_insertI less_SucI)
   6.329 +txt{*Kb3*}
   6.330 +apply (case_tac "Aa \<in> bad")
   6.331 + prefer 2 apply (blast dest: A_trusts_K_by_Kb2 unique_session_keys)
   6.332 +apply (blast dest: Says_imp_spies [THEN analz.Inj] Crypt_Spy_analz_bad elim!: MPair_analz intro: less_SucI)
   6.333 +txt{*Oops: PROOF FAILED if addIs below*}
   6.334 +apply (blast dest: unique_session_keys intro!: less_SucI)
   6.335 +done
   6.336  
   6.337  
   6.338 -    Kb4  "[| evs4 \\<in> kerberos_ban;  
   6.339 -             Says A' B {|(Crypt (shrK B) {|Number Ts, Agent A, Key K|}), 
   6.340 -		         (Crypt K {|Agent A, Number Ta|}) |}: set evs4;
   6.341 -             ~ Expired Ts evs4;  RecentAuth Ta evs4 |]
   6.342 -          ==> Says B A (Crypt K (Number Ta)) # evs4
   6.343 -                \\<in> kerberos_ban"
   6.344 +(** CONFIDENTIALITY for the SERVER:
   6.345 +                     Spy does not see the keys sent in msg Kb2 
   6.346 +                     as long as they have NOT EXPIRED
   6.347 +**)
   6.348 +lemma Confidentiality_S:
   6.349 +     "[| Says Server A                                            
   6.350 +          (Crypt K' {|Number T, Agent B, Key K, X|}) \<in> set evs;   
   6.351 +         ~ Expired T evs;                                         
   6.352 +         A \<notin> bad;  B \<notin> bad;  evs \<in> kerberos_ban                 
   6.353 +      |] ==> Key K \<notin> analz (spies evs)"
   6.354 +apply (frule Says_Server_message_form, assumption)
   6.355 +apply (blast intro: lemma2)
   6.356 +done
   6.357 +
   6.358 +(**** THE COUNTERPART OF CONFIDENTIALITY 
   6.359 +      [|...; Expired Ts evs; ...|] ==> Key K \<in> analz (spies evs)
   6.360 +      WOULD HOLD ONLY IF AN OOPS OCCURRED! ---> Nothing to prove!   ****)
   6.361 +
   6.362 +
   6.363 +(** CONFIDENTIALITY for ALICE: **)
   6.364 +(** Also A_trusts_K_by_Kb2 RS Confidentiality_S **)
   6.365 +lemma Confidentiality_A:
   6.366 +     "[| Crypt (shrK A) {|Number T, Agent B, Key K, X|} \<in> parts (spies evs); 
   6.367 +         ~ Expired T evs;           
   6.368 +         A \<notin> bad;  B \<notin> bad;  evs \<in> kerberos_ban                 
   6.369 +      |] ==> Key K \<notin> analz (spies evs)"
   6.370 +apply (blast dest!: A_trusts_K_by_Kb2 Confidentiality_S)
   6.371 +done
   6.372 +
   6.373 +
   6.374 +(** CONFIDENTIALITY for BOB: **)
   6.375 +(** Also B_trusts_K_by_Kb3 RS Confidentiality_S **)
   6.376 +lemma Confidentiality_B:
   6.377 +     "[| Crypt (shrK B) {|Number Tk, Agent A, Key K|}  
   6.378 +          \<in> parts (spies evs);               
   6.379 +        ~ Expired Tk evs;           
   6.380 +        A \<notin> bad;  B \<notin> bad;  evs \<in> kerberos_ban                 
   6.381 +      |] ==> Key K \<notin> analz (spies evs)"
   6.382 +apply (blast dest!: B_trusts_K_by_Kb3 Confidentiality_S)
   6.383 +done
   6.384 +
   6.385  
   6.386 -         (*Old session keys may become compromised*)
   6.387 -    Oops "[| evso \\<in> kerberos_ban;  
   6.388 -             Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
   6.389 -               \\<in> set evso;
   6.390 -             Expired Ts evso |]
   6.391 -          ==> Notes Spy {|Number Ts, Key K|} # evso \\<in> kerberos_ban"
   6.392 +lemma lemma_B [rule_format]:
   6.393 +     "[| B \<notin> bad;  evs \<in> kerberos_ban |]                         
   6.394 +      ==> Key K \<notin> analz (spies evs) -->                     
   6.395 +          Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})  
   6.396 +          \<in> set evs -->                                              
   6.397 +          Crypt K (Number Ta) \<in> parts (spies evs) -->         
   6.398 +          Says B A (Crypt K (Number Ta)) \<in> set evs"
   6.399 +apply (erule kerberos_ban.induct)
   6.400 +apply (frule_tac [7] Oops_parts_spies)
   6.401 +apply (frule_tac [5] Says_S_message_form)
   6.402 +apply (drule_tac [6] Kb3_msg_in_parts_spies, analz_mono_contra)
   6.403 +apply (simp_all (no_asm_simp) add: all_conj_distrib)
   6.404 +txt{*Fake*}
   6.405 +apply blast
   6.406 +txt{*Kb2*}
   6.407 +apply (force dest: Crypt_imp_invKey_keysFor) 
   6.408 +txt{*Kb4*}
   6.409 +apply (blast dest: B_trusts_K_by_Kb3 unique_session_keys 
   6.410 +                   Says_imp_spies [THEN analz.Inj] Crypt_Spy_analz_bad)
   6.411 +done
   6.412 +
   6.413 +
   6.414 +(*AUTHENTICATION OF B TO A*)
   6.415 +lemma Authentication_B:
   6.416 +     "[| Crypt K (Number Ta) \<in> parts (spies evs);            
   6.417 +         Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}     
   6.418 +         \<in> parts (spies evs);                                
   6.419 +         ~ Expired Ts evs;                                   
   6.420 +         A \<notin> bad;  B \<notin> bad;  evs \<in> kerberos_ban |]         
   6.421 +      ==> Says B A (Crypt K (Number Ta)) \<in> set evs"
   6.422 +by (blast dest!: A_trusts_K_by_Kb2
   6.423 +          intro!: lemma_B elim!: Confidentiality_S [THEN [2] rev_notE])
   6.424 +
   6.425 +
   6.426 +
   6.427 +lemma lemma_A [rule_format]:
   6.428 +     "[| A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |] 
   6.429 +      ==>           
   6.430 +         Key K \<notin> analz (spies evs) -->          
   6.431 +         Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})   
   6.432 +         \<in> set evs -->   
   6.433 +          Crypt K {|Agent A, Number Ta|} \<in> parts (spies evs) --> 
   6.434 +         Says A B {|X, Crypt K {|Agent A, Number Ta|}|}   
   6.435 +             \<in> set evs"
   6.436 +apply (erule kerberos_ban.induct)
   6.437 +apply (frule_tac [7] Oops_parts_spies)
   6.438 +apply (frule_tac [5] Says_S_message_form)
   6.439 +apply (frule_tac [6] Kb3_msg_in_parts_spies, analz_mono_contra)
   6.440 +apply (simp_all (no_asm_simp) add: all_conj_distrib)
   6.441 +txt{*Fake*}
   6.442 +apply blast
   6.443 +txt{*Kb2*}
   6.444 +apply (force dest: Crypt_imp_invKey_keysFor) 
   6.445 +txt{*Kb3*}
   6.446 +apply (blast dest: A_trusts_K_by_Kb2 unique_session_keys)
   6.447 +done
   6.448 +
   6.449 +
   6.450 +(*AUTHENTICATION OF A TO B*)
   6.451 +lemma Authentication_A:
   6.452 +     "[| Crypt K {|Agent A, Number Ta|} \<in> parts (spies evs);   
   6.453 +         Crypt (shrK B) {|Number Ts, Agent A, Key K|}          
   6.454 +         \<in> parts (spies evs);                                  
   6.455 +         ~ Expired Ts evs;                                     
   6.456 +         A \<notin> bad;  B \<notin> bad;  evs \<in> kerberos_ban |]           
   6.457 +      ==> Says A B {|Crypt (shrK B) {|Number Ts, Agent A, Key K|},      
   6.458 +                     Crypt K {|Agent A, Number Ta|}|} \<in> set evs"
   6.459 +by (blast dest!: B_trusts_K_by_Kb3
   6.460 +          intro!: lemma_A 
   6.461 +          elim!: Confidentiality_S [THEN [2] rev_notE])
   6.462  
   6.463  end
     7.1 --- a/src/HOL/Auth/Message.thy	Sat Apr 26 12:38:17 2003 +0200
     7.2 +++ b/src/HOL/Auth/Message.thy	Sat Apr 26 12:38:42 2003 +0200
     7.3 @@ -7,11 +7,10 @@
     7.4  Inductive relations "parts", "analz" and "synth"
     7.5  *)
     7.6  
     7.7 -theory Message = Main
     7.8 -files ("Message_lemmas.ML"):
     7.9 +theory Message = Main:
    7.10  
    7.11  (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
    7.12 -lemma [simp] : "A Un (B Un A) = B Un A"
    7.13 +lemma [simp] : "A \<union> (B \<union> A) = B \<union> A"
    7.14  by blast
    7.15  
    7.16  types 
    7.17 @@ -83,6 +82,238 @@
    7.18  done
    7.19  
    7.20  
    7.21 +(*Equations hold because constructors are injective; cannot prove for all f*)
    7.22 +lemma Friend_image_eq [simp]: "(Friend x \<in> Friend`A) = (x:A)"
    7.23 +by auto
    7.24 +
    7.25 +lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x\<in>A)"
    7.26 +by auto
    7.27 +
    7.28 +lemma Nonce_Key_image_eq [simp]: "(Nonce x \<notin> Key`A)"
    7.29 +by auto
    7.30 +
    7.31 +
    7.32 +(** Inverse of keys **)
    7.33 +
    7.34 +lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
    7.35 +apply safe
    7.36 +apply (drule_tac f = invKey in arg_cong, simp)
    7.37 +done
    7.38 +
    7.39 +
    7.40 +subsection{*keysFor operator*}
    7.41 +
    7.42 +lemma keysFor_empty [simp]: "keysFor {} = {}"
    7.43 +by (unfold keysFor_def, blast)
    7.44 +
    7.45 +lemma keysFor_Un [simp]: "keysFor (H \<union> H') = keysFor H \<union> keysFor H'"
    7.46 +by (unfold keysFor_def, blast)
    7.47 +
    7.48 +lemma keysFor_UN [simp]: "keysFor (\<Union>i\<in>A. H i) = (\<Union>i\<in>A. keysFor (H i))"
    7.49 +by (unfold keysFor_def, blast)
    7.50 +
    7.51 +(*Monotonicity*)
    7.52 +lemma keysFor_mono: "G\<subseteq>H ==> keysFor(G) \<subseteq> keysFor(H)"
    7.53 +by (unfold keysFor_def, blast)
    7.54 +
    7.55 +lemma keysFor_insert_Agent [simp]: "keysFor (insert (Agent A) H) = keysFor H"
    7.56 +by (unfold keysFor_def, auto)
    7.57 +
    7.58 +lemma keysFor_insert_Nonce [simp]: "keysFor (insert (Nonce N) H) = keysFor H"
    7.59 +by (unfold keysFor_def, auto)
    7.60 +
    7.61 +lemma keysFor_insert_Number [simp]: "keysFor (insert (Number N) H) = keysFor H"
    7.62 +by (unfold keysFor_def, auto)
    7.63 +
    7.64 +lemma keysFor_insert_Key [simp]: "keysFor (insert (Key K) H) = keysFor H"
    7.65 +by (unfold keysFor_def, auto)
    7.66 +
    7.67 +lemma keysFor_insert_Hash [simp]: "keysFor (insert (Hash X) H) = keysFor H"
    7.68 +by (unfold keysFor_def, auto)
    7.69 +
    7.70 +lemma keysFor_insert_MPair [simp]: "keysFor (insert {|X,Y|} H) = keysFor H"
    7.71 +by (unfold keysFor_def, auto)
    7.72 +
    7.73 +lemma keysFor_insert_Crypt [simp]: 
    7.74 +    "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"
    7.75 +apply (unfold keysFor_def, auto)
    7.76 +done
    7.77 +
    7.78 +lemma keysFor_image_Key [simp]: "keysFor (Key`E) = {}"
    7.79 +by (unfold keysFor_def, auto)
    7.80 +
    7.81 +lemma Crypt_imp_invKey_keysFor: "Crypt K X \<in> H ==> invKey K \<in> keysFor H"
    7.82 +by (unfold keysFor_def, blast)
    7.83 +
    7.84 +
    7.85 +subsection{*Inductive relation "parts"*}
    7.86 +
    7.87 +lemma MPair_parts:
    7.88 +     "[| {|X,Y|} \<in> parts H;        
    7.89 +         [| X \<in> parts H; Y \<in> parts H |] ==> P |] ==> P"
    7.90 +by (blast dest: parts.Fst parts.Snd) 
    7.91 +
    7.92 +declare MPair_parts [elim!]  parts.Body [dest!]
    7.93 +text{*NB These two rules are UNSAFE in the formal sense, as they discard the
    7.94 +     compound message.  They work well on THIS FILE.  
    7.95 +  @{text MPair_parts} is left as SAFE because it speeds up proofs.
    7.96 +  The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*}
    7.97 +
    7.98 +lemma parts_increasing: "H \<subseteq> parts(H)"
    7.99 +by blast
   7.100 +
   7.101 +lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD, standard]
   7.102 +
   7.103 +lemma parts_empty [simp]: "parts{} = {}"
   7.104 +apply safe
   7.105 +apply (erule parts.induct, blast+)
   7.106 +done
   7.107 +
   7.108 +lemma parts_emptyE [elim!]: "X\<in> parts{} ==> P"
   7.109 +by simp
   7.110 +
   7.111 +(*WARNING: loops if H = {Y}, therefore must not be repeated!*)
   7.112 +lemma parts_singleton: "X\<in> parts H ==> \<exists>Y\<in>H. X\<in> parts {Y}"
   7.113 +by (erule parts.induct, blast+)
   7.114 +
   7.115 +
   7.116 +(** Unions **)
   7.117 +
   7.118 +lemma parts_Un_subset1: "parts(G) \<union> parts(H) \<subseteq> parts(G \<union> H)"
   7.119 +by (intro Un_least parts_mono Un_upper1 Un_upper2)
   7.120 +
   7.121 +lemma parts_Un_subset2: "parts(G \<union> H) \<subseteq> parts(G) \<union> parts(H)"
   7.122 +apply (rule subsetI)
   7.123 +apply (erule parts.induct, blast+)
   7.124 +done
   7.125 +
   7.126 +lemma parts_Un [simp]: "parts(G \<union> H) = parts(G) \<union> parts(H)"
   7.127 +by (intro equalityI parts_Un_subset1 parts_Un_subset2)
   7.128 +
   7.129 +lemma parts_insert: "parts (insert X H) = parts {X} \<union> parts H"
   7.130 +apply (subst insert_is_Un [of _ H])
   7.131 +apply (simp only: parts_Un)
   7.132 +done
   7.133 +
   7.134 +(*TWO inserts to avoid looping.  This rewrite is better than nothing.
   7.135 +  Not suitable for Addsimps: its behaviour can be strange.*)
   7.136 +lemma parts_insert2: "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
   7.137 +apply (simp add: Un_assoc)
   7.138 +apply (simp add: parts_insert [symmetric])
   7.139 +done
   7.140 +
   7.141 +lemma parts_UN_subset1: "(\<Union>x\<in>A. parts(H x)) \<subseteq> parts(\<Union>x\<in>A. H x)"
   7.142 +by (intro UN_least parts_mono UN_upper)
   7.143 +
   7.144 +lemma parts_UN_subset2: "parts(\<Union>x\<in>A. H x) \<subseteq> (\<Union>x\<in>A. parts(H x))"
   7.145 +apply (rule subsetI)
   7.146 +apply (erule parts.induct, blast+)
   7.147 +done
   7.148 +
   7.149 +lemma parts_UN [simp]: "parts(\<Union>x\<in>A. H x) = (\<Union>x\<in>A. parts(H x))"
   7.150 +by (intro equalityI parts_UN_subset1 parts_UN_subset2)
   7.151 +
   7.152 +(*Added to simplify arguments to parts, analz and synth.
   7.153 +  NOTE: the UN versions are no longer used!*)
   7.154 +
   7.155 +
   7.156 +text{*This allows @{text blast} to simplify occurrences of 
   7.157 +  @{term "parts(G\<union>H)"} in the assumption.*}
   7.158 +declare parts_Un [THEN equalityD1, THEN subsetD, THEN UnE, elim!] 
   7.159 +
   7.160 +
   7.161 +lemma parts_insert_subset: "insert X (parts H) \<subseteq> parts(insert X H)"
   7.162 +by (blast intro: parts_mono [THEN [2] rev_subsetD])
   7.163 +
   7.164 +(** Idempotence and transitivity **)
   7.165 +
   7.166 +lemma parts_partsD [dest!]: "X\<in> parts (parts H) ==> X\<in> parts H"
   7.167 +by (erule parts.induct, blast+)
   7.168 +
   7.169 +lemma parts_idem [simp]: "parts (parts H) = parts H"
   7.170 +by blast
   7.171 +
   7.172 +lemma parts_trans: "[| X\<in> parts G;  G \<subseteq> parts H |] ==> X\<in> parts H"
   7.173 +by (drule parts_mono, blast)
   7.174 +
   7.175 +(*Cut*)
   7.176 +lemma parts_cut: "[| Y\<in> parts (insert X G);  X\<in> parts H |]  
   7.177 +               ==> Y\<in> parts (G \<union> H)"
   7.178 +apply (erule parts_trans, auto)
   7.179 +done
   7.180 +
   7.181 +lemma parts_cut_eq [simp]: "X\<in> parts H ==> parts (insert X H) = parts H"
   7.182 +by (force dest!: parts_cut intro: parts_insertI)
   7.183 +
   7.184 +
   7.185 +(** Rewrite rules for pulling out atomic messages **)
   7.186 +
   7.187 +lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset]
   7.188 +
   7.189 +
   7.190 +lemma parts_insert_Agent [simp]: "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"
   7.191 +apply (rule parts_insert_eq_I) 
   7.192 +apply (erule parts.induct, auto) 
   7.193 +done
   7.194 +
   7.195 +lemma parts_insert_Nonce [simp]: "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"
   7.196 +apply (rule parts_insert_eq_I) 
   7.197 +apply (erule parts.induct, auto) 
   7.198 +done
   7.199 +
   7.200 +lemma parts_insert_Number [simp]: "parts (insert (Number N) H) = insert (Number N) (parts H)"
   7.201 +apply (rule parts_insert_eq_I) 
   7.202 +apply (erule parts.induct, auto) 
   7.203 +done
   7.204 +
   7.205 +lemma parts_insert_Key [simp]: "parts (insert (Key K) H) = insert (Key K) (parts H)"
   7.206 +apply (rule parts_insert_eq_I) 
   7.207 +apply (erule parts.induct, auto) 
   7.208 +done
   7.209 +
   7.210 +lemma parts_insert_Hash [simp]: "parts (insert (Hash X) H) = insert (Hash X) (parts H)"
   7.211 +apply (rule parts_insert_eq_I) 
   7.212 +apply (erule parts.induct, auto) 
   7.213 +done
   7.214 +
   7.215 +lemma parts_insert_Crypt [simp]: "parts (insert (Crypt K X) H) =  
   7.216 +          insert (Crypt K X) (parts (insert X H))"
   7.217 +apply (rule equalityI)
   7.218 +apply (rule subsetI)
   7.219 +apply (erule parts.induct, auto)
   7.220 +apply (erule parts.induct)
   7.221 +apply (blast intro: parts.Body)+
   7.222 +done
   7.223 +
   7.224 +lemma parts_insert_MPair [simp]: "parts (insert {|X,Y|} H) =  
   7.225 +          insert {|X,Y|} (parts (insert X (insert Y H)))"
   7.226 +apply (rule equalityI)
   7.227 +apply (rule subsetI)
   7.228 +apply (erule parts.induct, auto)
   7.229 +apply (erule parts.induct)
   7.230 +apply (blast intro: parts.Fst parts.Snd)+
   7.231 +done
   7.232 +
   7.233 +lemma parts_image_Key [simp]: "parts (Key`N) = Key`N"
   7.234 +apply auto
   7.235 +apply (erule parts.induct, auto)
   7.236 +done
   7.237 +
   7.238 +
   7.239 +(*In any message, there is an upper bound N on its greatest nonce.*)
   7.240 +lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n --> Nonce n \<notin> parts {msg}"
   7.241 +apply (induct_tac "msg")
   7.242 +apply (simp_all (no_asm_simp) add: exI parts_insert2)
   7.243 +(*MPair case: blast_tac works out the necessary sum itself!*)
   7.244 +prefer 2 apply (blast elim!: add_leE)
   7.245 +(*Nonce case*)
   7.246 +apply (rule_tac x = "N + Suc nat" in exI)
   7.247 +apply (auto elim!: add_leE)
   7.248 +done
   7.249 +
   7.250 +
   7.251 +subsection{*Inductive relation "analz"*}
   7.252 +
   7.253  (** Inductive definition of "analz" -- what can be broken down from a set of
   7.254      messages, including keys.  A form of downward closure.  Pairs can
   7.255      be taken apart; messages decrypted with known keys.  **)
   7.256 @@ -104,6 +335,211 @@
   7.257  apply (auto dest: Fst Snd) 
   7.258  done
   7.259  
   7.260 +text{*Making it safe speeds up proofs*}
   7.261 +lemma MPair_analz [elim!]:
   7.262 +     "[| {|X,Y|} \<in> analz H;        
   7.263 +             [| X \<in> analz H; Y \<in> analz H |] ==> P   
   7.264 +          |] ==> P"
   7.265 +by (blast dest: analz.Fst analz.Snd)
   7.266 +
   7.267 +lemma analz_increasing: "H \<subseteq> analz(H)"
   7.268 +by blast
   7.269 +
   7.270 +lemma analz_subset_parts: "analz H \<subseteq> parts H"
   7.271 +apply (rule subsetI)
   7.272 +apply (erule analz.induct, blast+)
   7.273 +done
   7.274 +
   7.275 +lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
   7.276 +
   7.277 +
   7.278 +lemma parts_analz [simp]: "parts (analz H) = parts H"
   7.279 +apply (rule equalityI)
   7.280 +apply (rule analz_subset_parts [THEN parts_mono, THEN subset_trans], simp)
   7.281 +apply (blast intro: analz_increasing [THEN parts_mono, THEN subsetD])
   7.282 +done
   7.283 +
   7.284 +lemma analz_parts [simp]: "analz (parts H) = parts H"
   7.285 +apply auto
   7.286 +apply (erule analz.induct, auto)
   7.287 +done
   7.288 +
   7.289 +lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard]
   7.290 +
   7.291 +(** General equational properties **)
   7.292 +
   7.293 +lemma analz_empty [simp]: "analz{} = {}"
   7.294 +apply safe
   7.295 +apply (erule analz.induct, blast+)
   7.296 +done
   7.297 +
   7.298 +(*Converse fails: we can analz more from the union than from the 
   7.299 +  separate parts, as a key in one might decrypt a message in the other*)
   7.300 +lemma analz_Un: "analz(G) \<union> analz(H) \<subseteq> analz(G \<union> H)"
   7.301 +by (intro Un_least analz_mono Un_upper1 Un_upper2)
   7.302 +
   7.303 +lemma analz_insert: "insert X (analz H) \<subseteq> analz(insert X H)"
   7.304 +by (blast intro: analz_mono [THEN [2] rev_subsetD])
   7.305 +
   7.306 +(** Rewrite rules for pulling out atomic messages **)
   7.307 +
   7.308 +lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert]
   7.309 +
   7.310 +lemma analz_insert_Agent [simp]: "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"
   7.311 +apply (rule analz_insert_eq_I) 
   7.312 +apply (erule analz.induct, auto) 
   7.313 +done
   7.314 +
   7.315 +lemma analz_insert_Nonce [simp]: "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"
   7.316 +apply (rule analz_insert_eq_I) 
   7.317 +apply (erule analz.induct, auto) 
   7.318 +done
   7.319 +
   7.320 +lemma analz_insert_Number [simp]: "analz (insert (Number N) H) = insert (Number N) (analz H)"
   7.321 +apply (rule analz_insert_eq_I) 
   7.322 +apply (erule analz.induct, auto) 
   7.323 +done
   7.324 +
   7.325 +lemma analz_insert_Hash [simp]: "analz (insert (Hash X) H) = insert (Hash X) (analz H)"
   7.326 +apply (rule analz_insert_eq_I) 
   7.327 +apply (erule analz.induct, auto) 
   7.328 +done
   7.329 +
   7.330 +(*Can only pull out Keys if they are not needed to decrypt the rest*)
   7.331 +lemma analz_insert_Key [simp]: 
   7.332 +    "K \<notin> keysFor (analz H) ==>   
   7.333 +          analz (insert (Key K) H) = insert (Key K) (analz H)"
   7.334 +apply (unfold keysFor_def)
   7.335 +apply (rule analz_insert_eq_I) 
   7.336 +apply (erule analz.induct, auto) 
   7.337 +done
   7.338 +
   7.339 +lemma analz_insert_MPair [simp]: "analz (insert {|X,Y|} H) =  
   7.340 +          insert {|X,Y|} (analz (insert X (insert Y H)))"
   7.341 +apply (rule equalityI)
   7.342 +apply (rule subsetI)
   7.343 +apply (erule analz.induct, auto)
   7.344 +apply (erule analz.induct)
   7.345 +apply (blast intro: analz.Fst analz.Snd)+
   7.346 +done
   7.347 +
   7.348 +(*Can pull out enCrypted message if the Key is not known*)
   7.349 +lemma analz_insert_Crypt:
   7.350 +     "Key (invKey K) \<notin> analz H 
   7.351 +      ==> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)"
   7.352 +apply (rule analz_insert_eq_I) 
   7.353 +apply (erule analz.induct, auto) 
   7.354 +
   7.355 +done
   7.356 +
   7.357 +lemma lemma1: "Key (invKey K) \<in> analz H ==>   
   7.358 +               analz (insert (Crypt K X) H) \<subseteq>  
   7.359 +               insert (Crypt K X) (analz (insert X H))"
   7.360 +apply (rule subsetI)
   7.361 +apply (erule_tac xa = x in analz.induct, auto)
   7.362 +done
   7.363 +
   7.364 +lemma lemma2: "Key (invKey K) \<in> analz H ==>   
   7.365 +               insert (Crypt K X) (analz (insert X H)) \<subseteq>  
   7.366 +               analz (insert (Crypt K X) H)"
   7.367 +apply auto
   7.368 +apply (erule_tac xa = x in analz.induct, auto)
   7.369 +apply (blast intro: analz_insertI analz.Decrypt)
   7.370 +done
   7.371 +
   7.372 +lemma analz_insert_Decrypt: "Key (invKey K) \<in> analz H ==>   
   7.373 +               analz (insert (Crypt K X) H) =  
   7.374 +               insert (Crypt K X) (analz (insert X H))"
   7.375 +by (intro equalityI lemma1 lemma2)
   7.376 +
   7.377 +(*Case analysis: either the message is secure, or it is not!
   7.378 +  Effective, but can cause subgoals to blow up!
   7.379 +  Use with split_if;  apparently split_tac does not cope with patterns
   7.380 +  such as "analz (insert (Crypt K X) H)" *)
   7.381 +lemma analz_Crypt_if [simp]:
   7.382 +     "analz (insert (Crypt K X) H) =                 
   7.383 +          (if (Key (invKey K) \<in> analz H)                 
   7.384 +           then insert (Crypt K X) (analz (insert X H))  
   7.385 +           else insert (Crypt K X) (analz H))"
   7.386 +by (simp add: analz_insert_Crypt analz_insert_Decrypt)
   7.387 +
   7.388 +
   7.389 +(*This rule supposes "for the sake of argument" that we have the key.*)
   7.390 +lemma analz_insert_Crypt_subset: "analz (insert (Crypt K X) H) \<subseteq>   
   7.391 +           insert (Crypt K X) (analz (insert X H))"
   7.392 +apply (rule subsetI)
   7.393 +apply (erule analz.induct, auto)
   7.394 +done
   7.395 +
   7.396 +
   7.397 +lemma analz_image_Key [simp]: "analz (Key`N) = Key`N"
   7.398 +apply auto
   7.399 +apply (erule analz.induct, auto)
   7.400 +done
   7.401 +
   7.402 +
   7.403 +(** Idempotence and transitivity **)
   7.404 +
   7.405 +lemma analz_analzD [dest!]: "X\<in> analz (analz H) ==> X\<in> analz H"
   7.406 +by (erule analz.induct, blast+)
   7.407 +
   7.408 +lemma analz_idem [simp]: "analz (analz H) = analz H"
   7.409 +by blast
   7.410 +
   7.411 +lemma analz_trans: "[| X\<in> analz G;  G \<subseteq> analz H |] ==> X\<in> analz H"
   7.412 +by (drule analz_mono, blast)
   7.413 +
   7.414 +(*Cut; Lemma 2 of Lowe*)
   7.415 +lemma analz_cut: "[| Y\<in> analz (insert X H);  X\<in> analz H |] ==> Y\<in> analz H"
   7.416 +by (erule analz_trans, blast)
   7.417 +
   7.418 +(*Cut can be proved easily by induction on
   7.419 +   "Y: analz (insert X H) ==> X: analz H --> Y: analz H"
   7.420 +*)
   7.421 +
   7.422 +(*This rewrite rule helps in the simplification of messages that involve
   7.423 +  the forwarding of unknown components (X).  Without it, removing occurrences
   7.424 +  of X can be very complicated. *)
   7.425 +lemma analz_insert_eq: "X\<in> analz H ==> analz (insert X H) = analz H"
   7.426 +by (blast intro: analz_cut analz_insertI)
   7.427 +
   7.428 +
   7.429 +(** A congruence rule for "analz" **)
   7.430 +
   7.431 +lemma analz_subset_cong: "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H'  
   7.432 +               |] ==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
   7.433 +apply clarify
   7.434 +apply (erule analz.induct)
   7.435 +apply (best intro: analz_mono [THEN subsetD])+
   7.436 +done
   7.437 +
   7.438 +lemma analz_cong: "[| analz G = analz G'; analz H = analz H'  
   7.439 +               |] ==> analz (G \<union> H) = analz (G' \<union> H')"
   7.440 +apply (intro equalityI analz_subset_cong, simp_all) 
   7.441 +done
   7.442 +
   7.443 +
   7.444 +lemma analz_insert_cong: "analz H = analz H' ==> analz(insert X H) = analz(insert X H')"
   7.445 +by (force simp only: insert_def intro!: analz_cong)
   7.446 +
   7.447 +(*If there are no pairs or encryptions then analz does nothing*)
   7.448 +lemma analz_trivial: "[| \<forall>X Y. {|X,Y|} \<notin> H;  \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
   7.449 +apply safe
   7.450 +apply (erule analz.induct, blast+)
   7.451 +done
   7.452 +
   7.453 +(*These two are obsolete (with a single Spy) but cost little to prove...*)
   7.454 +lemma analz_UN_analz_lemma: "X\<in> analz (\<Union>i\<in>A. analz (H i)) ==> X\<in> analz (\<Union>i\<in>A. H i)"
   7.455 +apply (erule analz.induct)
   7.456 +apply (blast intro: analz_mono [THEN [2] rev_subsetD])+
   7.457 +done
   7.458 +
   7.459 +lemma analz_UN_analz [simp]: "analz (\<Union>i\<in>A. analz (H i)) = analz (\<Union>i\<in>A. H i)"
   7.460 +by (blast intro: analz_UN_analz_lemma analz_mono [THEN [2] rev_subsetD])
   7.461 +
   7.462 +
   7.463 +subsection{*Inductive relation "synth"*}
   7.464 +
   7.465  (** Inductive definition of "synth" -- what can be built up from a set of
   7.466      messages.  A form of upward closure.  Pairs can be built, messages
   7.467      encrypted with known keys.  Agent names are public domain.
   7.468 @@ -133,7 +569,376 @@
   7.469  inductive_cases MPair_synth [elim!]: "{|X,Y|} \<in> synth H"
   7.470  inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"
   7.471  
   7.472 -use "Message_lemmas.ML"
   7.473 +
   7.474 +lemma synth_increasing: "H \<subseteq> synth(H)"
   7.475 +by blast
   7.476 +
   7.477 +(** Unions **)
   7.478 +
   7.479 +(*Converse fails: we can synth more from the union than from the 
   7.480 +  separate parts, building a compound message using elements of each.*)
   7.481 +lemma synth_Un: "synth(G) \<union> synth(H) \<subseteq> synth(G \<union> H)"
   7.482 +by (intro Un_least synth_mono Un_upper1 Un_upper2)
   7.483 +
   7.484 +lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)"
   7.485 +by (blast intro: synth_mono [THEN [2] rev_subsetD])
   7.486 +
   7.487 +(** Idempotence and transitivity **)
   7.488 +
   7.489 +lemma synth_synthD [dest!]: "X\<in> synth (synth H) ==> X\<in> synth H"
   7.490 +by (erule synth.induct, blast+)
   7.491 +
   7.492 +lemma synth_idem: "synth (synth H) = synth H"
   7.493 +by blast
   7.494 +
   7.495 +lemma synth_trans: "[| X\<in> synth G;  G \<subseteq> synth H |] ==> X\<in> synth H"
   7.496 +by (drule synth_mono, blast)
   7.497 +
   7.498 +(*Cut; Lemma 2 of Lowe*)
   7.499 +lemma synth_cut: "[| Y\<in> synth (insert X H);  X\<in> synth H |] ==> Y\<in> synth H"
   7.500 +by (erule synth_trans, blast)
   7.501 +
   7.502 +lemma Agent_synth [simp]: "Agent A \<in> synth H"
   7.503 +by blast
   7.504 +
   7.505 +lemma Number_synth [simp]: "Number n \<in> synth H"
   7.506 +by blast
   7.507 +
   7.508 +lemma Nonce_synth_eq [simp]: "(Nonce N \<in> synth H) = (Nonce N \<in> H)"
   7.509 +by blast
   7.510 +
   7.511 +lemma Key_synth_eq [simp]: "(Key K \<in> synth H) = (Key K \<in> H)"
   7.512 +by blast
   7.513 +
   7.514 +lemma Crypt_synth_eq [simp]: "Key K \<notin> H ==> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)"
   7.515 +by blast
   7.516 +
   7.517 +
   7.518 +lemma keysFor_synth [simp]: 
   7.519 +    "keysFor (synth H) = keysFor H \<union> invKey`{K. Key K \<in> H}"
   7.520 +apply (unfold keysFor_def, blast)
   7.521 +done
   7.522 +
   7.523 +
   7.524 +(*** Combinations of parts, analz and synth ***)
   7.525 +
   7.526 +lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H"
   7.527 +apply (rule equalityI)
   7.528 +apply (rule subsetI)
   7.529 +apply (erule parts.induct)
   7.530 +apply (blast intro: synth_increasing [THEN parts_mono, THEN subsetD] 
   7.531 +                    parts.Fst parts.Snd parts.Body)+
   7.532 +done
   7.533 +
   7.534 +lemma analz_analz_Un [simp]: "analz (analz G \<union> H) = analz (G \<union> H)"
   7.535 +apply (intro equalityI analz_subset_cong)+
   7.536 +apply simp_all
   7.537 +done
   7.538 +
   7.539 +lemma analz_synth_Un [simp]: "analz (synth G \<union> H) = analz (G \<union> H) \<union> synth G"
   7.540 +apply (rule equalityI)
   7.541 +apply (rule subsetI)
   7.542 +apply (erule analz.induct)
   7.543 +prefer 5 apply (blast intro: analz_mono [THEN [2] rev_subsetD])
   7.544 +apply (blast intro: analz.Fst analz.Snd analz.Decrypt)+
   7.545 +done
   7.546 +
   7.547 +lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"
   7.548 +apply (cut_tac H = "{}" in analz_synth_Un)
   7.549 +apply (simp (no_asm_use))
   7.550 +done
   7.551 +
   7.552 +
   7.553 +(** For reasoning about the Fake rule in traces **)
   7.554 +
   7.555 +lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
   7.556 +by (rule subset_trans [OF parts_mono parts_Un_subset2], blast)
   7.557 +
   7.558 +(*More specifically for Fake.  Very occasionally we could do with a version
   7.559 +  of the form  parts{X} \<subseteq> synth (analz H) \<union> parts H *)
   7.560 +lemma Fake_parts_insert: "X \<in> synth (analz H) ==>  
   7.561 +      parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
   7.562 +apply (drule parts_insert_subset_Un)
   7.563 +apply (simp (no_asm_use))
   7.564 +apply blast
   7.565 +done
   7.566 +
   7.567 +(*H is sometimes (Key ` KK \<union> spies evs), so can't put G=H*)
   7.568 +lemma Fake_analz_insert: "X\<in> synth (analz G) ==>  
   7.569 +      analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
   7.570 +apply (rule subsetI)
   7.571 +apply (subgoal_tac "x \<in> analz (synth (analz G) \<union> H) ")
   7.572 +prefer 2 apply (blast intro: analz_mono [THEN [2] rev_subsetD] analz_mono [THEN synth_mono, THEN [2] rev_subsetD])
   7.573 +apply (simp (no_asm_use))
   7.574 +apply blast
   7.575 +done
   7.576 +
   7.577 +lemma analz_conj_parts [simp]: "(X \<in> analz H & X \<in> parts H) = (X \<in> analz H)"
   7.578 +by (blast intro: analz_subset_parts [THEN [2] rev_subsetD])
   7.579 +
   7.580 +lemma analz_disj_parts [simp]: "(X \<in> analz H | X \<in> parts H) = (X \<in> parts H)"
   7.581 +by (blast intro: analz_subset_parts [THEN [2] rev_subsetD])
   7.582 +
   7.583 +(*Without this equation, other rules for synth and analz would yield
   7.584 +  redundant cases*)
   7.585 +lemma MPair_synth_analz [iff]:
   7.586 +     "({|X,Y|} \<in> synth (analz H)) =  
   7.587 +      (X \<in> synth (analz H) & Y \<in> synth (analz H))"
   7.588 +by blast
   7.589 +
   7.590 +lemma Crypt_synth_analz: "[| Key K \<in> analz H;  Key (invKey K) \<in> analz H |]  
   7.591 +       ==> (Crypt K X \<in> synth (analz H)) = (X \<in> synth (analz H))"
   7.592 +by blast
   7.593 +
   7.594 +
   7.595 +lemma Hash_synth_analz [simp]: "X \<notin> synth (analz H)  
   7.596 +      ==> (Hash{|X,Y|} \<in> synth (analz H)) = (Hash{|X,Y|} \<in> analz H)"
   7.597 +by blast
   7.598 +
   7.599 +
   7.600 +subsection{*HPair: a combination of Hash and MPair*}
   7.601 +
   7.602 +(*** Freeness ***)
   7.603 +
   7.604 +lemma Agent_neq_HPair: "Agent A ~= Hash[X] Y"
   7.605 +by (unfold HPair_def, simp)
   7.606 +
   7.607 +lemma Nonce_neq_HPair: "Nonce N ~= Hash[X] Y"
   7.608 +by (unfold HPair_def, simp)
   7.609 +
   7.610 +lemma Number_neq_HPair: "Number N ~= Hash[X] Y"
   7.611 +by (unfold HPair_def, simp)
   7.612 +
   7.613 +lemma Key_neq_HPair: "Key K ~= Hash[X] Y"
   7.614 +by (unfold HPair_def, simp)
   7.615 +
   7.616 +lemma Hash_neq_HPair: "Hash Z ~= Hash[X] Y"
   7.617 +by (unfold HPair_def, simp)
   7.618 +
   7.619 +lemma Crypt_neq_HPair: "Crypt K X' ~= Hash[X] Y"
   7.620 +by (unfold HPair_def, simp)
   7.621 +
   7.622 +lemmas HPair_neqs = Agent_neq_HPair Nonce_neq_HPair Number_neq_HPair 
   7.623 +                    Key_neq_HPair Hash_neq_HPair Crypt_neq_HPair
   7.624 +
   7.625 +declare HPair_neqs [iff]
   7.626 +declare HPair_neqs [symmetric, iff]
   7.627 +
   7.628 +lemma HPair_eq [iff]: "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)"
   7.629 +by (simp add: HPair_def)
   7.630 +
   7.631 +lemma MPair_eq_HPair [iff]: "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)"
   7.632 +by (simp add: HPair_def)
   7.633 +
   7.634 +lemma HPair_eq_MPair [iff]: "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)"
   7.635 +by (auto simp add: HPair_def)
   7.636 +
   7.637 +
   7.638 +(*** Specialized laws, proved in terms of those for Hash and MPair ***)
   7.639 +
   7.640 +lemma keysFor_insert_HPair [simp]: "keysFor (insert (Hash[X] Y) H) = keysFor H"
   7.641 +by (simp add: HPair_def)
   7.642 +
   7.643 +lemma parts_insert_HPair [simp]: 
   7.644 +    "parts (insert (Hash[X] Y) H) =  
   7.645 +     insert (Hash[X] Y) (insert (Hash{|X,Y|}) (parts (insert Y H)))"
   7.646 +by (simp add: HPair_def)
   7.647 +
   7.648 +lemma analz_insert_HPair [simp]: 
   7.649 +    "analz (insert (Hash[X] Y) H) =  
   7.650 +     insert (Hash[X] Y) (insert (Hash{|X,Y|}) (analz (insert Y H)))"
   7.651 +by (simp add: HPair_def)
   7.652 +
   7.653 +lemma HPair_synth_analz [simp]:
   7.654 +     "X \<notin> synth (analz H)  
   7.655 +    ==> (Hash[X] Y \<in> synth (analz H)) =  
   7.656 +        (Hash {|X, Y|} \<in> analz H & Y \<in> synth (analz H))"
   7.657 +by (simp add: HPair_def)
   7.658 +
   7.659 +
   7.660 +(*We do NOT want Crypt... messages broken up in protocols!!*)
   7.661 +declare parts.Body [rule del]
   7.662 +
   7.663 +
   7.664 +ML
   7.665 +{*
   7.666 +(*ML bindings for definitions and axioms*)
   7.667 +
   7.668 +val invKey = thm "invKey"
   7.669 +val keysFor_def = thm "keysFor_def"
   7.670 +val HPair_def = thm "HPair_def"
   7.671 +val symKeys_def = thm "symKeys_def"
   7.672 +
   7.673 +structure parts =
   7.674 +  struct
   7.675 +  val induct = thm "parts.induct"
   7.676 +  val Inj    = thm "parts.Inj"
   7.677 +  val Fst    = thm "parts.Fst"
   7.678 +  val Snd    = thm "parts.Snd"
   7.679 +  val Body   = thm "parts.Body"
   7.680 +  end
   7.681 +
   7.682 +structure analz =
   7.683 +  struct
   7.684 +  val induct = thm "analz.induct"
   7.685 +  val Inj    = thm "analz.Inj"
   7.686 +  val Fst    = thm "analz.Fst"
   7.687 +  val Snd    = thm "analz.Snd"
   7.688 +  val Decrypt = thm "analz.Decrypt"
   7.689 +  end
   7.690 +
   7.691 +
   7.692 +(** Rewrites to push in Key and Crypt messages, so that other messages can
   7.693 +    be pulled out using the analz_insert rules **)
   7.694 +
   7.695 +fun insComm x y = inst "x" x (inst "y" y insert_commute);
   7.696 +
   7.697 +bind_thms ("pushKeys",
   7.698 +           map (insComm "Key ?K") 
   7.699 +                   ["Agent ?C", "Nonce ?N", "Number ?N", 
   7.700 +		    "Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"]);
   7.701 +
   7.702 +bind_thms ("pushCrypts",
   7.703 +           map (insComm "Crypt ?X ?K") 
   7.704 +                     ["Agent ?C", "Nonce ?N", "Number ?N", 
   7.705 +		      "Hash ?X'", "MPair ?X' ?Y"]);
   7.706 +*}
   7.707 +
   7.708 +text{*Cannot be added with @{text "[simp]"} -- messages should not always be
   7.709 +  re-ordered. *}
   7.710 +lemmas pushes = pushKeys pushCrypts
   7.711 +
   7.712 +
   7.713 +subsection{*Tactics useful for many protocol proofs*}
   7.714 +ML
   7.715 +{*
   7.716 +val parts_mono = thm "parts_mono";
   7.717 +val analz_mono = thm "analz_mono";
   7.718 +val Key_image_eq = thm "Key_image_eq";
   7.719 +val Nonce_Key_image_eq = thm "Nonce_Key_image_eq";
   7.720 +val keysFor_Un = thm "keysFor_Un";
   7.721 +val keysFor_mono = thm "keysFor_mono";
   7.722 +val keysFor_image_Key = thm "keysFor_image_Key";
   7.723 +val Crypt_imp_invKey_keysFor = thm "Crypt_imp_invKey_keysFor";
   7.724 +val MPair_parts = thm "MPair_parts";
   7.725 +val parts_increasing = thm "parts_increasing";
   7.726 +val parts_insertI = thm "parts_insertI";
   7.727 +val parts_empty = thm "parts_empty";
   7.728 +val parts_emptyE = thm "parts_emptyE";
   7.729 +val parts_singleton = thm "parts_singleton";
   7.730 +val parts_Un_subset1 = thm "parts_Un_subset1";
   7.731 +val parts_Un_subset2 = thm "parts_Un_subset2";
   7.732 +val parts_insert = thm "parts_insert";
   7.733 +val parts_insert2 = thm "parts_insert2";
   7.734 +val parts_UN_subset1 = thm "parts_UN_subset1";
   7.735 +val parts_UN_subset2 = thm "parts_UN_subset2";
   7.736 +val parts_UN = thm "parts_UN";
   7.737 +val parts_insert_subset = thm "parts_insert_subset";
   7.738 +val parts_partsD = thm "parts_partsD";
   7.739 +val parts_trans = thm "parts_trans";
   7.740 +val parts_cut = thm "parts_cut";
   7.741 +val parts_cut_eq = thm "parts_cut_eq";
   7.742 +val parts_insert_eq_I = thm "parts_insert_eq_I";
   7.743 +val parts_image_Key = thm "parts_image_Key";
   7.744 +val MPair_analz = thm "MPair_analz";
   7.745 +val analz_increasing = thm "analz_increasing";
   7.746 +val analz_subset_parts = thm "analz_subset_parts";
   7.747 +val not_parts_not_analz = thm "not_parts_not_analz";
   7.748 +val parts_analz = thm "parts_analz";
   7.749 +val analz_parts = thm "analz_parts";
   7.750 +val analz_insertI = thm "analz_insertI";
   7.751 +val analz_empty = thm "analz_empty";
   7.752 +val analz_Un = thm "analz_Un";
   7.753 +val analz_insert_Crypt_subset = thm "analz_insert_Crypt_subset";
   7.754 +val analz_image_Key = thm "analz_image_Key";
   7.755 +val analz_analzD = thm "analz_analzD";
   7.756 +val analz_trans = thm "analz_trans";
   7.757 +val analz_cut = thm "analz_cut";
   7.758 +val analz_insert_eq = thm "analz_insert_eq";
   7.759 +val analz_subset_cong = thm "analz_subset_cong";
   7.760 +val analz_cong = thm "analz_cong";
   7.761 +val analz_insert_cong = thm "analz_insert_cong";
   7.762 +val analz_trivial = thm "analz_trivial";
   7.763 +val analz_UN_analz = thm "analz_UN_analz";
   7.764 +val synth_mono = thm "synth_mono";
   7.765 +val synth_increasing = thm "synth_increasing";
   7.766 +val synth_Un = thm "synth_Un";
   7.767 +val synth_insert = thm "synth_insert";
   7.768 +val synth_synthD = thm "synth_synthD";
   7.769 +val synth_trans = thm "synth_trans";
   7.770 +val synth_cut = thm "synth_cut";
   7.771 +val Agent_synth = thm "Agent_synth";
   7.772 +val Number_synth = thm "Number_synth";
   7.773 +val Nonce_synth_eq = thm "Nonce_synth_eq";
   7.774 +val Key_synth_eq = thm "Key_synth_eq";
   7.775 +val Crypt_synth_eq = thm "Crypt_synth_eq";
   7.776 +val keysFor_synth = thm "keysFor_synth";
   7.777 +val parts_synth = thm "parts_synth";
   7.778 +val analz_analz_Un = thm "analz_analz_Un";
   7.779 +val analz_synth_Un = thm "analz_synth_Un";
   7.780 +val analz_synth = thm "analz_synth";
   7.781 +val parts_insert_subset_Un = thm "parts_insert_subset_Un";
   7.782 +val Fake_parts_insert = thm "Fake_parts_insert";
   7.783 +val Fake_analz_insert = thm "Fake_analz_insert";
   7.784 +val analz_conj_parts = thm "analz_conj_parts";
   7.785 +val analz_disj_parts = thm "analz_disj_parts";
   7.786 +val MPair_synth_analz = thm "MPair_synth_analz";
   7.787 +val Crypt_synth_analz = thm "Crypt_synth_analz";
   7.788 +val Hash_synth_analz = thm "Hash_synth_analz";
   7.789 +val pushes = thms "pushes";
   7.790 +
   7.791 +
   7.792 +(*Prove base case (subgoal i) and simplify others.  A typical base case
   7.793 +  concerns  Crypt K X \<notin> Key`shrK`bad  and cannot be proved by rewriting
   7.794 +  alone.*)
   7.795 +fun prove_simple_subgoals_tac i = 
   7.796 +    force_tac (claset(), simpset() addsimps [image_eq_UN]) i THEN
   7.797 +    ALLGOALS Asm_simp_tac
   7.798 +
   7.799 +(*Analysis of Fake cases.  Also works for messages that forward unknown parts,
   7.800 +  but this application is no longer necessary if analz_insert_eq is used.
   7.801 +  Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
   7.802 +  DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
   7.803 +
   7.804 +(*Apply rules to break down assumptions of the form
   7.805 +  Y \<in> parts(insert X H)  and  Y \<in> analz(insert X H)
   7.806 +*)
   7.807 +val Fake_insert_tac = 
   7.808 +    dresolve_tac [impOfSubs Fake_analz_insert,
   7.809 +                  impOfSubs Fake_parts_insert] THEN'
   7.810 +    eresolve_tac [asm_rl, thm"synth.Inj"];
   7.811 +
   7.812 +fun Fake_insert_simp_tac ss i = 
   7.813 +    REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
   7.814 +
   7.815 +fun atomic_spy_analz_tac (cs,ss) = SELECT_GOAL
   7.816 +    (Fake_insert_simp_tac ss 1
   7.817 +     THEN
   7.818 +     IF_UNSOLVED (Blast.depth_tac
   7.819 +		  (cs addIs [analz_insertI,
   7.820 +				   impOfSubs analz_subset_parts]) 4 1))
   7.821 +
   7.822 +(*The explicit claset and simpset arguments help it work with Isar*)
   7.823 +fun gen_spy_analz_tac (cs,ss) i =
   7.824 +  DETERM
   7.825 +   (SELECT_GOAL
   7.826 +     (EVERY 
   7.827 +      [  (*push in occurrences of X...*)
   7.828 +       (REPEAT o CHANGED)
   7.829 +           (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
   7.830 +       (*...allowing further simplifications*)
   7.831 +       simp_tac ss 1,
   7.832 +       REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
   7.833 +       DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i)
   7.834 +
   7.835 +fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i
   7.836 +*}
   7.837 +
   7.838 +(*By default only o_apply is built-in.  But in the presence of eta-expansion
   7.839 +  this means that some terms displayed as (f o g) will be rewritten, and others
   7.840 +  will not!*)
   7.841 +declare o_def [simp]
   7.842 +
   7.843  
   7.844  lemma Crypt_notin_image_Key [simp]: "Crypt K X \<notin> Key ` A"
   7.845  by auto
   7.846 @@ -174,7 +979,7 @@
   7.847  done
   7.848  
   7.849  lemma Fake_parts_sing:
   7.850 -     "X \<in> synth (analz H) ==> parts{X} \<subseteq> synth (analz H) Un parts H";
   7.851 +     "X \<in> synth (analz H) ==> parts{X} \<subseteq> synth (analz H) \<union> parts H";
   7.852  apply (rule subset_trans) 
   7.853   apply (erule_tac [2] Fake_parts_insert) 
   7.854  apply (simp add: parts_mono) 
   7.855 @@ -200,4 +1005,5 @@
   7.856              Fake_insert_simp_tac (Simplifier.get_local_simpset ctxt) 1)) *}
   7.857      "for debugging spy_analz"
   7.858  
   7.859 +
   7.860  end
     8.1 --- a/src/HOL/Auth/Message_lemmas.ML	Sat Apr 26 12:38:17 2003 +0200
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,902 +0,0 @@
     8.4 -(*  Title:      HOL/Auth/Message
     8.5 -    ID:         $Id$
     8.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.7 -    Copyright   1996  University of Cambridge
     8.8 -
     8.9 -Datatypes of agents and messages;
    8.10 -Inductive relations "parts", "analz" and "synth"
    8.11 -*)
    8.12 -
    8.13 -(*ML bindings for definitions and axioms*)
    8.14 -val invKey = thm "invKey";
    8.15 -val keysFor_def = thm "keysFor_def";
    8.16 -val parts_mono = thm "parts_mono";
    8.17 -val analz_mono = thm "analz_mono";
    8.18 -val synth_mono = thm "synth_mono";
    8.19 -val HPair_def = thm "HPair_def";
    8.20 -val symKeys_def = thm "symKeys_def";
    8.21 -
    8.22 -structure parts =
    8.23 -  struct
    8.24 -  val induct = thm "parts.induct";
    8.25 -  val Inj    = thm "parts.Inj";
    8.26 -  val Fst    = thm "parts.Fst";
    8.27 -  val Snd    = thm "parts.Snd";
    8.28 -  val Body   = thm "parts.Body";
    8.29 -  end;
    8.30 -
    8.31 -structure analz =
    8.32 -  struct
    8.33 -  val induct = thm "analz.induct";
    8.34 -  val Inj    = thm "analz.Inj";
    8.35 -  val Fst    = thm "analz.Fst";
    8.36 -  val Snd    = thm "analz.Snd";
    8.37 -  val Decrypt = thm "analz.Decrypt";
    8.38 -  end;
    8.39 -
    8.40 -structure synth =
    8.41 -  struct
    8.42 -  val induct = thm "synth.induct";
    8.43 -  val Inj    = thm "synth.Inj";
    8.44 -  val Agent  = thm "synth.Agent";
    8.45 -  val Number = thm "synth.Number";
    8.46 -  val Hash   = thm "synth.Hash";
    8.47 -  val Crypt  = thm "synth.Crypt";
    8.48 -  end;
    8.49 -
    8.50 -
    8.51 -(*Equations hold because constructors are injective; cannot prove for all f*)
    8.52 -Goal "(Friend x \\<in> Friend`A) = (x:A)";
    8.53 -by Auto_tac;
    8.54 -qed "Friend_image_eq";
    8.55 -
    8.56 -Goal "(Key x \\<in> Key`A) = (x\\<in>A)";
    8.57 -by Auto_tac;
    8.58 -qed "Key_image_eq";
    8.59 -
    8.60 -Goal "(Nonce x \\<notin> Key`A)";
    8.61 -by Auto_tac;
    8.62 -qed "Nonce_Key_image_eq";
    8.63 -Addsimps [Friend_image_eq, Key_image_eq, Nonce_Key_image_eq];
    8.64 -
    8.65 -
    8.66 -(** Inverse of keys **)
    8.67 -
    8.68 -Goal "(invKey K = invKey K') = (K=K')";
    8.69 -by Safe_tac;
    8.70 -by (rtac box_equals 1);
    8.71 -by (REPEAT (rtac invKey 2));
    8.72 -by (Asm_simp_tac 1);
    8.73 -qed "invKey_eq";
    8.74 -
    8.75 -Addsimps [invKey_eq];
    8.76 -
    8.77 -
    8.78 -(**** keysFor operator ****)
    8.79 -
    8.80 -Goalw [keysFor_def] "keysFor {} = {}";
    8.81 -by (Blast_tac 1);
    8.82 -qed "keysFor_empty";
    8.83 -
    8.84 -Goalw [keysFor_def] "keysFor (H Un H') = keysFor H Un keysFor H'";
    8.85 -by (Blast_tac 1);
    8.86 -qed "keysFor_Un";
    8.87 -
    8.88 -Goalw [keysFor_def] "keysFor (\\<Union>i\\<in>A. H i) = (\\<Union>i\\<in>A. keysFor (H i))";
    8.89 -by (Blast_tac 1);
    8.90 -qed "keysFor_UN";
    8.91 -
    8.92 -(*Monotonicity*)
    8.93 -Goalw [keysFor_def] "G\\<subseteq>H ==> keysFor(G) \\<subseteq> keysFor(H)";
    8.94 -by (Blast_tac 1);
    8.95 -qed "keysFor_mono";
    8.96 -
    8.97 -Goalw [keysFor_def] "keysFor (insert (Agent A) H) = keysFor H";
    8.98 -by Auto_tac;
    8.99 -qed "keysFor_insert_Agent";
   8.100 -
   8.101 -Goalw [keysFor_def] "keysFor (insert (Nonce N) H) = keysFor H";
   8.102 -by Auto_tac;
   8.103 -qed "keysFor_insert_Nonce";
   8.104 -
   8.105 -Goalw [keysFor_def] "keysFor (insert (Number N) H) = keysFor H";
   8.106 -by Auto_tac;
   8.107 -qed "keysFor_insert_Number";
   8.108 -
   8.109 -Goalw [keysFor_def] "keysFor (insert (Key K) H) = keysFor H";
   8.110 -by Auto_tac;
   8.111 -qed "keysFor_insert_Key";
   8.112 -
   8.113 -Goalw [keysFor_def] "keysFor (insert (Hash X) H) = keysFor H";
   8.114 -by Auto_tac;
   8.115 -qed "keysFor_insert_Hash";
   8.116 -
   8.117 -Goalw [keysFor_def] "keysFor (insert {|X,Y|} H) = keysFor H";
   8.118 -by Auto_tac;
   8.119 -qed "keysFor_insert_MPair";
   8.120 -
   8.121 -Goalw [keysFor_def]
   8.122 -    "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)";
   8.123 -by Auto_tac;
   8.124 -qed "keysFor_insert_Crypt";
   8.125 -
   8.126 -Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, 
   8.127 -          keysFor_insert_Agent, keysFor_insert_Nonce, 
   8.128 -	  keysFor_insert_Number, keysFor_insert_Key, 
   8.129 -          keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt];
   8.130 -AddSEs [keysFor_Un RS equalityD1 RS subsetD RS UnE,
   8.131 -	keysFor_UN RS equalityD1 RS subsetD RS UN_E];
   8.132 -
   8.133 -Goalw [keysFor_def] "keysFor (Key`E) = {}";
   8.134 -by Auto_tac;
   8.135 -qed "keysFor_image_Key";
   8.136 -Addsimps [keysFor_image_Key];
   8.137 -
   8.138 -Goalw [keysFor_def] "Crypt K X \\<in> H ==> invKey K \\<in> keysFor H";
   8.139 -by (Blast_tac 1);
   8.140 -qed "Crypt_imp_invKey_keysFor";
   8.141 -
   8.142 -
   8.143 -(**** Inductive relation "parts" ****)
   8.144 -
   8.145 -val major::prems = 
   8.146 -Goal "[| {|X,Y|} \\<in> parts H;       \
   8.147 -\         [| X \\<in> parts H; Y \\<in> parts H |] ==> P  \
   8.148 -\     |] ==> P";
   8.149 -by (cut_facts_tac [major] 1);
   8.150 -by (resolve_tac prems 1);
   8.151 -by (REPEAT (eresolve_tac [asm_rl, parts.Fst, parts.Snd] 1));
   8.152 -qed "MPair_parts";
   8.153 -
   8.154 -AddSEs [MPair_parts, make_elim parts.Body];
   8.155 -(*NB These two rules are UNSAFE in the formal sense, as they discard the
   8.156 -     compound message.  They work well on THIS FILE.  
   8.157 -  MPair_parts is left as SAFE because it speeds up proofs.
   8.158 -  The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*)
   8.159 -
   8.160 -Goal "H \\<subseteq> parts(H)";
   8.161 -by (Blast_tac 1);
   8.162 -qed "parts_increasing";
   8.163 -
   8.164 -bind_thm ("parts_insertI", impOfSubs (subset_insertI RS parts_mono));
   8.165 -
   8.166 -Goal "parts{} = {}";
   8.167 -by Safe_tac;
   8.168 -by (etac parts.induct 1);
   8.169 -by (ALLGOALS Blast_tac);
   8.170 -qed "parts_empty";
   8.171 -Addsimps [parts_empty];
   8.172 -
   8.173 -Goal "X\\<in> parts{} ==> P";
   8.174 -by (Asm_full_simp_tac 1);
   8.175 -qed "parts_emptyE";
   8.176 -AddSEs [parts_emptyE];
   8.177 -
   8.178 -(*WARNING: loops if H = {Y}, therefore must not be repeated!*)
   8.179 -Goal "X\\<in> parts H ==> \\<exists>Y\\<in>H. X\\<in> parts {Y}";
   8.180 -by (etac parts.induct 1);
   8.181 -by (ALLGOALS Blast_tac);
   8.182 -qed "parts_singleton";
   8.183 -
   8.184 -
   8.185 -(** Unions **)
   8.186 -
   8.187 -Goal "parts(G) Un parts(H) \\<subseteq> parts(G Un H)";
   8.188 -by (REPEAT (ares_tac [Un_least, parts_mono, Un_upper1, Un_upper2] 1));
   8.189 -val parts_Un_subset1 = result();
   8.190 -
   8.191 -Goal "parts(G Un H) \\<subseteq> parts(G) Un parts(H)";
   8.192 -by (rtac subsetI 1);
   8.193 -by (etac parts.induct 1);
   8.194 -by (ALLGOALS Blast_tac);
   8.195 -val parts_Un_subset2 = result();
   8.196 -
   8.197 -Goal "parts(G Un H) = parts(G) Un parts(H)";
   8.198 -by (REPEAT (ares_tac [equalityI, parts_Un_subset1, parts_Un_subset2] 1));
   8.199 -qed "parts_Un";
   8.200 -
   8.201 -Goal "parts (insert X H) = parts {X} Un parts H";
   8.202 -by (stac (read_instantiate [("A","H")] insert_is_Un) 1);
   8.203 -by (simp_tac (HOL_ss addsimps [parts_Un]) 1);
   8.204 -qed "parts_insert";
   8.205 -
   8.206 -(*TWO inserts to avoid looping.  This rewrite is better than nothing.
   8.207 -  Not suitable for Addsimps: its behaviour can be strange.*)
   8.208 -Goal "parts (insert X (insert Y H)) = parts {X} Un parts {Y} Un parts H";
   8.209 -by (simp_tac (simpset() addsimps [Un_assoc]) 1);
   8.210 -by (simp_tac (simpset() addsimps [parts_insert RS sym]) 1);
   8.211 -qed "parts_insert2";
   8.212 -
   8.213 -Goal "(\\<Union>x\\<in>A. parts(H x)) \\<subseteq> parts(\\<Union>x\\<in>A. H x)";
   8.214 -by (REPEAT (ares_tac [UN_least, parts_mono, UN_upper] 1));
   8.215 -val parts_UN_subset1 = result();
   8.216 -
   8.217 -Goal "parts(\\<Union>x\\<in>A. H x) \\<subseteq> (\\<Union>x\\<in>A. parts(H x))";
   8.218 -by (rtac subsetI 1);
   8.219 -by (etac parts.induct 1);
   8.220 -by (ALLGOALS Blast_tac);
   8.221 -val parts_UN_subset2 = result();
   8.222 -
   8.223 -Goal "parts(\\<Union>x\\<in>A. H x) = (\\<Union>x\\<in>A. parts(H x))";
   8.224 -by (REPEAT (ares_tac [equalityI, parts_UN_subset1, parts_UN_subset2] 1));
   8.225 -qed "parts_UN";
   8.226 -
   8.227 -(*Added to simplify arguments to parts, analz and synth.
   8.228 -  NOTE: the UN versions are no longer used!*)
   8.229 -Addsimps [parts_Un, parts_UN];
   8.230 -AddSEs [parts_Un RS equalityD1 RS subsetD RS UnE,
   8.231 -	parts_UN RS equalityD1 RS subsetD RS UN_E];
   8.232 -
   8.233 -Goal "insert X (parts H) \\<subseteq> parts(insert X H)";
   8.234 -by (blast_tac (claset() addIs [impOfSubs parts_mono]) 1);
   8.235 -qed "parts_insert_subset";
   8.236 -
   8.237 -(** Idempotence and transitivity **)
   8.238 -
   8.239 -Goal "X\\<in> parts (parts H) ==> X\\<in> parts H";
   8.240 -by (etac parts.induct 1);
   8.241 -by (ALLGOALS Blast_tac);
   8.242 -qed "parts_partsD";
   8.243 -AddSDs [parts_partsD];
   8.244 -
   8.245 -Goal "parts (parts H) = parts H";
   8.246 -by (Blast_tac 1);
   8.247 -qed "parts_idem";
   8.248 -Addsimps [parts_idem];
   8.249 -
   8.250 -Goal "[| X\\<in> parts G;  G \\<subseteq> parts H |] ==> X\\<in> parts H";
   8.251 -by (dtac parts_mono 1);
   8.252 -by (Blast_tac 1);
   8.253 -qed "parts_trans";
   8.254 -
   8.255 -(*Cut*)
   8.256 -Goal "[| Y\\<in> parts (insert X G);  X\\<in> parts H |] \
   8.257 -\              ==> Y\\<in> parts (G Un H)";
   8.258 -by (etac parts_trans 1);
   8.259 -by Auto_tac;
   8.260 -qed "parts_cut";
   8.261 -
   8.262 -Goal "X\\<in> parts H ==> parts (insert X H) = parts H";
   8.263 -by (fast_tac (claset() addSDs [parts_cut]
   8.264 -                       addIs  [parts_insertI] 
   8.265 -                       addss (simpset())) 1);
   8.266 -qed "parts_cut_eq";
   8.267 -
   8.268 -Addsimps [parts_cut_eq];
   8.269 -
   8.270 -
   8.271 -(** Rewrite rules for pulling out atomic messages **)
   8.272 -
   8.273 -fun parts_tac i =
   8.274 -  EVERY [rtac ([subsetI, parts_insert_subset] MRS equalityI) i,
   8.275 -         etac parts.induct i,
   8.276 -         Auto_tac];
   8.277 -
   8.278 -Goal "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)";
   8.279 -by (parts_tac 1);
   8.280 -qed "parts_insert_Agent";
   8.281 -
   8.282 -Goal "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)";
   8.283 -by (parts_tac 1);
   8.284 -qed "parts_insert_Nonce";
   8.285 -
   8.286 -Goal "parts (insert (Number N) H) = insert (Number N) (parts H)";
   8.287 -by (parts_tac 1);
   8.288 -qed "parts_insert_Number";
   8.289 -
   8.290 -Goal "parts (insert (Key K) H) = insert (Key K) (parts H)";
   8.291 -by (parts_tac 1);
   8.292 -qed "parts_insert_Key";
   8.293 -
   8.294 -Goal "parts (insert (Hash X) H) = insert (Hash X) (parts H)";
   8.295 -by (parts_tac 1);
   8.296 -qed "parts_insert_Hash";
   8.297 -
   8.298 -Goal "parts (insert (Crypt K X) H) = \
   8.299 -\         insert (Crypt K X) (parts (insert X H))";
   8.300 -by (rtac equalityI 1);
   8.301 -by (rtac subsetI 1);
   8.302 -by (etac parts.induct 1);
   8.303 -by Auto_tac;
   8.304 -by (etac parts.induct 1);
   8.305 -by (ALLGOALS (blast_tac (claset() addIs [parts.Body])));
   8.306 -qed "parts_insert_Crypt";
   8.307 -
   8.308 -Goal "parts (insert {|X,Y|} H) = \
   8.309 -\         insert {|X,Y|} (parts (insert X (insert Y H)))";
   8.310 -by (rtac equalityI 1);
   8.311 -by (rtac subsetI 1);
   8.312 -by (etac parts.induct 1);
   8.313 -by Auto_tac;
   8.314 -by (etac parts.induct 1);
   8.315 -by (ALLGOALS (blast_tac (claset() addIs [parts.Fst, parts.Snd])));
   8.316 -qed "parts_insert_MPair";
   8.317 -
   8.318 -Addsimps [parts_insert_Agent, parts_insert_Nonce, 
   8.319 -	  parts_insert_Number, parts_insert_Key, 
   8.320 -          parts_insert_Hash, parts_insert_Crypt, parts_insert_MPair];
   8.321 -
   8.322 -
   8.323 -Goal "parts (Key`N) = Key`N";
   8.324 -by Auto_tac;
   8.325 -by (etac parts.induct 1);
   8.326 -by Auto_tac;
   8.327 -qed "parts_image_Key";
   8.328 -Addsimps [parts_image_Key];
   8.329 -
   8.330 -
   8.331 -(*In any message, there is an upper bound N on its greatest nonce.*)
   8.332 -Goal "\\<exists>N. \\<forall>n. N\\<le>n --> Nonce n \\<notin> parts {msg}";
   8.333 -by (induct_tac "msg" 1);
   8.334 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [exI, parts_insert2])));
   8.335 -(*MPair case: blast_tac works out the necessary sum itself!*)
   8.336 -by (blast_tac (claset() addSEs [add_leE]) 2);
   8.337 -(*Nonce case*)
   8.338 -by (res_inst_tac [("x","N + Suc nat")] exI 1);
   8.339 -by (auto_tac (claset() addSEs [add_leE], simpset()));
   8.340 -qed "msg_Nonce_supply";
   8.341 -
   8.342 -
   8.343 -(**** Inductive relation "analz" ****)
   8.344 -
   8.345 -val major::prems = 
   8.346 -Goal "[| {|X,Y|} \\<in> analz H;       \
   8.347 -\            [| X \\<in> analz H; Y \\<in> analz H |] ==> P  \
   8.348 -\         |] ==> P";
   8.349 -by (cut_facts_tac [major] 1);
   8.350 -by (resolve_tac prems 1);
   8.351 -by (REPEAT (eresolve_tac [asm_rl, analz.Fst, analz.Snd] 1));
   8.352 -qed "MPair_analz";
   8.353 -
   8.354 -AddSEs [MPair_analz];     (*Making it safe speeds up proofs*)
   8.355 -
   8.356 -Goal "H \\<subseteq> analz(H)";
   8.357 -by (Blast_tac 1);
   8.358 -qed "analz_increasing";
   8.359 -
   8.360 -Goal "analz H \\<subseteq> parts H";
   8.361 -by (rtac subsetI 1);
   8.362 -by (etac analz.induct 1);
   8.363 -by (ALLGOALS Blast_tac);
   8.364 -qed "analz_subset_parts";
   8.365 -
   8.366 -bind_thm ("not_parts_not_analz", analz_subset_parts RS contra_subsetD);
   8.367 -
   8.368 -
   8.369 -Goal "parts (analz H) = parts H";
   8.370 -by (rtac equalityI 1);
   8.371 -by (rtac (analz_subset_parts RS parts_mono RS subset_trans) 1);
   8.372 -by (Simp_tac 1);
   8.373 -by (blast_tac (claset() addIs [analz_increasing RS parts_mono RS subsetD]) 1);
   8.374 -qed "parts_analz";
   8.375 -Addsimps [parts_analz];
   8.376 -
   8.377 -Goal "analz (parts H) = parts H";
   8.378 -by Auto_tac;
   8.379 -by (etac analz.induct 1);
   8.380 -by Auto_tac;
   8.381 -qed "analz_parts";
   8.382 -Addsimps [analz_parts];
   8.383 -
   8.384 -bind_thm ("analz_insertI", impOfSubs (subset_insertI RS analz_mono));
   8.385 -
   8.386 -(** General equational properties **)
   8.387 -
   8.388 -Goal "analz{} = {}";
   8.389 -by Safe_tac;
   8.390 -by (etac analz.induct 1);
   8.391 -by (ALLGOALS Blast_tac);
   8.392 -qed "analz_empty";
   8.393 -Addsimps [analz_empty];
   8.394 -
   8.395 -(*Converse fails: we can analz more from the union than from the 
   8.396 -  separate parts, as a key in one might decrypt a message in the other*)
   8.397 -Goal "analz(G) Un analz(H) \\<subseteq> analz(G Un H)";
   8.398 -by (REPEAT (ares_tac [Un_least, analz_mono, Un_upper1, Un_upper2] 1));
   8.399 -qed "analz_Un";
   8.400 -
   8.401 -Goal "insert X (analz H) \\<subseteq> analz(insert X H)";
   8.402 -by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
   8.403 -qed "analz_insert";
   8.404 -
   8.405 -(** Rewrite rules for pulling out atomic messages **)
   8.406 -
   8.407 -fun analz_tac i =
   8.408 -  EVERY [rtac ([subsetI, analz_insert] MRS equalityI) i,
   8.409 -         etac analz.induct i,
   8.410 -         Auto_tac];
   8.411 -
   8.412 -Goal "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)";
   8.413 -by (analz_tac 1);
   8.414 -qed "analz_insert_Agent";
   8.415 -
   8.416 -Goal "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)";
   8.417 -by (analz_tac 1);
   8.418 -qed "analz_insert_Nonce";
   8.419 -
   8.420 -Goal "analz (insert (Number N) H) = insert (Number N) (analz H)";
   8.421 -by (analz_tac 1);
   8.422 -qed "analz_insert_Number";
   8.423 -
   8.424 -Goal "analz (insert (Hash X) H) = insert (Hash X) (analz H)";
   8.425 -by (analz_tac 1);
   8.426 -qed "analz_insert_Hash";
   8.427 -
   8.428 -(*Can only pull out Keys if they are not needed to decrypt the rest*)
   8.429 -Goalw [keysFor_def]
   8.430 -    "K \\<notin> keysFor (analz H) ==>  \
   8.431 -\         analz (insert (Key K) H) = insert (Key K) (analz H)";
   8.432 -by (analz_tac 1);
   8.433 -qed "analz_insert_Key";
   8.434 -
   8.435 -Goal "analz (insert {|X,Y|} H) = \
   8.436 -\         insert {|X,Y|} (analz (insert X (insert Y H)))";
   8.437 -by (rtac equalityI 1);
   8.438 -by (rtac subsetI 1);
   8.439 -by (etac analz.induct 1);
   8.440 -by Auto_tac;
   8.441 -by (etac analz.induct 1);
   8.442 -by (ALLGOALS (blast_tac (claset() addIs [analz.Fst, analz.Snd])));
   8.443 -qed "analz_insert_MPair";
   8.444 -
   8.445 -(*Can pull out enCrypted message if the Key is not known*)
   8.446 -Goal "Key (invKey K) \\<notin> analz H ==>  \
   8.447 -\              analz (insert (Crypt K X) H) = \
   8.448 -\              insert (Crypt K X) (analz H)";
   8.449 -by (analz_tac 1);
   8.450 -qed "analz_insert_Crypt";
   8.451 -
   8.452 -Goal "Key (invKey K) \\<in> analz H ==>  \
   8.453 -\              analz (insert (Crypt K X) H) \\<subseteq> \
   8.454 -\              insert (Crypt K X) (analz (insert X H))";
   8.455 -by (rtac subsetI 1);
   8.456 -by (eres_inst_tac [("xa","x")] analz.induct 1);
   8.457 -by Auto_tac;
   8.458 -val lemma1 = result();
   8.459 -
   8.460 -Goal "Key (invKey K) \\<in> analz H ==>  \
   8.461 -\              insert (Crypt K X) (analz (insert X H)) \\<subseteq> \
   8.462 -\              analz (insert (Crypt K X) H)";
   8.463 -by Auto_tac;
   8.464 -by (eres_inst_tac [("xa","x")] analz.induct 1);
   8.465 -by Auto_tac;
   8.466 -by (blast_tac (claset() addIs [analz_insertI, analz.Decrypt]) 1);
   8.467 -val lemma2 = result();
   8.468 -
   8.469 -Goal "Key (invKey K) \\<in> analz H ==>  \
   8.470 -\              analz (insert (Crypt K X) H) = \
   8.471 -\              insert (Crypt K X) (analz (insert X H))";
   8.472 -by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1));
   8.473 -qed "analz_insert_Decrypt";
   8.474 -
   8.475 -(*Case analysis: either the message is secure, or it is not!
   8.476 -  Effective, but can cause subgoals to blow up!
   8.477 -  Use with split_if;  apparently split_tac does not cope with patterns
   8.478 -  such as "analz (insert (Crypt K X) H)" *)
   8.479 -Goal "analz (insert (Crypt K X) H) =                \
   8.480 -\         (if (Key (invKey K) \\<in> analz H)                \
   8.481 -\          then insert (Crypt K X) (analz (insert X H)) \
   8.482 -\          else insert (Crypt K X) (analz H))";
   8.483 -by (case_tac "Key (invKey K)  \\<in> analz H " 1);
   8.484 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [analz_insert_Crypt, 
   8.485 -						analz_insert_Decrypt])));
   8.486 -qed "analz_Crypt_if";
   8.487 -
   8.488 -Addsimps [analz_insert_Agent, analz_insert_Nonce, 
   8.489 -	  analz_insert_Number, analz_insert_Key, 
   8.490 -          analz_insert_Hash, analz_insert_MPair, analz_Crypt_if];
   8.491 -
   8.492 -(*This rule supposes "for the sake of argument" that we have the key.*)
   8.493 -Goal  "analz (insert (Crypt K X) H) \\<subseteq>  \
   8.494 -\          insert (Crypt K X) (analz (insert X H))";
   8.495 -by (rtac subsetI 1);
   8.496 -by (etac analz.induct 1);
   8.497 -by Auto_tac;
   8.498 -qed "analz_insert_Crypt_subset";
   8.499 -
   8.500 -
   8.501 -Goal "analz (Key`N) = Key`N";
   8.502 -by Auto_tac;
   8.503 -by (etac analz.induct 1);
   8.504 -by Auto_tac;
   8.505 -qed "analz_image_Key";
   8.506 -
   8.507 -Addsimps [analz_image_Key];
   8.508 -
   8.509 -
   8.510 -(** Idempotence and transitivity **)
   8.511 -
   8.512 -Goal "X\\<in> analz (analz H) ==> X\\<in> analz H";
   8.513 -by (etac analz.induct 1);
   8.514 -by (ALLGOALS Blast_tac);
   8.515 -qed "analz_analzD";
   8.516 -AddSDs [analz_analzD];
   8.517 -
   8.518 -Goal "analz (analz H) = analz H";
   8.519 -by (Blast_tac 1);
   8.520 -qed "analz_idem";
   8.521 -Addsimps [analz_idem];
   8.522 -
   8.523 -Goal "[| X\\<in> analz G;  G \\<subseteq> analz H |] ==> X\\<in> analz H";
   8.524 -by (dtac analz_mono 1);
   8.525 -by (Blast_tac 1);
   8.526 -qed "analz_trans";
   8.527 -
   8.528 -(*Cut; Lemma 2 of Lowe*)
   8.529 -Goal "[| Y\\<in> analz (insert X H);  X\\<in> analz H |] ==> Y\\<in> analz H";
   8.530 -by (etac analz_trans 1);
   8.531 -by (Blast_tac 1);
   8.532 -qed "analz_cut";
   8.533 -
   8.534 -(*Cut can be proved easily by induction on
   8.535 -   "Y: analz (insert X H) ==> X: analz H --> Y: analz H"
   8.536 -*)
   8.537 -
   8.538 -(*This rewrite rule helps in the simplification of messages that involve
   8.539 -  the forwarding of unknown components (X).  Without it, removing occurrences
   8.540 -  of X can be very complicated. *)
   8.541 -Goal "X\\<in> analz H ==> analz (insert X H) = analz H";
   8.542 -by (blast_tac (claset() addIs [analz_cut, analz_insertI]) 1);
   8.543 -qed "analz_insert_eq";
   8.544 -
   8.545 -
   8.546 -(** A congruence rule for "analz" **)
   8.547 -
   8.548 -Goal "[| analz G \\<subseteq> analz G'; analz H \\<subseteq> analz H' \
   8.549 -\              |] ==> analz (G Un H) \\<subseteq> analz (G' Un H')";
   8.550 -by (Clarify_tac 1);
   8.551 -by (etac analz.induct 1);
   8.552 -by (ALLGOALS (best_tac (claset() addIs [analz_mono RS subsetD])));
   8.553 -qed "analz_subset_cong";
   8.554 -
   8.555 -Goal "[| analz G = analz G'; analz H = analz H' \
   8.556 -\              |] ==> analz (G Un H) = analz (G' Un H')";
   8.557 -by (REPEAT_FIRST (ares_tac [equalityI, analz_subset_cong]
   8.558 -          ORELSE' etac equalityE));
   8.559 -qed "analz_cong";
   8.560 -
   8.561 -
   8.562 -Goal "analz H = analz H' ==> analz(insert X H) = analz(insert X H')";
   8.563 -by (asm_simp_tac (simpset() addsimps [insert_def] delsimps [singleton_conv]
   8.564 -                            setloop (rtac analz_cong)) 1);
   8.565 -qed "analz_insert_cong";
   8.566 -
   8.567 -(*If there are no pairs or encryptions then analz does nothing*)
   8.568 -Goal "[| \\<forall>X Y. {|X,Y|} \\<notin> H;  \\<forall>X K. Crypt K X \\<notin> H |] ==> analz H = H";
   8.569 -by Safe_tac;
   8.570 -by (etac analz.induct 1);
   8.571 -by (ALLGOALS Blast_tac);
   8.572 -qed "analz_trivial";
   8.573 -
   8.574 -(*These two are obsolete (with a single Spy) but cost little to prove...*)
   8.575 -Goal "X\\<in> analz (\\<Union>i\\<in>A. analz (H i)) ==> X\\<in> analz (\\<Union>i\\<in>A. H i)";
   8.576 -by (etac analz.induct 1);
   8.577 -by (ALLGOALS (blast_tac (claset() addIs [impOfSubs analz_mono])));
   8.578 -val lemma = result();
   8.579 -
   8.580 -Goal "analz (\\<Union>i\\<in>A. analz (H i)) = analz (\\<Union>i\\<in>A. H i)";
   8.581 -by (blast_tac (claset() addIs [lemma, impOfSubs analz_mono]) 1);
   8.582 -qed "analz_UN_analz";
   8.583 -Addsimps [analz_UN_analz];
   8.584 -
   8.585 -
   8.586 -(**** Inductive relation "synth" ****)
   8.587 -
   8.588 -Goal "H \\<subseteq> synth(H)";
   8.589 -by (Blast_tac 1);
   8.590 -qed "synth_increasing";
   8.591 -
   8.592 -(** Unions **)
   8.593 -
   8.594 -(*Converse fails: we can synth more from the union than from the 
   8.595 -  separate parts, building a compound message using elements of each.*)
   8.596 -Goal "synth(G) Un synth(H) \\<subseteq> synth(G Un H)";
   8.597 -by (REPEAT (ares_tac [Un_least, synth_mono, Un_upper1, Un_upper2] 1));
   8.598 -qed "synth_Un";
   8.599 -
   8.600 -Goal "insert X (synth H) \\<subseteq> synth(insert X H)";
   8.601 -by (blast_tac (claset() addIs [impOfSubs synth_mono]) 1);
   8.602 -qed "synth_insert";
   8.603 -
   8.604 -(** Idempotence and transitivity **)
   8.605 -
   8.606 -Goal "X\\<in> synth (synth H) ==> X\\<in> synth H";
   8.607 -by (etac synth.induct 1);
   8.608 -by (ALLGOALS Blast_tac);
   8.609 -qed "synth_synthD";
   8.610 -AddSDs [synth_synthD];
   8.611 -
   8.612 -Goal "synth (synth H) = synth H";
   8.613 -by (Blast_tac 1);
   8.614 -qed "synth_idem";
   8.615 -
   8.616 -Goal "[| X\\<in> synth G;  G \\<subseteq> synth H |] ==> X\\<in> synth H";
   8.617 -by (dtac synth_mono 1);
   8.618 -by (Blast_tac 1);
   8.619 -qed "synth_trans";
   8.620 -
   8.621 -(*Cut; Lemma 2 of Lowe*)
   8.622 -Goal "[| Y\\<in> synth (insert X H);  X\\<in> synth H |] ==> Y\\<in> synth H";
   8.623 -by (etac synth_trans 1);
   8.624 -by (Blast_tac 1);
   8.625 -qed "synth_cut";
   8.626 -
   8.627 -Goal "Agent A \\<in> synth H";
   8.628 -by (Blast_tac 1);
   8.629 -qed "Agent_synth";
   8.630 -
   8.631 -Goal "Number n \\<in> synth H";
   8.632 -by (Blast_tac 1);
   8.633 -qed "Number_synth";
   8.634 -
   8.635 -Goal "(Nonce N \\<in> synth H) = (Nonce N \\<in> H)";
   8.636 -by (Blast_tac 1);
   8.637 -qed "Nonce_synth_eq";
   8.638 -
   8.639 -Goal "(Key K \\<in> synth H) = (Key K \\<in> H)";
   8.640 -by (Blast_tac 1);
   8.641 -qed "Key_synth_eq";
   8.642 -
   8.643 -Goal "Key K \\<notin> H ==> (Crypt K X \\<in> synth H) = (Crypt K X \\<in> H)";
   8.644 -by (Blast_tac 1);
   8.645 -qed "Crypt_synth_eq";
   8.646 -
   8.647 -Addsimps [Agent_synth, Number_synth, 
   8.648 -	  Nonce_synth_eq, Key_synth_eq, Crypt_synth_eq];
   8.649 -
   8.650 -
   8.651 -Goalw [keysFor_def]
   8.652 -    "keysFor (synth H) = keysFor H Un invKey`{K. Key K \\<in> H}";
   8.653 -by (Blast_tac 1);
   8.654 -qed "keysFor_synth";
   8.655 -Addsimps [keysFor_synth];
   8.656 -
   8.657 -
   8.658 -(*** Combinations of parts, analz and synth ***)
   8.659 -
   8.660 -Goal "parts (synth H) = parts H Un synth H";
   8.661 -by (rtac equalityI 1);
   8.662 -by (rtac subsetI 1);
   8.663 -by (etac parts.induct 1);
   8.664 -by (ALLGOALS
   8.665 -    (blast_tac (claset() addIs [synth_increasing RS parts_mono RS subsetD,
   8.666 -                                parts.Fst, parts.Snd, parts.Body])));
   8.667 -qed "parts_synth";
   8.668 -Addsimps [parts_synth];
   8.669 -
   8.670 -Goal "analz (analz G Un H) = analz (G Un H)";
   8.671 -by (REPEAT_FIRST (resolve_tac [equalityI, analz_subset_cong]));
   8.672 -by (ALLGOALS Simp_tac);
   8.673 -qed "analz_analz_Un";
   8.674 -
   8.675 -Goal "analz (synth G Un H) = analz (G Un H) Un synth G";
   8.676 -by (rtac equalityI 1);
   8.677 -by (rtac subsetI 1);
   8.678 -by (etac analz.induct 1);
   8.679 -by (blast_tac (claset() addIs [impOfSubs analz_mono]) 5);
   8.680 -by (ALLGOALS 
   8.681 -    (blast_tac (claset() addIs [analz.Fst, analz.Snd, analz.Decrypt])));
   8.682 -qed "analz_synth_Un";
   8.683 -
   8.684 -Goal "analz (synth H) = analz H Un synth H";
   8.685 -by (cut_inst_tac [("H","{}")] analz_synth_Un 1);
   8.686 -by (Full_simp_tac 1);
   8.687 -qed "analz_synth";
   8.688 -Addsimps [analz_analz_Un, analz_synth_Un, analz_synth];
   8.689 -
   8.690 -
   8.691 -(** For reasoning about the Fake rule in traces **)
   8.692 -
   8.693 -Goal "X\\<in> G ==> parts(insert X H) \\<subseteq> parts G Un parts H";
   8.694 -by (rtac ([parts_mono, parts_Un_subset2] MRS subset_trans) 1);
   8.695 -by (Blast_tac 1);
   8.696 -qed "parts_insert_subset_Un";
   8.697 -
   8.698 -(*More specifically for Fake.  Very occasionally we could do with a version
   8.699 -  of the form  parts{X} \\<subseteq> synth (analz H) Un parts H *)
   8.700 -Goal "X\\<in> synth (analz H) ==> \
   8.701 -\     parts (insert X H) \\<subseteq> synth (analz H) Un parts H";
   8.702 -by (dtac parts_insert_subset_Un 1);
   8.703 -by (Full_simp_tac 1);
   8.704 -by (Blast_tac 1);
   8.705 -qed "Fake_parts_insert";
   8.706 -
   8.707 -(*H is sometimes (Key ` KK Un spies evs), so can't put G=H*)
   8.708 -Goal "X\\<in> synth (analz G) ==> \
   8.709 -\     analz (insert X H) \\<subseteq> synth (analz G) Un analz (G Un H)";
   8.710 -by (rtac subsetI 1);
   8.711 -by (subgoal_tac "x \\<in> analz (synth (analz G) Un H)" 1);
   8.712 -by (blast_tac (claset() addIs [impOfSubs analz_mono,
   8.713 -			       impOfSubs (analz_mono RS synth_mono)]) 2);
   8.714 -by (Full_simp_tac 1);
   8.715 -by (Blast_tac 1);
   8.716 -qed "Fake_analz_insert";
   8.717 -
   8.718 -Goal "(X\\<in> analz H & X\\<in> parts H) = (X\\<in> analz H)";
   8.719 -by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1);
   8.720 -val analz_conj_parts = result();
   8.721 -
   8.722 -Goal "(X\\<in> analz H | X\\<in> parts H) = (X\\<in> parts H)";
   8.723 -by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1);
   8.724 -val analz_disj_parts = result();
   8.725 -
   8.726 -AddIffs [analz_conj_parts, analz_disj_parts];
   8.727 -
   8.728 -(*Without this equation, other rules for synth and analz would yield
   8.729 -  redundant cases*)
   8.730 -Goal "({|X,Y|} \\<in> synth (analz H)) = \
   8.731 -\     (X \\<in> synth (analz H) & Y \\<in> synth (analz H))";
   8.732 -by (Blast_tac 1);
   8.733 -qed "MPair_synth_analz";
   8.734 -
   8.735 -AddIffs [MPair_synth_analz];
   8.736 -
   8.737 -Goal "[| Key K \\<in> analz H;  Key (invKey K) \\<in> analz H |] \
   8.738 -\      ==> (Crypt K X \\<in> synth (analz H)) = (X \\<in> synth (analz H))";
   8.739 -by (Blast_tac 1);
   8.740 -qed "Crypt_synth_analz";
   8.741 -
   8.742 -
   8.743 -Goal "X \\<notin> synth (analz H) \
   8.744 -\     ==> (Hash{|X,Y|} \\<in> synth (analz H)) = (Hash{|X,Y|} \\<in> analz H)";
   8.745 -by (Blast_tac 1);
   8.746 -qed "Hash_synth_analz";
   8.747 -Addsimps [Hash_synth_analz];
   8.748 -
   8.749 -
   8.750 -(**** HPair: a combination of Hash and MPair ****)
   8.751 -
   8.752 -(*** Freeness ***)
   8.753 -
   8.754 -Goalw [HPair_def] "Agent A ~= Hash[X] Y";
   8.755 -by (Simp_tac 1);
   8.756 -qed "Agent_neq_HPair";
   8.757 -
   8.758 -Goalw [HPair_def] "Nonce N ~= Hash[X] Y";
   8.759 -by (Simp_tac 1);
   8.760 -qed "Nonce_neq_HPair";
   8.761 -
   8.762 -Goalw [HPair_def] "Number N ~= Hash[X] Y";
   8.763 -by (Simp_tac 1);
   8.764 -qed "Number_neq_HPair";
   8.765 -
   8.766 -Goalw [HPair_def] "Key K ~= Hash[X] Y";
   8.767 -by (Simp_tac 1);
   8.768 -qed "Key_neq_HPair";
   8.769 -
   8.770 -Goalw [HPair_def] "Hash Z ~= Hash[X] Y";
   8.771 -by (Simp_tac 1);
   8.772 -qed "Hash_neq_HPair";
   8.773 -
   8.774 -Goalw [HPair_def] "Crypt K X' ~= Hash[X] Y";
   8.775 -by (Simp_tac 1);
   8.776 -qed "Crypt_neq_HPair";
   8.777 -
   8.778 -val HPair_neqs = [Agent_neq_HPair, Nonce_neq_HPair, Number_neq_HPair, 
   8.779 -                  Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair];
   8.780 -
   8.781 -AddIffs HPair_neqs;
   8.782 -AddIffs (HPair_neqs RL [not_sym]);
   8.783 -
   8.784 -Goalw [HPair_def] "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)";
   8.785 -by (Simp_tac 1);
   8.786 -qed "HPair_eq";
   8.787 -
   8.788 -Goalw [HPair_def] "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)";
   8.789 -by (Simp_tac 1);
   8.790 -qed "MPair_eq_HPair";
   8.791 -
   8.792 -Goalw [HPair_def] "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)";
   8.793 -by Auto_tac;
   8.794 -qed "HPair_eq_MPair";
   8.795 -
   8.796 -AddIffs [HPair_eq, MPair_eq_HPair, HPair_eq_MPair];
   8.797 -
   8.798 -
   8.799 -(*** Specialized laws, proved in terms of those for Hash and MPair ***)
   8.800 -
   8.801 -Goalw [HPair_def] "keysFor (insert (Hash[X] Y) H) = keysFor H";
   8.802 -by (Simp_tac 1);
   8.803 -qed "keysFor_insert_HPair";
   8.804 -
   8.805 -Goalw [HPair_def]
   8.806 -    "parts (insert (Hash[X] Y) H) = \
   8.807 -\    insert (Hash[X] Y) (insert (Hash{|X,Y|}) (parts (insert Y H)))";
   8.808 -by (Simp_tac 1);
   8.809 -qed "parts_insert_HPair";
   8.810 -
   8.811 -Goalw [HPair_def]
   8.812 -    "analz (insert (Hash[X] Y) H) = \
   8.813 -\    insert (Hash[X] Y) (insert (Hash{|X,Y|}) (analz (insert Y H)))";
   8.814 -by (Simp_tac 1);
   8.815 -qed "analz_insert_HPair";
   8.816 -
   8.817 -Goalw [HPair_def] "X \\<notin> synth (analz H) \
   8.818 -\   ==> (Hash[X] Y \\<in> synth (analz H)) = \
   8.819 -\       (Hash {|X, Y|} \\<in> analz H & Y \\<in> synth (analz H))";
   8.820 -by (Simp_tac 1);
   8.821 -by (Blast_tac 1);
   8.822 -qed "HPair_synth_analz";
   8.823 -
   8.824 -Addsimps [keysFor_insert_HPair, parts_insert_HPair, analz_insert_HPair, 
   8.825 -          HPair_synth_analz, HPair_synth_analz];
   8.826 -
   8.827 -
   8.828 -(*We do NOT want Crypt... messages broken up in protocols!!*)
   8.829 -Delrules [make_elim parts.Body];
   8.830 -
   8.831 -
   8.832 -(** Rewrites to push in Key and Crypt messages, so that other messages can
   8.833 -    be pulled out using the analz_insert rules **)
   8.834 -
   8.835 -fun insComm x y = inst "x" x (inst "y" y insert_commute);
   8.836 -
   8.837 -val pushKeys = map (insComm "Key ?K") 
   8.838 -                   ["Agent ?C", "Nonce ?N", "Number ?N", 
   8.839 -		    "Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"];
   8.840 -
   8.841 -val pushCrypts = map (insComm "Crypt ?X ?K") 
   8.842 -                     ["Agent ?C", "Nonce ?N", "Number ?N", 
   8.843 -		      "Hash ?X'", "MPair ?X' ?Y"];
   8.844 -
   8.845 -(*Cannot be added with Addsimps -- we don't always want to re-order messages*)
   8.846 -bind_thms ("pushes", pushKeys@pushCrypts);
   8.847 -
   8.848 -
   8.849 -(*** Tactics useful for many protocol proofs ***)
   8.850 -
   8.851 -(*Prove base case (subgoal i) and simplify others.  A typical base case
   8.852 -  concerns  Crypt K X \\<notin> Key`shrK`bad  and cannot be proved by rewriting
   8.853 -  alone.*)
   8.854 -fun prove_simple_subgoals_tac i = 
   8.855 -    force_tac (claset(), simpset() addsimps [image_eq_UN]) i THEN
   8.856 -    ALLGOALS Asm_simp_tac;
   8.857 -
   8.858 -fun Fake_parts_insert_tac i = 
   8.859 -    blast_tac (claset() addIs [parts_insertI]
   8.860 -			addDs [impOfSubs analz_subset_parts,
   8.861 -			       impOfSubs Fake_parts_insert]) i;
   8.862 -
   8.863 -(*Apply rules to break down assumptions of the form
   8.864 -  Y \\<in> parts(insert X H)  and  Y \\<in> analz(insert X H)
   8.865 -*)
   8.866 -val Fake_insert_tac = 
   8.867 -    dresolve_tac [impOfSubs Fake_analz_insert,
   8.868 -                  impOfSubs Fake_parts_insert] THEN'
   8.869 -    eresolve_tac [asm_rl, synth.Inj];
   8.870 -
   8.871 -fun Fake_insert_simp_tac ss i = 
   8.872 -    REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
   8.873 -
   8.874 -
   8.875 -(*Analysis of Fake cases.  Also works for messages that forward unknown parts,
   8.876 -  but this application is no longer necessary if analz_insert_eq is used.
   8.877 -  Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
   8.878 -  DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
   8.879 -
   8.880 -fun atomic_spy_analz_tac (cs,ss) = SELECT_GOAL
   8.881 -    (Fake_insert_simp_tac ss 1
   8.882 -     THEN
   8.883 -     IF_UNSOLVED (Blast.depth_tac
   8.884 -		  (cs addIs [analz_insertI,
   8.885 -				   impOfSubs analz_subset_parts]) 4 1));
   8.886 -
   8.887 -(*The explicit claset and simpset arguments help it work with Isar*)
   8.888 -fun gen_spy_analz_tac (cs,ss) i =
   8.889 -  DETERM
   8.890 -   (SELECT_GOAL
   8.891 -     (EVERY 
   8.892 -      [  (*push in occurrences of X...*)
   8.893 -       (REPEAT o CHANGED)
   8.894 -           (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
   8.895 -       (*...allowing further simplifications*)
   8.896 -       simp_tac ss 1,
   8.897 -       REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
   8.898 -       DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i);
   8.899 -
   8.900 -fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i;
   8.901 -
   8.902 -(*By default only o_apply is built-in.  But in the presence of eta-expansion
   8.903 -  this means that some terms displayed as (f o g) will be rewritten, and others
   8.904 -  will not!*)
   8.905 -Addsimps [o_def];
     9.1 --- a/src/HOL/Auth/NS_Public.thy	Sat Apr 26 12:38:17 2003 +0200
     9.2 +++ b/src/HOL/Auth/NS_Public.thy	Sat Apr 26 12:38:42 2003 +0200
     9.3 @@ -50,7 +50,8 @@
     9.4  apply (intro exI bexI)
     9.5  apply (rule_tac [2] ns_public.Nil [THEN ns_public.NS1, THEN ns_public.NS2, 
     9.6                                     THEN ns_public.NS3])
     9.7 -by possibility
     9.8 +apply possibility
     9.9 +done
    9.10  
    9.11  
    9.12  (**** Inductive proofs about ns_public ****)
    10.1 --- a/src/HOL/Auth/NS_Shared.thy	Sat Apr 26 12:38:17 2003 +0200
    10.2 +++ b/src/HOL/Auth/NS_Shared.thy	Sat Apr 26 12:38:42 2003 +0200
    10.3 @@ -16,60 +16,60 @@
    10.4  inductive "ns_shared"
    10.5   intros
    10.6  	(*Initial trace is empty*)
    10.7 -  Nil:  "[] \\<in> ns_shared"
    10.8 +  Nil:  "[] \<in> ns_shared"
    10.9  	(*The spy MAY say anything he CAN say.  We do not expect him to
   10.10  	  invent new nonces here, but he can also use NS1.  Common to
   10.11  	  all similar protocols.*)
   10.12 -  Fake: "\\<lbrakk>evsf \\<in> ns_shared;  X \\<in> synth (analz (spies evsf))\\<rbrakk>
   10.13 -	 \\<Longrightarrow> Says Spy B X # evsf \\<in> ns_shared"
   10.14 +  Fake: "\<lbrakk>evsf \<in> ns_shared;  X \<in> synth (analz (spies evsf))\<rbrakk>
   10.15 +	 \<Longrightarrow> Says Spy B X # evsf \<in> ns_shared"
   10.16  
   10.17  	(*Alice initiates a protocol run, requesting to talk to any B*)
   10.18 -  NS1:  "\\<lbrakk>evs1 \\<in> ns_shared;  Nonce NA \\<notin> used evs1\\<rbrakk>
   10.19 -	 \\<Longrightarrow> Says A Server \\<lbrace>Agent A, Agent B, Nonce NA\\<rbrace> # evs1  \\<in>  ns_shared"
   10.20 +  NS1:  "\<lbrakk>evs1 \<in> ns_shared;  Nonce NA \<notin> used evs1\<rbrakk>
   10.21 +	 \<Longrightarrow> Says A Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> # evs1  \<in>  ns_shared"
   10.22  
   10.23  	(*Server's response to Alice's message.
   10.24  	  !! It may respond more than once to A's request !!
   10.25  	  Server doesn't know who the true sender is, hence the A' in
   10.26  	      the sender field.*)
   10.27 -  NS2:  "\\<lbrakk>evs2 \\<in> ns_shared;  Key KAB \\<notin> used evs2;
   10.28 -	  Says A' Server \\<lbrace>Agent A, Agent B, Nonce NA\\<rbrace> \\<in> set evs2\\<rbrakk>
   10.29 -	 \\<Longrightarrow> Says Server A
   10.30 +  NS2:  "\<lbrakk>evs2 \<in> ns_shared;  Key KAB \<notin> used evs2;
   10.31 +	  Says A' Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in> set evs2\<rbrakk>
   10.32 +	 \<Longrightarrow> Says Server A
   10.33  	       (Crypt (shrK A)
   10.34 -		  \\<lbrace>Nonce NA, Agent B, Key KAB,
   10.35 -		    (Crypt (shrK B) \\<lbrace>Key KAB, Agent A\\<rbrace>)\\<rbrace>)
   10.36 -	       # evs2 \\<in> ns_shared"
   10.37 +		  \<lbrace>Nonce NA, Agent B, Key KAB,
   10.38 +		    (Crypt (shrK B) \<lbrace>Key KAB, Agent A\<rbrace>)\<rbrace>)
   10.39 +	       # evs2 \<in> ns_shared"
   10.40  
   10.41  	 (*We can't assume S=Server.  Agent A "remembers" her nonce.
   10.42 -	   Need A \\<noteq> Server because we allow messages to self.*)
   10.43 -  NS3:  "\\<lbrakk>evs3 \\<in> ns_shared;  A \\<noteq> Server;
   10.44 -	  Says S A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs3;
   10.45 -	  Says A Server \\<lbrace>Agent A, Agent B, Nonce NA\\<rbrace> \\<in> set evs3\\<rbrakk>
   10.46 -	 \\<Longrightarrow> Says A B X # evs3 \\<in> ns_shared"
   10.47 +	   Need A \<noteq> Server because we allow messages to self.*)
   10.48 +  NS3:  "\<lbrakk>evs3 \<in> ns_shared;  A \<noteq> Server;
   10.49 +	  Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs3;
   10.50 +	  Says A Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in> set evs3\<rbrakk>
   10.51 +	 \<Longrightarrow> Says A B X # evs3 \<in> ns_shared"
   10.52  
   10.53  	(*Bob's nonce exchange.  He does not know who the message came
   10.54  	  from, but responds to A because she is mentioned inside.*)
   10.55 -  NS4:  "\\<lbrakk>evs4 \\<in> ns_shared;  Nonce NB \\<notin> used evs4;
   10.56 -	  Says A' B (Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>) \\<in> set evs4\\<rbrakk>
   10.57 -	 \\<Longrightarrow> Says B A (Crypt K (Nonce NB)) # evs4 \\<in> ns_shared"
   10.58 +  NS4:  "\<lbrakk>evs4 \<in> ns_shared;  Nonce NB \<notin> used evs4;
   10.59 +	  Says A' B (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>) \<in> set evs4\<rbrakk>
   10.60 +	 \<Longrightarrow> Says B A (Crypt K (Nonce NB)) # evs4 \<in> ns_shared"
   10.61  
   10.62  	(*Alice responds with Nonce NB if she has seen the key before.
   10.63  	  Maybe should somehow check Nonce NA again.
   10.64  	  We do NOT send NB-1 or similar as the Spy cannot spoof such things.
   10.65  	  Letting the Spy add or subtract 1 lets him send all nonces.
   10.66  	  Instead we distinguish the messages by sending the nonce twice.*)
   10.67 -  NS5:  "\\<lbrakk>evs5 \\<in> ns_shared;
   10.68 -	  Says B' A (Crypt K (Nonce NB)) \\<in> set evs5;
   10.69 -	  Says S  A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>)
   10.70 -	    \\<in> set evs5\\<rbrakk>
   10.71 -	 \\<Longrightarrow> Says A B (Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace>) # evs5 \\<in> ns_shared"
   10.72 +  NS5:  "\<lbrakk>evs5 \<in> ns_shared;
   10.73 +	  Says B' A (Crypt K (Nonce NB)) \<in> set evs5;
   10.74 +	  Says S  A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
   10.75 +	    \<in> set evs5\<rbrakk>
   10.76 +	 \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) # evs5 \<in> ns_shared"
   10.77  
   10.78  	(*This message models possible leaks of session keys.
   10.79  	  The two Nonces identify the protocol run: the rule insists upon
   10.80  	  the true senders in order to make them accurate.*)
   10.81 -  Oops: "\\<lbrakk>evso \\<in> ns_shared;  Says B A (Crypt K (Nonce NB)) \\<in> set evso;
   10.82 -	  Says Server A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>)
   10.83 -	      \\<in> set evso\\<rbrakk>
   10.84 -	 \\<Longrightarrow> Notes Spy \\<lbrace>Nonce NA, Nonce NB, Key K\\<rbrace> # evso \\<in> ns_shared"
   10.85 +  Oops: "\<lbrakk>evso \<in> ns_shared;  Says B A (Crypt K (Nonce NB)) \<in> set evso;
   10.86 +	  Says Server A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
   10.87 +	      \<in> set evso\<rbrakk>
   10.88 +	 \<Longrightarrow> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> ns_shared"
   10.89  
   10.90  
   10.91  declare Says_imp_knows_Spy [THEN parts.Inj, dest]
   10.92 @@ -79,9 +79,9 @@
   10.93  declare image_eq_UN [simp]  (*accelerates proofs involving nested images*)
   10.94  
   10.95  
   10.96 -(*A "possibility property": there are traces that reach the end*)
   10.97 -lemma "A \\<noteq> Server \\<Longrightarrow> \\<exists>N K. \\<exists>evs \\<in> ns_shared.
   10.98 -                              Says A B (Crypt K \\<lbrace>Nonce N, Nonce N\\<rbrace>) \\<in> set evs"
   10.99 +text{*A "possibility property": there are traces that reach the end*}
  10.100 +lemma "A \<noteq> Server \<Longrightarrow> \<exists>N K. \<exists>evs \<in> ns_shared.
  10.101 +                              Says A B (Crypt K \<lbrace>Nonce N, Nonce N\<rbrace>) \<in> set evs"
  10.102  apply (intro exI bexI)
  10.103  apply (rule_tac [2] ns_shared.Nil
  10.104         [THEN ns_shared.NS1, THEN ns_shared.NS2, THEN ns_shared.NS3,
  10.105 @@ -89,94 +89,94 @@
  10.106  done
  10.107  
  10.108  (*This version is similar, while instantiating ?K and ?N to epsilon-terms
  10.109 -lemma "A \\<noteq> Server \\<Longrightarrow> \\<exists>evs \\<in> ns_shared.
  10.110 -                Says A B (Crypt ?K \\<lbrace>Nonce ?N, Nonce ?N\\<rbrace>) \\<in> set evs"
  10.111 +lemma "A \<noteq> Server \<Longrightarrow> \<exists>evs \<in> ns_shared.
  10.112 +                Says A B (Crypt ?K \<lbrace>Nonce ?N, Nonce ?N\<rbrace>) \<in> set evs"
  10.113  *)
  10.114  
  10.115  
  10.116 -(**** Inductive proofs about ns_shared ****)
  10.117 +subsection{*Inductive proofs about @{term ns_shared}*}
  10.118  
  10.119 -(** Forwarding lemmas, to aid simplification **)
  10.120 +subsubsection{*Forwarding lemmas, to aid simplification*}
  10.121  
  10.122 -(*For reasoning about the encrypted portion of message NS3*)
  10.123 +text{*For reasoning about the encrypted portion of message NS3*}
  10.124  lemma NS3_msg_in_parts_spies:
  10.125 -     "Says S A (Crypt KA \\<lbrace>N, B, K, X\\<rbrace>) \\<in> set evs \\<Longrightarrow> X \\<in> parts (spies evs)"
  10.126 +     "Says S A (Crypt KA \<lbrace>N, B, K, X\<rbrace>) \<in> set evs \<Longrightarrow> X \<in> parts (spies evs)"
  10.127  by blast
  10.128  
  10.129 -(*For reasoning about the Oops message*)
  10.130 +text{*For reasoning about the Oops message*}
  10.131  lemma Oops_parts_spies:
  10.132 -     "Says Server A (Crypt (shrK A) \\<lbrace>NA, B, K, X\\<rbrace>) \\<in> set evs
  10.133 -            \\<Longrightarrow> K \\<in> parts (spies evs)"
  10.134 +     "Says Server A (Crypt (shrK A) \<lbrace>NA, B, K, X\<rbrace>) \<in> set evs
  10.135 +            \<Longrightarrow> K \<in> parts (spies evs)"
  10.136  by blast
  10.137  
  10.138 -(** Theorems of the form X \\<notin> parts (spies evs) imply that NOBODY
  10.139 -    sends messages containing X! **)
  10.140 +text{*Theorems of the form @{term "X \<notin> parts (spies evs)"} imply that NOBODY
  10.141 +    sends messages containing @{term X}*}
  10.142  
  10.143 -(*Spy never sees another agent's shared key! (unless it's bad at start)*)
  10.144 +text{*Spy never sees another agent's shared key! (unless it's bad at start)*}
  10.145  lemma Spy_see_shrK [simp]:
  10.146 -     "evs \\<in> ns_shared \\<Longrightarrow> (Key (shrK A) \\<in> parts (spies evs)) = (A \\<in> bad)"
  10.147 +     "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
  10.148  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all, blast+)
  10.149  done
  10.150  
  10.151  lemma Spy_analz_shrK [simp]:
  10.152 -     "evs \\<in> ns_shared \\<Longrightarrow> (Key (shrK A) \\<in> analz (spies evs)) = (A \\<in> bad)"
  10.153 +     "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
  10.154  by auto
  10.155  
  10.156  
  10.157 -(*Nobody can have used non-existent keys!*)
  10.158 +text{*Nobody can have used non-existent keys!*}
  10.159  lemma new_keys_not_used [rule_format, simp]:
  10.160 -    "evs \\<in> ns_shared \\<Longrightarrow> Key K \\<notin> used evs \\<longrightarrow> K \\<notin> keysFor (parts (spies evs))"
  10.161 +    "evs \<in> ns_shared \<Longrightarrow> Key K \<notin> used evs \<longrightarrow> K \<notin> keysFor (parts (spies evs))"
  10.162  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
  10.163 -(*Fake, NS2, NS4, NS5*)
  10.164 -apply (blast dest!: keysFor_parts_insert)+
  10.165 +txt{*Fake, NS2, NS4, NS5*}
  10.166 +apply (force dest!: keysFor_parts_insert, blast+)
  10.167  done
  10.168  
  10.169  
  10.170 -(** Lemmas concerning the form of items passed in messages **)
  10.171 +subsubsection{*Lemmas concerning the form of items passed in messages*}
  10.172  
  10.173 -(*Describes the form of K, X and K' when the Server sends this message.*)
  10.174 +text{*Describes the form of K, X and K' when the Server sends this message.*}
  10.175  lemma Says_Server_message_form:
  10.176 -     "\\<lbrakk>Says Server A (Crypt K' \\<lbrace>N, Agent B, Key K, X\\<rbrace>) \\<in> set evs;
  10.177 -       evs \\<in> ns_shared\\<rbrakk>
  10.178 -      \\<Longrightarrow> K \\<notin> range shrK \\<and>
  10.179 -          X = (Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>) \\<and>
  10.180 +     "\<lbrakk>Says Server A (Crypt K' \<lbrace>N, Agent B, Key K, X\<rbrace>) \<in> set evs;
  10.181 +       evs \<in> ns_shared\<rbrakk>
  10.182 +      \<Longrightarrow> K \<notin> range shrK \<and>
  10.183 +          X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>) \<and>
  10.184            K' = shrK A"
  10.185  by (erule rev_mp, erule ns_shared.induct, auto)
  10.186  
  10.187  
  10.188 -(*If the encrypted message appears then it originated with the Server*)
  10.189 +text{*If the encrypted message appears then it originated with the Server*}
  10.190  lemma A_trusts_NS2:
  10.191 -     "\\<lbrakk>Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace> \\<in> parts (spies evs);
  10.192 -       A \\<notin> bad;  evs \\<in> ns_shared\\<rbrakk>
  10.193 -      \\<Longrightarrow> Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs"
  10.194 +     "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
  10.195 +       A \<notin> bad;  evs \<in> ns_shared\<rbrakk>
  10.196 +      \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs"
  10.197  apply (erule rev_mp)
  10.198  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto)
  10.199  done
  10.200  
  10.201  lemma cert_A_form:
  10.202 -     "\\<lbrakk>Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace> \\<in> parts (spies evs);
  10.203 -       A \\<notin> bad;  evs \\<in> ns_shared\\<rbrakk>
  10.204 -      \\<Longrightarrow> K \\<notin> range shrK \\<and>  X = (Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>)"
  10.205 +     "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
  10.206 +       A \<notin> bad;  evs \<in> ns_shared\<rbrakk>
  10.207 +      \<Longrightarrow> K \<notin> range shrK \<and>  X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>)"
  10.208  by (blast dest!: A_trusts_NS2 Says_Server_message_form)
  10.209  
  10.210  (*EITHER describes the form of X when the following message is sent,
  10.211    OR     reduces it to the Fake case.
  10.212    Use Says_Server_message_form if applicable.*)
  10.213  lemma Says_S_message_form:
  10.214 -     "\\<lbrakk>Says S A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs;
  10.215 -       evs \\<in> ns_shared\\<rbrakk>
  10.216 -      \\<Longrightarrow> (K \\<notin> range shrK \\<and> X = (Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>))
  10.217 -          \\<or> X \\<in> analz (spies evs)"
  10.218 +     "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
  10.219 +       evs \<in> ns_shared\<rbrakk>
  10.220 +      \<Longrightarrow> (K \<notin> range shrK \<and> X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>))
  10.221 +          \<or> X \<in> analz (spies evs)"
  10.222  by (blast dest: Says_imp_knows_Spy cert_A_form analz.Inj)
  10.223  
  10.224  
  10.225  (*Alternative version also provable
  10.226  lemma Says_S_message_form2:
  10.227 -  "\\<lbrakk>Says S A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs;
  10.228 -    evs \\<in> ns_shared\\<rbrakk>
  10.229 -   \\<Longrightarrow> Says Server A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs
  10.230 -       \\<or> X \\<in> analz (spies evs)"
  10.231 -apply (case_tac "A \\<in> bad")
  10.232 +  "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
  10.233 +    evs \<in> ns_shared\<rbrakk>
  10.234 +   \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs
  10.235 +       \<or> X \<in> analz (spies evs)"
  10.236 +apply (case_tac "A \<in> bad")
  10.237  apply (force dest!: Says_imp_knows_Spy [THEN analz.Inj])
  10.238  by (blast dest!: A_trusts_NS2 Says_Server_message_form)
  10.239  *)
  10.240 @@ -185,35 +185,35 @@
  10.241  (****
  10.242   SESSION KEY COMPROMISE THEOREM.  To prove theorems of the form
  10.243  
  10.244 -  Key K \\<in> analz (insert (Key KAB) (spies evs)) \\<Longrightarrow>
  10.245 -  Key K \\<in> analz (spies evs)
  10.246 +  Key K \<in> analz (insert (Key KAB) (spies evs)) \<Longrightarrow>
  10.247 +  Key K \<in> analz (spies evs)
  10.248  
  10.249   A more general formula must be proved inductively.
  10.250  ****)
  10.251  
  10.252 -(*NOT useful in this form, but it says that session keys are not used
  10.253 +text{*NOT useful in this form, but it says that session keys are not used
  10.254    to encrypt messages containing other keys, in the actual protocol.
  10.255 -  We require that agents should behave like this subsequently also.*)
  10.256 -lemma  "\\<lbrakk>evs \\<in> ns_shared;  Kab \\<notin> range shrK\\<rbrakk> \\<Longrightarrow>
  10.257 -         (Crypt KAB X) \\<in> parts (spies evs) \\<and>
  10.258 -         Key K \\<in> parts {X} \\<longrightarrow> Key K \\<in> parts (spies evs)"
  10.259 +  We require that agents should behave like this subsequently also.*}
  10.260 +lemma  "\<lbrakk>evs \<in> ns_shared;  Kab \<notin> range shrK\<rbrakk> \<Longrightarrow>
  10.261 +         (Crypt KAB X) \<in> parts (spies evs) \<and>
  10.262 +         Key K \<in> parts {X} \<longrightarrow> Key K \<in> parts (spies evs)"
  10.263  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
  10.264 -(*Fake*)
  10.265 +txt{*Fake*}
  10.266  apply (blast dest: parts_insert_subset_Un)
  10.267 -(*Base, NS4 and NS5*)
  10.268 +txt{*Base, NS4 and NS5*}
  10.269  apply auto
  10.270  done
  10.271  
  10.272  
  10.273 -(** Session keys are not used to encrypt other session keys **)
  10.274 +subsubsection{*Session keys are not used to encrypt other session keys*}
  10.275  
  10.276 -(*The equality makes the induction hypothesis easier to apply*)
  10.277 +text{*The equality makes the induction hypothesis easier to apply*}
  10.278  
  10.279  lemma analz_image_freshK [rule_format]:
  10.280 - "evs \\<in> ns_shared \\<Longrightarrow>
  10.281 -   \\<forall>K KK. KK \\<subseteq> - (range shrK) \\<longrightarrow>
  10.282 -             (Key K \\<in> analz (Key`KK \\<union> (spies evs))) =
  10.283 -             (K \\<in> KK \\<or> Key K \\<in> analz (spies evs))"
  10.284 + "evs \<in> ns_shared \<Longrightarrow>
  10.285 +   \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow>
  10.286 +             (Key K \<in> analz (Key`KK \<union> (spies evs))) =
  10.287 +             (K \<in> KK \<or> Key K \<in> analz (spies evs))"
  10.288  apply (erule ns_shared.induct, force)
  10.289  apply (drule_tac [7] Says_Server_message_form)
  10.290  apply (erule_tac [4] Says_S_message_form [THEN disjE], analz_freshK, spy_analz)
  10.291 @@ -221,97 +221,100 @@
  10.292  
  10.293  
  10.294  lemma analz_insert_freshK:
  10.295 -     "\\<lbrakk>evs \\<in> ns_shared;  KAB \\<notin> range shrK\\<rbrakk> \\<Longrightarrow>
  10.296 -       (Key K \\<in> analz (insert (Key KAB) (spies evs))) =
  10.297 -       (K = KAB \\<or> Key K \\<in> analz (spies evs))"
  10.298 +     "\<lbrakk>evs \<in> ns_shared;  KAB \<notin> range shrK\<rbrakk> \<Longrightarrow>
  10.299 +       (Key K \<in> analz (insert (Key KAB) (spies evs))) =
  10.300 +       (K = KAB \<or> Key K \<in> analz (spies evs))"
  10.301  by (simp only: analz_image_freshK analz_image_freshK_simps)
  10.302  
  10.303  
  10.304 -(** The session key K uniquely identifies the message **)
  10.305 +subsubsection{*The session key K uniquely identifies the message*}
  10.306  
  10.307 -(*In messages of this form, the session key uniquely identifies the rest*)
  10.308 +text{*In messages of this form, the session key uniquely identifies the rest*}
  10.309  lemma unique_session_keys:
  10.310 -     "\\<lbrakk>Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs;
  10.311 -       Says Server A' (Crypt (shrK A') \\<lbrace>NA', Agent B', Key K, X'\\<rbrace>) \\<in> set evs;
  10.312 -       evs \\<in> ns_shared\\<rbrakk> \\<Longrightarrow> A=A' \\<and> NA=NA' \\<and> B=B' \\<and> X = X'"
  10.313 +     "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
  10.314 +       Says Server A' (Crypt (shrK A') \<lbrace>NA', Agent B', Key K, X'\<rbrace>) \<in> set evs;
  10.315 +       evs \<in> ns_shared\<rbrakk> \<Longrightarrow> A=A' \<and> NA=NA' \<and> B=B' \<and> X = X'"
  10.316  apply (erule rev_mp, erule rev_mp, erule ns_shared.induct, simp_all, blast+)
  10.317  done
  10.318  
  10.319  
  10.320 -(** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
  10.321 +subsubsection{*Crucial secrecy property: Spy does not see the keys sent in msg NS2*}
  10.322  
  10.323 -(*Beware of [rule_format] and the universal quantifier!*)
  10.324 +text{*Beware of [rule_format] and the universal quantifier!*}
  10.325  lemma secrecy_lemma:
  10.326 -     "\\<lbrakk>Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K,
  10.327 -                                      Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>\\<rbrace>)
  10.328 -              \\<in> set evs;
  10.329 -         A \\<notin> bad;  B \\<notin> bad;  evs \\<in> ns_shared\\<rbrakk>
  10.330 -      \\<Longrightarrow> (\\<forall>NB. Notes Spy \\<lbrace>NA, NB, Key K\\<rbrace> \\<notin> set evs) \\<longrightarrow>
  10.331 -         Key K \\<notin> analz (spies evs)"
  10.332 +     "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
  10.333 +                                      Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
  10.334 +              \<in> set evs;
  10.335 +         A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
  10.336 +      \<Longrightarrow> (\<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs) \<longrightarrow>
  10.337 +         Key K \<notin> analz (spies evs)"
  10.338  apply (erule rev_mp)
  10.339  apply (erule ns_shared.induct, force)
  10.340  apply (frule_tac [7] Says_Server_message_form)
  10.341  apply (frule_tac [4] Says_S_message_form)
  10.342  apply (erule_tac [5] disjE)
  10.343 -apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs, spy_analz)  (*Fake*)
  10.344 -apply blast      (*NS2*)
  10.345 -(*NS3, Server sub-case*) (**LEVEL 8 **)
  10.346 +apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs, spy_analz)  
  10.347 +txt{*NS2*}
  10.348 +apply blast
  10.349 +txt{*NS3, Server sub-case*} 
  10.350  apply (blast dest!: Crypt_Spy_analz_bad A_trusts_NS2
  10.351  	     dest:  Says_imp_knows_Spy analz.Inj unique_session_keys)
  10.352 -(*NS3, Spy sub-case; also Oops*)
  10.353 +txt{*NS3, Spy sub-case; also Oops*}
  10.354  apply (blast dest: unique_session_keys)+
  10.355  done
  10.356  
  10.357  
  10.358  
  10.359 -(*Final version: Server's message in the most abstract form*)
  10.360 +text{*Final version: Server's message in the most abstract form*}
  10.361  lemma Spy_not_see_encrypted_key:
  10.362 -     "\\<lbrakk>Says Server A (Crypt K' \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs;
  10.363 -       \\<forall>NB. Notes Spy \\<lbrace>NA, NB, Key K\\<rbrace> \\<notin> set evs;
  10.364 -       A \\<notin> bad;  B \\<notin> bad;  evs \\<in> ns_shared\\<rbrakk>
  10.365 -      \\<Longrightarrow> Key K \\<notin> analz (spies evs)"
  10.366 +     "\<lbrakk>Says Server A (Crypt K' \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
  10.367 +       \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
  10.368 +       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
  10.369 +      \<Longrightarrow> Key K \<notin> analz (spies evs)"
  10.370  by (blast dest: Says_Server_message_form secrecy_lemma)
  10.371  
  10.372  
  10.373 -(**** Guarantees available at various stages of protocol ***)
  10.374 +subsection{*Guarantees available at various stages of protocol*}
  10.375  
  10.376 -(*If the encrypted message appears then it originated with the Server*)
  10.377 +text{*If the encrypted message appears then it originated with the Server*}
  10.378  lemma B_trusts_NS3:
  10.379 -     "\\<lbrakk>Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace> \\<in> parts (spies evs);
  10.380 -       B \\<notin> bad;  evs \\<in> ns_shared\\<rbrakk>
  10.381 -      \\<Longrightarrow> \\<exists>NA. Says Server A
  10.382 -               (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K,
  10.383 -                                 Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>\\<rbrace>)
  10.384 -              \\<in> set evs"
  10.385 +     "\<lbrakk>Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
  10.386 +       B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
  10.387 +      \<Longrightarrow> \<exists>NA. Says Server A
  10.388 +               (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
  10.389 +                                 Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
  10.390 +              \<in> set evs"
  10.391  apply (erule rev_mp)
  10.392  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto)
  10.393  done
  10.394  
  10.395  
  10.396  lemma A_trusts_NS4_lemma [rule_format]:
  10.397 -   "evs \\<in> ns_shared \\<Longrightarrow>
  10.398 -      Key K \\<notin> analz (spies evs) \\<longrightarrow>
  10.399 -      Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs \\<longrightarrow>
  10.400 -      Crypt K (Nonce NB) \\<in> parts (spies evs) \\<longrightarrow>
  10.401 -      Says B A (Crypt K (Nonce NB)) \\<in> set evs"
  10.402 +   "evs \<in> ns_shared \<Longrightarrow>
  10.403 +      Key K \<notin> analz (spies evs) \<longrightarrow>
  10.404 +      Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow>
  10.405 +      Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
  10.406 +      Says B A (Crypt K (Nonce NB)) \<in> set evs"
  10.407  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
  10.408 -apply (analz_mono_contra, simp_all, blast)     (*Fake*)
  10.409 +apply (analz_mono_contra, simp_all, blast) 
  10.410  (*NS2: contradiction from the assumptions
  10.411 -  Key K \\<notin> used evs2  and Crypt K (Nonce NB) \\<in> parts (spies evs2) *)
  10.412 -apply (force dest!: Crypt_imp_keysFor, blast)     (*NS3*)
  10.413 -(*NS4*)
  10.414 +  Key K \<notin> used evs2  and Crypt K (Nonce NB) \<in> parts (spies evs2) *)
  10.415 +apply (force dest!: Crypt_imp_keysFor)     
  10.416 +txt{*NS3*}
  10.417 +apply blast 
  10.418 +txt{*NS4*}
  10.419  apply (blast dest!: B_trusts_NS3
  10.420  	     dest: Says_imp_knows_Spy [THEN analz.Inj]
  10.421                     Crypt_Spy_analz_bad unique_session_keys)
  10.422  done
  10.423  
  10.424 -(*This version no longer assumes that K is secure*)
  10.425 +text{*This version no longer assumes that K is secure*}
  10.426  lemma A_trusts_NS4:
  10.427 -     "\\<lbrakk>Crypt K (Nonce NB) \\<in> parts (spies evs);
  10.428 -       Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace> \\<in> parts (spies evs);
  10.429 -       \\<forall>NB. Notes Spy \\<lbrace>NA, NB, Key K\\<rbrace> \\<notin> set evs;
  10.430 -       A \\<notin> bad;  B \\<notin> bad;  evs \\<in> ns_shared\\<rbrakk>
  10.431 -      \\<Longrightarrow> Says B A (Crypt K (Nonce NB)) \\<in> set evs"
  10.432 +     "\<lbrakk>Crypt K (Nonce NB) \<in> parts (spies evs);
  10.433 +       Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
  10.434 +       \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
  10.435 +       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
  10.436 +      \<Longrightarrow> Says B A (Crypt K (Nonce NB)) \<in> set evs"
  10.437  by (blast intro: A_trusts_NS4_lemma
  10.438            dest: A_trusts_NS2 Spy_not_see_encrypted_key)
  10.439  
  10.440 @@ -319,16 +322,18 @@
  10.441    component X in some instance of NS4.  Perhaps an interesting property,
  10.442    but not needed (after all) for the proofs below.*)
  10.443  theorem NS4_implies_NS3 [rule_format]:
  10.444 -  "evs \\<in> ns_shared \\<Longrightarrow>
  10.445 -     Key K \\<notin> analz (spies evs) \\<longrightarrow>
  10.446 -     Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs \\<longrightarrow>
  10.447 -     Crypt K (Nonce NB) \\<in> parts (spies evs) \\<longrightarrow>
  10.448 -     (\\<exists>A'. Says A' B X \\<in> set evs)"
  10.449 +  "evs \<in> ns_shared \<Longrightarrow>
  10.450 +     Key K \<notin> analz (spies evs) \<longrightarrow>
  10.451 +     Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow>
  10.452 +     Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
  10.453 +     (\<exists>A'. Says A' B X \<in> set evs)"
  10.454  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra)
  10.455 -apply (simp_all add: ex_disj_distrib, blast)  (*Fake*)
  10.456 -apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  (*NS2*)
  10.457 -apply blast  (*NS3*)
  10.458 -(*NS4*)
  10.459 +apply (simp_all add: ex_disj_distrib, blast)
  10.460 +txt{*NS2*}
  10.461 +apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  
  10.462 +txt{*NS3*}
  10.463 +apply blast
  10.464 +txt{*NS4*}
  10.465  apply (blast dest!: B_trusts_NS3
  10.466  	     dest: Says_imp_knows_Spy [THEN analz.Inj]
  10.467                     unique_session_keys Crypt_Spy_analz_bad)
  10.468 @@ -336,30 +341,32 @@
  10.469  
  10.470  
  10.471  lemma B_trusts_NS5_lemma [rule_format]:
  10.472 -  "\\<lbrakk>B \\<notin> bad;  evs \\<in> ns_shared\\<rbrakk> \\<Longrightarrow>
  10.473 -     Key K \\<notin> analz (spies evs) \\<longrightarrow>
  10.474 +  "\<lbrakk>B \<notin> bad;  evs \<in> ns_shared\<rbrakk> \<Longrightarrow>
  10.475 +     Key K \<notin> analz (spies evs) \<longrightarrow>
  10.476       Says Server A
  10.477 -	  (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K,
  10.478 -			    Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>\\<rbrace>) \\<in> set evs \\<longrightarrow>
  10.479 -     Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace> \\<in> parts (spies evs) \\<longrightarrow>
  10.480 -     Says A B (Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace>) \\<in> set evs"
  10.481 -apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra, simp_all, blast)  (*Fake*)
  10.482 -apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  (*NS2*)
  10.483 -apply (blast dest!: cert_A_form) (*NS3*)
  10.484 -(*NS5*)
  10.485 +	  (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
  10.486 +			    Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>) \<in> set evs \<longrightarrow>
  10.487 +     Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow>
  10.488 +     Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
  10.489 +apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra, simp_all, blast)
  10.490 +txt{*NS2*}
  10.491 +apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  
  10.492 +txt{*NS3*}
  10.493 +apply (blast dest!: cert_A_form) 
  10.494 +txt{*NS5*}
  10.495  apply (blast dest!: A_trusts_NS2
  10.496  	     dest: Says_imp_knows_Spy [THEN analz.Inj]
  10.497                     unique_session_keys Crypt_Spy_analz_bad)
  10.498  done
  10.499  
  10.500  
  10.501 -(*Very strong Oops condition reveals protocol's weakness*)
  10.502 +text{*Very strong Oops condition reveals protocol's weakness*}
  10.503  lemma B_trusts_NS5:
  10.504 -     "\\<lbrakk>Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace> \\<in> parts (spies evs);
  10.505 -       Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace> \\<in> parts (spies evs);
  10.506 -       \\<forall>NA NB. Notes Spy \\<lbrace>NA, NB, Key K\\<rbrace> \\<notin> set evs;
  10.507 -       A \\<notin> bad;  B \\<notin> bad;  evs \\<in> ns_shared\\<rbrakk>
  10.508 -      \\<Longrightarrow> Says A B (Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace>) \\<in> set evs"
  10.509 +     "\<lbrakk>Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs);
  10.510 +       Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
  10.511 +       \<forall>NA NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
  10.512 +       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
  10.513 +      \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
  10.514  by (blast intro: B_trusts_NS5_lemma
  10.515            dest: B_trusts_NS3 Spy_not_see_encrypted_key)
  10.516  
    11.1 --- a/src/HOL/Auth/Public.thy	Sat Apr 26 12:38:17 2003 +0200
    11.2 +++ b/src/HOL/Auth/Public.thy	Sat Apr 26 12:38:42 2003 +0200
    11.3 @@ -55,42 +55,28 @@
    11.4      keys are private!) *)
    11.5    privateKey_neq_publicKey [iff]: "privateKey b A \<noteq> publicKey c A'"
    11.6  
    11.7 +declare privateKey_neq_publicKey [THEN not_sym, iff]
    11.8  
    11.9  
   11.10 -
   11.11 -(*** Basic properties of pubK & priK ***)
   11.12 +subsection{*Basic properties of @{term pubK} and @{term priK}*}
   11.13  
   11.14  lemma [iff]: "(publicKey b A = publicKey c A') = (b=c & A=A')"
   11.15  by (blast dest!: injective_publicKey) 
   11.16  
   11.17 -lemma [iff]:
   11.18 -    "(privateKey b A = privateKey c A') = (b=c & A=A')"
   11.19 -apply (rule iffI) 
   11.20 -apply (drule_tac f = "invKey" in arg_cong)
   11.21 -apply (auto ); 
   11.22 -done
   11.23 -
   11.24 -declare privateKey_neq_publicKey [THEN not_sym, iff]
   11.25 -
   11.26  lemma not_symKeys_pubK [iff]: "publicKey b A \<notin> symKeys"
   11.27 -apply (simp add: symKeys_def)
   11.28 -done
   11.29 +by (simp add: symKeys_def)
   11.30  
   11.31  lemma not_symKeys_priK [iff]: "privateKey b A \<notin> symKeys"
   11.32 -apply (simp add: symKeys_def)
   11.33 -done
   11.34 +by (simp add: symKeys_def)
   11.35  
   11.36  lemma symKey_neq_priEK: "K \<in> symKeys ==> K \<noteq> priEK A"
   11.37  by auto
   11.38  
   11.39  lemma symKeys_neq_imp_neq: "(K \<in> symKeys) \<noteq> (K' \<in> symKeys) ==> K \<noteq> K'"
   11.40 -apply blast
   11.41 -done
   11.42 +by blast
   11.43  
   11.44  lemma symKeys_invKey_iff [iff]: "(invKey K \<in> symKeys) = (K \<in> symKeys)"
   11.45 -apply (unfold symKeys_def)
   11.46 -apply auto
   11.47 -done
   11.48 +by (unfold symKeys_def, auto)
   11.49  
   11.50  lemma analz_symKeys_Decrypt:
   11.51       "[| Crypt K X \<in> analz H;  K \<in> symKeys;  Key K \<in> analz H |]  
   11.52 @@ -102,8 +88,7 @@
   11.53  subsection{*"Image" equations that hold for injective functions*}
   11.54  
   11.55  lemma invKey_image_eq [simp]: "(invKey x \<in> invKey`A) = (x \<in> A)"
   11.56 -apply auto
   11.57 -done
   11.58 +by auto
   11.59  
   11.60  (*holds because invKey is injective*)
   11.61  lemma publicKey_image_eq [simp]:
   11.62 @@ -111,16 +96,14 @@
   11.63  by auto
   11.64  
   11.65  lemma privateKey_notin_image_publicKey [simp]: "privateKey b x \<notin> publicKey c ` AA"
   11.66 -apply auto
   11.67 -done
   11.68 +by auto
   11.69  
   11.70  lemma privateKey_image_eq [simp]:
   11.71       "(privateKey b A \<in> invKey ` publicKey c ` AS) = (b=c & A\<in>AS)"
   11.72  by auto
   11.73  
   11.74  lemma publicKey_notin_image_privateKey [simp]: "publicKey b A \<notin> invKey ` publicKey c ` AS"
   11.75 -apply auto
   11.76 -done
   11.77 +by auto
   11.78  
   11.79  
   11.80  subsection{*Symmetric Keys*}
   11.81 @@ -140,14 +123,12 @@
   11.82  declare inj_shrK [THEN inj_eq, iff]
   11.83  
   11.84  lemma priK_neq_shrK [iff]: "shrK A \<noteq> privateKey b C"
   11.85 -apply (simp add: symKeys_neq_imp_neq)
   11.86 -done
   11.87 +by (simp add: symKeys_neq_imp_neq)
   11.88  
   11.89  declare priK_neq_shrK [THEN not_sym, simp]
   11.90  
   11.91  lemma pubK_neq_shrK [iff]: "shrK A \<noteq> publicKey b C"
   11.92 -apply (simp add: symKeys_neq_imp_neq)
   11.93 -done
   11.94 +by (simp add: symKeys_neq_imp_neq)
   11.95  
   11.96  declare pubK_neq_shrK [THEN not_sym, simp]
   11.97  
   11.98 @@ -242,29 +223,23 @@
   11.99  
  11.100  (*Agents see their own shared keys!*)
  11.101  lemma shrK_in_initState [iff]: "Key (shrK A) \<in> initState A"
  11.102 -apply (induct_tac "A")
  11.103 -apply auto
  11.104 -done
  11.105 +by (induct_tac "A", auto)
  11.106  
  11.107  lemma shrK_in_knows [iff]: "Key (shrK A) \<in> knows A evs"
  11.108  by (simp add: initState_subset_knows [THEN subsetD])
  11.109  
  11.110  lemma shrK_in_used [iff]: "Key (shrK A) \<in> used evs"
  11.111 -apply (rule initState_into_used)
  11.112 -apply blast
  11.113 -done
  11.114 +by (rule initState_into_used, blast)
  11.115  
  11.116  (** Fresh keys never clash with long-term shared keys **)
  11.117  
  11.118  (*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
  11.119    from long-term shared keys*)
  11.120  lemma Key_not_used: "Key K \<notin> used evs ==> K \<notin> range shrK"
  11.121 -apply blast
  11.122 -done
  11.123 +by blast
  11.124  
  11.125  lemma shrK_neq: "Key K \<notin> used evs ==> shrK B \<noteq> K"
  11.126 -apply blast
  11.127 -done
  11.128 +by blast
  11.129  
  11.130  
  11.131  
  11.132 @@ -272,15 +247,11 @@
  11.133  
  11.134  text{*Agents see their own private keys!*}
  11.135  lemma priK_in_initState [iff]: "Key (privateKey b A) \<in> initState A"
  11.136 -apply (induct_tac "A")
  11.137 -apply auto
  11.138 -done
  11.139 +by (induct_tac "A", auto)
  11.140  
  11.141  text{*Agents see all public keys!*}
  11.142  lemma publicKey_in_initState [iff]: "Key (publicKey b A) \<in> initState B"
  11.143 -apply (case_tac "B")
  11.144 -apply auto
  11.145 -done
  11.146 +by (case_tac "B", auto)
  11.147  
  11.148  text{*All public keys are visible*}
  11.149  lemma spies_pubK [iff]: "Key (publicKey b A) \<in> spies evs"
  11.150 @@ -318,13 +289,10 @@
  11.151  subsection{*Fresh Nonces*}
  11.152  
  11.153  lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState B)"
  11.154 -apply (induct_tac "B")
  11.155 -apply auto
  11.156 -done
  11.157 +by (induct_tac "B", auto)
  11.158  
  11.159  lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []"
  11.160 -apply (simp add: used_Nil)
  11.161 -done
  11.162 +by (simp add: used_Nil)
  11.163  
  11.164  
  11.165  subsection{*Supply fresh nonces for possibility theorems*}
  11.166 @@ -332,32 +300,27 @@
  11.167  text{*In any trace, there is an upper bound N on the greatest nonce in use*}
  11.168  lemma Nonce_supply_lemma: "EX N. ALL n. N<=n --> Nonce n \<notin> used evs"
  11.169  apply (induct_tac "evs")
  11.170 -apply (rule_tac x = "0" in exI)
  11.171 +apply (rule_tac x = 0 in exI)
  11.172  apply (simp_all (no_asm_simp) add: used_Cons split add: event.split)
  11.173  apply safe
  11.174  apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
  11.175  done
  11.176  
  11.177  lemma Nonce_supply1: "EX N. Nonce N \<notin> used evs"
  11.178 -apply (rule Nonce_supply_lemma [THEN exE])
  11.179 -apply blast
  11.180 -done
  11.181 +by (rule Nonce_supply_lemma [THEN exE], blast)
  11.182  
  11.183  lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs"
  11.184  apply (rule Nonce_supply_lemma [THEN exE])
  11.185 -apply (rule someI)
  11.186 -apply fast
  11.187 +apply (rule someI, fast)
  11.188  done
  11.189  
  11.190  subsection{*Specialized rewriting for the analz_image_... theorems*}
  11.191  
  11.192  lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} Un H"
  11.193 -apply blast
  11.194 -done
  11.195 +by blast
  11.196  
  11.197  lemma insert_Key_image: "insert (Key K) (Key`KK \<union> C) = Key ` (insert K KK) \<union> C"
  11.198 -apply blast
  11.199 -done
  11.200 +by blast
  11.201  
  11.202  ML
  11.203  {*
  11.204 @@ -388,8 +351,7 @@
  11.205  by (simp add: symKeys_def)
  11.206  
  11.207  lemma Crypt_imp_keysFor :"[|K \<in> symKeys; Crypt K X \<in> H|] ==> K \<in> keysFor H"
  11.208 -apply (drule Crypt_imp_invKey_keysFor, simp)
  11.209 -done
  11.210 +by (drule Crypt_imp_invKey_keysFor, simp)
  11.211  
  11.212  
  11.213  subsection{*Specialized Methods for Possibility Theorems*}
  11.214 @@ -419,20 +381,35 @@
  11.215  
  11.216  
  11.217  
  11.218 +lemmas analz_image_freshK_simps =
  11.219 +       simp_thms mem_simps --{*these two allow its use with @{text "only:"}*}
  11.220 +       disj_comms 
  11.221 +       image_insert [THEN sym] image_Un [THEN sym] empty_subsetI insert_subset
  11.222 +       analz_insert_eq Un_upper2 [THEN analz_mono, THEN [2] rev_subsetD]
  11.223 +       insert_Key_singleton 
  11.224 +       Key_not_used insert_Key_image Un_assoc [THEN sym]
  11.225 +
  11.226  ML
  11.227  {*
  11.228 -bind_thms ("analz_image_freshK_simps",
  11.229 -           simp_thms @ mem_simps @  (*these two allow its use with only:*)
  11.230 -           disj_comms @
  11.231 -           [image_insert RS sym, image_Un RS sym, empty_subsetI, insert_subset,
  11.232 -            analz_insert_eq, impOfSubs (Un_upper2 RS analz_mono),
  11.233 -	    insert_Key_singleton, 
  11.234 -            Key_not_used, insert_Key_image, Un_assoc RS sym]);
  11.235 -
  11.236  val analz_image_freshK_ss =
  11.237       simpset() delsimps [image_insert, image_Un]
  11.238  	       delsimps [imp_disjL]    (*reduces blow-up*)
  11.239 -	       addsimps analz_image_freshK_simps;
  11.240 +	       addsimps thms"analz_image_freshK_simps"
  11.241  *}
  11.242  
  11.243 +axioms
  11.244 +  Key_supply_ax:  "finite KK ==> \<exists>K\<in>symKeys. K \<notin> KK & Key K \<notin> used evs"
  11.245 +  --{*Unlike the corresponding property of nonces, this cannot be proved.
  11.246 +    We have infinitely many agents and there is nothing to stop their
  11.247 +    long-term keys from exhausting all the natural numbers.  The axiom
  11.248 +    assumes that their keys are dispersed so as to leave room for infinitely
  11.249 +    many fresh session keys.  We could, alternatively, restrict agents to
  11.250 +    an unspecified finite number.  We could however replace @{term"used evs"} 
  11.251 +    by @{term "used []"}.*}
  11.252 +
  11.253 +
  11.254 +lemma Key_supply1: "\<exists>K\<in>symKeys. Key K \<notin> used evs"
  11.255 +by (rule Finites.emptyI [THEN Key_supply_ax, THEN bexE], blast)
  11.256 +
  11.257 +
  11.258  end
    12.1 --- a/src/HOL/Auth/Shared.thy	Sat Apr 26 12:38:17 2003 +0200
    12.2 +++ b/src/HOL/Auth/Shared.thy	Sat Apr 26 12:38:42 2003 +0200
    12.3 @@ -8,8 +8,7 @@
    12.4  Shared, long-term keys; initial states of agents
    12.5  *)
    12.6  
    12.7 -theory Shared = Event
    12.8 -files ("Shared_lemmas.ML"):
    12.9 +theory Shared = Event:
   12.10  
   12.11  consts
   12.12    shrK    :: "agent => key"  (*symmetric keys*)
   12.13 @@ -25,16 +24,264 @@
   12.14    initState_Spy:     "initState Spy        = Key`shrK`bad"
   12.15  
   12.16  
   12.17 +subsection{*Basic properties of shrK*}
   12.18 +
   12.19 +(*Injectiveness: Agents' long-term keys are distinct.*)
   12.20 +declare inj_shrK [THEN inj_eq, iff]
   12.21 +
   12.22 +lemma invKey_K [simp]: "invKey K = K"
   12.23 +apply (insert isSym_keys)
   12.24 +apply (simp add: symKeys_def) 
   12.25 +done
   12.26 +
   12.27 +
   12.28 +lemma analz_Decrypt' [dest]:
   12.29 +     "[| Crypt K X \<in> analz H;  Key K  \<in> analz H |] ==> X \<in> analz H"
   12.30 +by auto
   12.31 +
   12.32 +text{*Now cancel the @{text dest} attribute given to
   12.33 + @{text analz.Decrypt} in its declaration.*}
   12.34 +ML
   12.35 +{*
   12.36 +Delrules [analz.Decrypt];
   12.37 +*}
   12.38 +
   12.39 +text{*Rewrites should not refer to  @{term "initState(Friend i)"} because
   12.40 +  that expression is not in normal form.*}
   12.41 +
   12.42 +lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}"
   12.43 +apply (unfold keysFor_def)
   12.44 +apply (induct_tac "C", auto)
   12.45 +done
   12.46 +
   12.47 +(*Specialized to shared-key model: no @{term invKey}*)
   12.48 +lemma keysFor_parts_insert:
   12.49 +     "[| K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) |] \
   12.50 +\     ==> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H";
   12.51 +by (force dest: Event.keysFor_parts_insert)  
   12.52 +
   12.53 +lemma Crypt_imp_keysFor: "Crypt K X \<in> H ==> K \<in> keysFor H"
   12.54 +by (drule Crypt_imp_invKey_keysFor, simp)
   12.55 +
   12.56 +
   12.57 +subsection{*Function "knows"*}
   12.58 +
   12.59 +(*Spy sees shared keys of agents!*)
   12.60 +lemma Spy_knows_Spy_bad [intro!]: "A: bad ==> Key (shrK A) \<in> knows Spy evs"
   12.61 +apply (induct_tac "evs")
   12.62 +apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
   12.63 +done
   12.64 +
   12.65 +(*For case analysis on whether or not an agent is compromised*)
   12.66 +lemma Crypt_Spy_analz_bad: "[| Crypt (shrK A) X \<in> analz (knows Spy evs);  A: bad |]  
   12.67 +      ==> X \<in> analz (knows Spy evs)"
   12.68 +apply (force dest!: analz.Decrypt)
   12.69 +done
   12.70 +
   12.71 +
   12.72 +(** Fresh keys never clash with long-term shared keys **)
   12.73 +
   12.74 +(*Agents see their own shared keys!*)
   12.75 +lemma shrK_in_initState [iff]: "Key (shrK A) \<in> initState A"
   12.76 +by (induct_tac "A", auto)
   12.77 +
   12.78 +lemma shrK_in_used [iff]: "Key (shrK A) \<in> used evs"
   12.79 +by (rule initState_into_used, blast)
   12.80 +
   12.81 +(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
   12.82 +  from long-term shared keys*)
   12.83 +lemma Key_not_used [simp]: "Key K \<notin> used evs ==> K \<notin> range shrK"
   12.84 +by blast
   12.85 +
   12.86 +lemma shrK_neq [simp]: "Key K \<notin> used evs ==> shrK B \<noteq> K"
   12.87 +by blast
   12.88 +
   12.89 +declare shrK_neq [THEN not_sym, simp]
   12.90 +
   12.91 +
   12.92 +subsection{*Fresh nonces*}
   12.93 +
   12.94 +lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState B)"
   12.95 +by (induct_tac "B", auto)
   12.96 +
   12.97 +lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []"
   12.98 +apply (simp (no_asm) add: used_Nil)
   12.99 +done
  12.100 +
  12.101 +
  12.102 +subsection{*Supply fresh nonces for possibility theorems.*}
  12.103 +
  12.104 +(*In any trace, there is an upper bound N on the greatest nonce in use.*)
  12.105 +lemma Nonce_supply_lemma: "\<exists>N. ALL n. N<=n --> Nonce n \<notin> used evs"
  12.106 +apply (induct_tac "evs")
  12.107 +apply (rule_tac x = 0 in exI)
  12.108 +apply (simp_all (no_asm_simp) add: used_Cons split add: event.split)
  12.109 +apply safe
  12.110 +apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
  12.111 +done
  12.112 +
  12.113 +lemma Nonce_supply1: "\<exists>N. Nonce N \<notin> used evs"
  12.114 +by (rule Nonce_supply_lemma [THEN exE], blast)
  12.115 +
  12.116 +lemma Nonce_supply2: "\<exists>N N'. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' & N \<noteq> N'"
  12.117 +apply (cut_tac evs = evs in Nonce_supply_lemma)
  12.118 +apply (cut_tac evs = "evs'" in Nonce_supply_lemma, clarify)
  12.119 +apply (rule_tac x = N in exI)
  12.120 +apply (rule_tac x = "Suc (N+Na) " in exI)
  12.121 +apply (simp (no_asm_simp) add: less_not_refl3 le_add1 le_add2 less_Suc_eq_le)
  12.122 +done
  12.123 +
  12.124 +lemma Nonce_supply3: "\<exists>N N' N''. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' &  
  12.125 +                    Nonce N'' \<notin> used evs'' & N \<noteq> N' & N' \<noteq> N'' & N \<noteq> N''"
  12.126 +apply (cut_tac evs = evs in Nonce_supply_lemma)
  12.127 +apply (cut_tac evs = "evs'" in Nonce_supply_lemma)
  12.128 +apply (cut_tac evs = "evs''" in Nonce_supply_lemma, clarify)
  12.129 +apply (rule_tac x = N in exI)
  12.130 +apply (rule_tac x = "Suc (N+Na) " in exI)
  12.131 +apply (rule_tac x = "Suc (Suc (N+Na+Nb))" in exI)
  12.132 +apply (simp (no_asm_simp) add: less_not_refl3 le_add1 le_add2 less_Suc_eq_le)
  12.133 +done
  12.134 +
  12.135 +lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs"
  12.136 +apply (rule Nonce_supply_lemma [THEN exE])
  12.137 +apply (rule someI, blast)
  12.138 +done
  12.139 +
  12.140 +subsection{*Supply fresh keys for possibility theorems.*}
  12.141 +
  12.142  axioms
  12.143 -  (*Unlike the corresponding property of nonces, this cannot be proved.
  12.144 +  Key_supply_ax:  "finite KK ==> \<exists>K. K \<notin> KK & Key K \<notin> used evs"
  12.145 +  --{*Unlike the corresponding property of nonces, this cannot be proved.
  12.146      We have infinitely many agents and there is nothing to stop their
  12.147      long-term keys from exhausting all the natural numbers.  The axiom
  12.148      assumes that their keys are dispersed so as to leave room for infinitely
  12.149      many fresh session keys.  We could, alternatively, restrict agents to
  12.150 -    an unspecified finite number.*)
  12.151 -  Key_supply_ax:  "finite KK ==> EX K. K ~: KK & Key K ~: used evs"
  12.152 +    an unspecified finite number.  We could however replace @{term"used evs"} 
  12.153 +    by @{term "used []"}.*}
  12.154 +
  12.155 +lemma Key_supply1: "\<exists>K. Key K \<notin> used evs"
  12.156 +by (rule Finites.emptyI [THEN Key_supply_ax, THEN exE], blast)
  12.157 +
  12.158 +lemma Key_supply2: "\<exists>K K'. Key K \<notin> used evs & Key K' \<notin> used evs' & K \<noteq> K'"
  12.159 +apply (cut_tac evs = evs in Finites.emptyI [THEN Key_supply_ax])
  12.160 +apply (erule exE)
  12.161 +apply (cut_tac evs="evs'" in Finites.emptyI [THEN Finites.insertI, THEN Key_supply_ax], auto) 
  12.162 +done
  12.163 +
  12.164 +lemma Key_supply3: "\<exists>K K' K''. Key K \<notin> used evs & Key K' \<notin> used evs' &  
  12.165 +                       Key K'' \<notin> used evs'' & K \<noteq> K' & K' \<noteq> K'' & K \<noteq> K''"
  12.166 +apply (cut_tac evs = evs in Finites.emptyI [THEN Key_supply_ax])
  12.167 +apply (erule exE)
  12.168 +(*Blast_tac requires instantiation of the keys for some reason*)
  12.169 +apply (cut_tac evs="evs'" and a1 = K in Finites.emptyI [THEN Finites.insertI, THEN Key_supply_ax])
  12.170 +apply (erule exE)
  12.171 +apply (cut_tac evs = "evs''" and a1 = Ka and a2 = K 
  12.172 +       in Finites.emptyI [THEN Finites.insertI, THEN Finites.insertI, THEN Key_supply_ax], blast)
  12.173 +done
  12.174 +
  12.175 +lemma Key_supply: "Key (@ K. Key K \<notin> used evs) \<notin> used evs"
  12.176 +apply (rule Finites.emptyI [THEN Key_supply_ax, THEN exE])
  12.177 +apply (rule someI, blast)
  12.178 +done
  12.179 +
  12.180 +subsection{*Tactics for possibility theorems*}
  12.181 +
  12.182 +ML
  12.183 +{*
  12.184 +val inj_shrK      = thm "inj_shrK";
  12.185 +val isSym_keys    = thm "isSym_keys";
  12.186 +val Key_supply_ax = thm "Key_supply_ax";
  12.187 +val Key_supply = thm "Key_supply";
  12.188 +val Nonce_supply = thm "Nonce_supply";
  12.189 +val invKey_K = thm "invKey_K";
  12.190 +val analz_Decrypt' = thm "analz_Decrypt'";
  12.191 +val keysFor_parts_initState = thm "keysFor_parts_initState";
  12.192 +val keysFor_parts_insert = thm "keysFor_parts_insert";
  12.193 +val Crypt_imp_keysFor = thm "Crypt_imp_keysFor";
  12.194 +val Spy_knows_Spy_bad = thm "Spy_knows_Spy_bad";
  12.195 +val Crypt_Spy_analz_bad = thm "Crypt_Spy_analz_bad";
  12.196 +val shrK_in_initState = thm "shrK_in_initState";
  12.197 +val shrK_in_used = thm "shrK_in_used";
  12.198 +val Key_not_used = thm "Key_not_used";
  12.199 +val shrK_neq = thm "shrK_neq";
  12.200 +val Nonce_notin_initState = thm "Nonce_notin_initState";
  12.201 +val Nonce_notin_used_empty = thm "Nonce_notin_used_empty";
  12.202 +val Nonce_supply_lemma = thm "Nonce_supply_lemma";
  12.203 +val Nonce_supply1 = thm "Nonce_supply1";
  12.204 +val Nonce_supply2 = thm "Nonce_supply2";
  12.205 +val Nonce_supply3 = thm "Nonce_supply3";
  12.206 +val Nonce_supply = thm "Nonce_supply";
  12.207 +val Key_supply1 = thm "Key_supply1";
  12.208 +val Key_supply2 = thm "Key_supply2";
  12.209 +val Key_supply3 = thm "Key_supply3";
  12.210 +val Key_supply = thm "Key_supply";
  12.211 +*}
  12.212 +
  12.213  
  12.214 -use "Shared_lemmas.ML"
  12.215 +ML
  12.216 +{*
  12.217 +(*Omitting used_Says makes the tactic much faster: it leaves expressions
  12.218 +    such as  Nonce ?N \<notin> used evs that match Nonce_supply*)
  12.219 +fun gen_possibility_tac ss state = state |>
  12.220 +   (REPEAT 
  12.221 +    (ALLGOALS (simp_tac (ss delsimps [used_Says, used_Notes, used_Gets] 
  12.222 +                         setSolver safe_solver))
  12.223 +     THEN
  12.224 +     REPEAT_FIRST (eq_assume_tac ORELSE' 
  12.225 +                   resolve_tac [refl, conjI, Nonce_supply, Key_supply])))
  12.226 +
  12.227 +(*Tactic for possibility theorems (ML script version)*)
  12.228 +fun possibility_tac state = gen_possibility_tac (simpset()) state
  12.229 +
  12.230 +(*For harder protocols (such as Recur) where we have to set up some
  12.231 +  nonces and keys initially*)
  12.232 +fun basic_possibility_tac st = st |>
  12.233 +    REPEAT 
  12.234 +    (ALLGOALS (asm_simp_tac (simpset() setSolver safe_solver))
  12.235 +     THEN
  12.236 +     REPEAT_FIRST (resolve_tac [refl, conjI]))
  12.237 +*}
  12.238 +
  12.239 +subsection{*Specialized rewriting for analz_insert_freshK*}
  12.240 +
  12.241 +lemma subset_Compl_range: "A <= - (range shrK) ==> shrK x \<notin> A"
  12.242 +by blast
  12.243 +
  12.244 +lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} \<union> H"
  12.245 +by blast
  12.246 +
  12.247 +lemma insert_Key_image: "insert (Key K) (Key`KK \<union> C) = Key ` (insert K KK) \<union> C"
  12.248 +by blast
  12.249 +
  12.250 +(** Reverse the normal simplification of "image" to build up (not break down)
  12.251 +    the set of keys.  Use analz_insert_eq with (Un_upper2 RS analz_mono) to
  12.252 +    erase occurrences of forwarded message components (X). **)
  12.253 +
  12.254 +lemmas analz_image_freshK_simps =
  12.255 +       simp_thms mem_simps --{*these two allow its use with @{text "only:"}*}
  12.256 +       disj_comms 
  12.257 +       image_insert [THEN sym] image_Un [THEN sym] empty_subsetI insert_subset
  12.258 +       analz_insert_eq Un_upper2 [THEN analz_mono, THEN [2] rev_subsetD]
  12.259 +       insert_Key_singleton subset_Compl_range
  12.260 +       Key_not_used insert_Key_image Un_assoc [THEN sym]
  12.261 +
  12.262 +(*Lemma for the trivial direction of the if-and-only-if*)
  12.263 +lemma analz_image_freshK_lemma:
  12.264 +     "(Key K \<in> analz (Key`nE \<union> H)) --> (K \<in> nE | Key K \<in> analz H)  ==>  
  12.265 +         (Key K \<in> analz (Key`nE \<union> H)) = (K \<in> nE | Key K \<in> analz H)"
  12.266 +by (blast intro: analz_mono [THEN [2] rev_subsetD])
  12.267 +
  12.268 +ML
  12.269 +{*
  12.270 +val analz_image_freshK_lemma = thm "analz_image_freshK_lemma";
  12.271 +
  12.272 +val analz_image_freshK_ss = 
  12.273 +     simpset() delsimps [image_insert, image_Un]
  12.274 +	       delsimps [imp_disjL]    (*reduces blow-up*)
  12.275 +	       addsimps thms "analz_image_freshK_simps"
  12.276 +*}
  12.277 +
  12.278 +
  12.279  
  12.280  (*Lets blast_tac perform this step without needing the simplifier*)
  12.281  lemma invKey_shrK_iff [iff]:
    13.1 --- a/src/HOL/Auth/Yahalom.thy	Sat Apr 26 12:38:17 2003 +0200
    13.2 +++ b/src/HOL/Auth/Yahalom.thy	Sat Apr 26 12:38:42 2003 +0200
    13.3 @@ -150,8 +150,10 @@
    13.4   "evs \<in> yahalom ==> Key K \<notin> used evs --> K \<notin> keysFor (parts (knows Spy evs))"
    13.5  apply (erule yahalom.induct, force, 
    13.6         frule_tac [6] YM4_parts_knows_Spy, simp_all)
    13.7 -(*Fake, YM3, YM4*)
    13.8 -apply (blast dest!: keysFor_parts_insert)+
    13.9 +txt{*Fake*}
   13.10 +apply (force dest!: keysFor_parts_insert)
   13.11 +txt{*YM3, YM4*}
   13.12 +apply blast+
   13.13  done
   13.14  
   13.15  
    14.1 --- a/src/HOL/Auth/Yahalom2.thy	Sat Apr 26 12:38:17 2003 +0200
    14.2 +++ b/src/HOL/Auth/Yahalom2.thy	Sat Apr 26 12:38:42 2003 +0200
    14.3 @@ -137,8 +137,10 @@
    14.4   "evs \<in> yahalom ==> Key K \<notin> used evs --> K \<notin> keysFor (parts (knows Spy evs))"
    14.5  apply (erule yahalom.induct, force,
    14.6         frule_tac [6] YM4_parts_knows_Spy, simp_all)
    14.7 -(*Fake, YM3, YM4*)
    14.8 -apply (blast dest!: keysFor_parts_insert)+
    14.9 +txt{*Fake*}
   14.10 +apply (force dest!: keysFor_parts_insert)
   14.11 +txt{*YM3, YM4*}
   14.12 +apply blast+
   14.13  done
   14.14  
   14.15  
   14.16 @@ -394,7 +396,7 @@
   14.17  apply (force dest!: Crypt_imp_keysFor)
   14.18  (*YM4: was Crypt K (Nonce NB) the very last message?  If so, apply unicity
   14.19    of session keys; if not, use ind. hyp.*)
   14.20 -apply (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys  )
   14.21 +apply (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys )
   14.22  done
   14.23  
   14.24  
    15.1 --- a/src/HOL/Auth/Yahalom_Bad.thy	Sat Apr 26 12:38:17 2003 +0200
    15.2 +++ b/src/HOL/Auth/Yahalom_Bad.thy	Sat Apr 26 12:38:42 2003 +0200
    15.3 @@ -128,8 +128,10 @@
    15.4   "evs \<in> yahalom ==> Key K \<notin> used evs --> K \<notin> keysFor (parts (knows Spy evs))"
    15.5  apply (erule yahalom.induct, force,
    15.6         frule_tac [6] YM4_parts_knows_Spy, simp_all)
    15.7 -(*Fake, YM3, YM4*)
    15.8 -apply (blast dest!: keysFor_parts_insert)+
    15.9 +txt{*Fake*}
   15.10 +apply (force dest!: keysFor_parts_insert)
   15.11 +txt{*YM3, YM4*}
   15.12 +apply blast+
   15.13  done
   15.14  
   15.15  
    16.1 --- a/src/HOL/IsaMakefile	Sat Apr 26 12:38:17 2003 +0200
    16.2 +++ b/src/HOL/IsaMakefile	Sat Apr 26 12:38:42 2003 +0200
    16.3 @@ -363,14 +363,13 @@
    16.4  HOL-Auth: HOL $(LOG)/HOL-Auth.gz
    16.5  
    16.6  $(LOG)/HOL-Auth.gz: $(OUT)/HOL \
    16.7 -  Auth/CertifiedEmail.thy Auth/Event_lemmas.ML Auth/Event.thy \
    16.8 -  Auth/Message_lemmas.ML Auth/Message.thy Auth/NS_Public.thy \
    16.9 -  Auth/NS_Public_Bad.thy \
   16.10 +  Auth/CertifiedEmail.thy Auth/Event.thy \
   16.11 +  Auth/Message.thy Auth/NS_Public.thy Auth/NS_Public_Bad.thy \
   16.12    Auth/NS_Shared.thy Auth/OtwayRees.thy Auth/OtwayRees_AN.thy \
   16.13    Auth/OtwayRees_Bad.thy Auth/Public.thy Auth/ROOT.ML \
   16.14 -  Auth/Recur.thy Auth/Shared_lemmas.ML Auth/Shared.thy \
   16.15 +  Auth/Recur.thy Auth/Shared.thy \
   16.16    Auth/TLS.thy Auth/WooLam.thy \
   16.17 -  Auth/Kerberos_BAN.ML Auth/Kerberos_BAN.thy \
   16.18 +  Auth/Kerberos_BAN.thy \
   16.19    Auth/KerberosIV.ML Auth/KerberosIV.thy \
   16.20    Auth/Yahalom.thy Auth/Yahalom2.thy Auth/Yahalom_Bad.thy \
   16.21    Auth/Guard/Analz.thy Auth/Guard/Extensions.thy Auth/Guard/GuardK.thy \