--- a/src/HOL/Auth/CertifiedEmail.thy Sat Apr 26 12:38:17 2003 +0200
+++ b/src/HOL/Auth/CertifiedEmail.thy Sat Apr 26 12:38:42 2003 +0200
@@ -16,8 +16,8 @@
TTPVerKey :: key
translations
- "TTP" == "Server"
- "RPwd" == "shrK"
+ "TTP" == "Server "
+ "RPwd" == "shrK "
"TTPDecKey" == "priEK Server"
"TTPEncKey" == "pubEK Server"
"TTPSigKey" == "priSK Server"
@@ -89,6 +89,7 @@
TTP \<noteq> R'; hs' = hr'; k' \<in> symKeys|]
==>
Notes R' {|Agent TTP, Agent R', Key k', hr'|} #
+ Gets S (Crypt TTPSigKey S2TTP'') #
Says TTP S (Crypt TTPSigKey S2TTP'') # evs3 \<in> certified_mail"
Reception:
@@ -96,20 +97,6 @@
==> Gets B X#evsr \<in> certified_mail"
-axioms
- (*Unlike the corresponding property of nonces, this cannot be proved.
- We have infinitely many agents and there is nothing to stop their
- long-term keys from exhausting all the natural numbers. The axiom
- assumes that their keys are dispersed so as to leave room for infinitely
- many fresh session keys. We could, alternatively, restrict agents to
- an unspecified finite number. TOO STRONG. REPLACE "used evs" BY
- used []*)
- Key_supply_ax: "finite KK ==> \<exists>K\<in>symKeys. K \<notin> KK & Key K \<notin> used evs"
-
-
-lemma Key_supply1: "\<exists>K\<in>symKeys. Key K \<notin> used evs"
-by (rule Finites.emptyI [THEN Key_supply_ax, THEN bexE], blast)
-
(*A "possibility property": there are traces that reach the end*)
lemma "\<exists>S2TTP. \<exists>evs \<in> certified_mail.
Says TTP S (Crypt TTPSigKey S2TTP) \<in> set evs"
@@ -374,7 +361,7 @@
text{*Less easy to prove @{term "m'=m"}. Maybe needs a separate unicity
-theorem fror ciphertexts of the form @{term "Crypt K (Number m)"},
+theorem for ciphertexts of the form @{term "Crypt K (Number m)"},
where @{term K} is secure.*}
lemma Key_unique_lemma [rule_format]:
"evs \<in> certified_mail ==>
@@ -399,7 +386,7 @@
done
text{*The key determines the sender, recipient and protocol options.*}
-theorem Key_unique:
+lemma Key_unique:
"[|Says S R
{|Agent S, Agent TTP, Crypt K (Number m), Number AO,
Number cleartext, Nonce q,
@@ -415,9 +402,11 @@
==> R' = R & S' = S & AO' = AO & hs' = hs"
by (rule Key_unique_lemma, assumption+)
+subsection{*The Guarantees for Sender and Recipient*}
+
text{*If Spy gets the key then @{term R} is bad and also @{term S} at least
gets his return receipt (and therefore has no grounds for complaint).*}
-lemma Spy_see_encrypted_key_imp:
+theorem Spy_see_encrypted_key_imp:
"[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
Number cleartext, Nonce q, S2TTP|} \<in> set evs;
Key K \<in> analz(knows Spy evs);
@@ -455,8 +444,6 @@
by (blast dest: Spy_see_encrypted_key_imp)
-subsection{*The Guarantees for Sender and Recipient*}
-
text{*Agent @{term R}, who may be the Spy, doesn't receive the key
until @{term S} has access to the return receipt.*}
theorem S_guarantee:
--- a/src/HOL/Auth/Event.thy Sat Apr 26 12:38:17 2003 +0200
+++ b/src/HOL/Auth/Event.thy Sat Apr 26 12:38:42 2003 +0200
@@ -11,8 +11,7 @@
stores are visible to him
*)
-theory Event = Message
-files ("Event_lemmas.ML"):
+theory Event = Message:
consts (*Initial states of agents -- parameter of the construction*)
initState :: "agent => msg set"
@@ -74,43 +73,234 @@
used_Nil: "used [] = (UN B. parts (initState B))"
used_Cons: "used (ev # evs) =
(case ev of
- Says A B X => parts {X} Un (used evs)
+ Says A B X => parts {X} \<union> (used evs)
| Gets A X => used evs
- | Notes A X => parts {X} Un (used evs))"
+ | Notes A X => parts {X} \<union> (used evs))"
-lemma Notes_imp_used [rule_format]: "Notes A X : set evs --> X : used evs"
-apply (induct_tac evs);
+lemma Notes_imp_used [rule_format]: "Notes A X \<in> set evs --> X \<in> used evs"
+apply (induct_tac evs)
apply (auto split: event.split)
done
-lemma Says_imp_used [rule_format]: "Says A B X : set evs --> X : used evs"
-apply (induct_tac evs);
+lemma Says_imp_used [rule_format]: "Says A B X \<in> set evs --> X \<in> used evs"
+apply (induct_tac evs)
apply (auto split: event.split)
done
lemma MPair_used [rule_format]:
- "MPair X Y : used evs --> X : used evs & Y : used evs"
-apply (induct_tac evs);
+ "MPair X Y \<in> used evs --> X \<in> used evs & Y \<in> used evs"
+apply (induct_tac evs)
apply (auto split: event.split)
done
-use "Event_lemmas.ML"
+
+subsection{*Function @{term knows}*}
+
+text{*Simplifying @term{"parts (insert X (knows Spy evs))
+ = parts {X} \<union> parts (knows Spy evs)"}. The general case loops.*)
+
+text{*This version won't loop with the simplifier.*}
+lemmas parts_insert_knows_Spy = parts_insert [of _ "knows Spy evs", standard]
+
+lemma knows_Spy_Says [simp]:
+ "knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
+by simp
+
+text{*The point of letting the Spy see "bad" agents' notes is to prevent
+ redundant case-splits on whether A=Spy and whether A:bad*}
+lemma knows_Spy_Notes [simp]:
+ "knows Spy (Notes A X # evs) =
+ (if A:bad then insert X (knows Spy evs) else knows Spy evs)"
+by simp
+
+lemma knows_Spy_Gets [simp]: "knows Spy (Gets A X # evs) = knows Spy evs"
+by simp
+
+lemma knows_Spy_subset_knows_Spy_Says:
+ "knows Spy evs <= knows Spy (Says A B X # evs)"
+by (simp add: subset_insertI)
+
+lemma knows_Spy_subset_knows_Spy_Notes:
+ "knows Spy evs <= knows Spy (Notes A X # evs)"
+by force
+
+lemma knows_Spy_subset_knows_Spy_Gets:
+ "knows Spy evs <= knows Spy (Gets A X # evs)"
+by (simp add: subset_insertI)
+
+text{*Spy sees what is sent on the traffic*}
+lemma Says_imp_knows_Spy [rule_format]:
+ "Says A B X \<in> set evs --> X \<in> knows Spy evs"
+apply (induct_tac "evs")
+apply (simp_all (no_asm_simp) split add: event.split)
+done
+
+lemma Notes_imp_knows_Spy [rule_format]:
+ "Notes A X \<in> set evs --> A: bad --> X \<in> knows Spy evs"
+apply (induct_tac "evs")
+apply (simp_all (no_asm_simp) split add: event.split)
+done
+
+
+text{*Elimination rules: derive contradictions from old Says events containing
+ items known to be fresh*}
+lemmas knows_Spy_partsEs =
+ Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard]
+ parts.Body [THEN revcut_rl, standard]
+
+text{*Compatibility for the old "spies" function*}
+lemmas spies_partsEs = knows_Spy_partsEs
+lemmas Says_imp_spies = Says_imp_knows_Spy
+lemmas parts_insert_spies = parts_insert_knows_Spy
+
+
+subsection{*Knowledge of Agents*}
+
+lemma knows_Says: "knows A (Says A B X # evs) = insert X (knows A evs)"
+by simp
+
+lemma knows_Notes: "knows A (Notes A X # evs) = insert X (knows A evs)"
+by simp
+
+lemma knows_Gets:
+ "A \<noteq> Spy --> knows A (Gets A X # evs) = insert X (knows A evs)"
+by simp
+
+
+lemma knows_subset_knows_Says: "knows A evs <= knows A (Says A' B X # evs)"
+apply (simp add: subset_insertI)
+done
+
+lemma knows_subset_knows_Notes: "knows A evs <= knows A (Notes A' X # evs)"
+apply (simp add: subset_insertI)
+done
+
+lemma knows_subset_knows_Gets: "knows A evs <= knows A (Gets A' X # evs)"
+apply (simp add: subset_insertI)
+done
+
+text{*Agents know what they say*}
+lemma Says_imp_knows [rule_format]: "Says A B X \<in> set evs --> X \<in> knows A evs"
+apply (induct_tac "evs")
+apply (simp_all (no_asm_simp) split add: event.split)
+apply blast
+done
+
+text{*Agents know what they note*}
+lemma Notes_imp_knows [rule_format]: "Notes A X \<in> set evs --> X \<in> knows A evs"
+apply (induct_tac "evs")
+apply (simp_all (no_asm_simp) split add: event.split)
+apply blast
+done
+
+text{*Agents know what they receive*}
+lemma Gets_imp_knows_agents [rule_format]:
+ "A \<noteq> Spy --> Gets A X \<in> set evs --> X \<in> knows A evs"
+apply (induct_tac "evs")
+apply (simp_all (no_asm_simp) split add: event.split)
+done
+
+
+text{*What agents DIFFERENT FROM Spy know
+ was either said, or noted, or got, or known initially*}
+lemma knows_imp_Says_Gets_Notes_initState [rule_format]:
+ "[| X \<in> knows A evs; A \<noteq> Spy |] ==> EX B.
+ Says A B X \<in> set evs | Gets A X \<in> set evs | Notes A X \<in> set evs | X \<in> initState A"
+apply (erule rev_mp)
+apply (induct_tac "evs")
+apply (simp_all (no_asm_simp) split add: event.split)
+apply blast
+done
+
+text{*What the Spy knows -- for the time being --
+ was either said or noted, or known initially*}
+lemma knows_Spy_imp_Says_Notes_initState [rule_format]:
+ "[| X \<in> knows Spy evs |] ==> EX A B.
+ Says A B X \<in> set evs | Notes A X \<in> set evs | X \<in> initState Spy"
+apply (erule rev_mp)
+apply (induct_tac "evs")
+apply (simp_all (no_asm_simp) split add: event.split)
+apply blast
+done
+
+
+
+
+text{*NOTE REMOVAL--laws above are cleaner, as they don't involve "case"*}
+declare knows_Cons [simp del]
+
+
+subsection{*Fresh Nonces*}
+
+lemma parts_knows_Spy_subset_used: "parts (knows Spy evs) <= used evs"
+apply (induct_tac "evs")
+apply (simp_all (no_asm_simp) add: parts_insert_knows_Spy split add: event.split)
+apply blast+
+done
+
+lemmas usedI = parts_knows_Spy_subset_used [THEN subsetD, intro]
+
+lemma initState_into_used: "X \<in> parts (initState B) ==> X \<in> used evs"
+apply (induct_tac "evs")
+apply (simp_all (no_asm_simp) add: parts_insert_knows_Spy split add: event.split)
+apply blast
+done
+
+lemma used_Says [simp]: "used (Says A B X # evs) = parts{X} \<union> used evs"
+by simp
+
+lemma used_Notes [simp]: "used (Notes A X # evs) = parts{X} \<union> used evs"
+by simp
+
+lemma used_Gets [simp]: "used (Gets A X # evs) = used evs"
+by simp
+
+lemma used_nil_subset: "used [] <= used evs"
+apply (simp)
+apply (blast intro: initState_into_used)
+done
+
+text{*NOTE REMOVAL--laws above are cleaner, as they don't involve "case"*}
+declare used_Nil [simp del] used_Cons [simp del]
+
+
+text{*For proving theorems of the form @{term "X \<notin> analz (knows Spy evs) --> P"}
+ New events added by induction to "evs" are discarded. Provided
+ this information isn't needed, the proof will be much shorter, since
+ it will omit complicated reasoning about @{term analz}.*}
+
+lemmas analz_mono_contra =
+ knows_Spy_subset_knows_Spy_Says [THEN analz_mono, THEN contra_subsetD]
+ knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD]
+ knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD]
+
+ML
+{*
+val analz_mono_contra_tac =
+ let val analz_impI = inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
+ in
+ rtac analz_impI THEN'
+ REPEAT1 o
+ (dresolve_tac (thms"analz_mono_contra"))
+ THEN' mp_tac
+ end
+*}
+
lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
by (induct e, auto simp: knows_Cons)
lemma initState_subset_knows: "initState A <= knows A evs"
-apply (induct_tac evs)
-apply (simp add: );
+apply (induct_tac evs, simp)
apply (blast intro: knows_subset_knows_Cons [THEN subsetD])
done
-(*For proving new_keys_not_used*)
+text{*For proving @{text new_keys_not_used}*}
lemma keysFor_parts_insert:
- "[| K \<in> keysFor (parts (insert X G)); X \<in> synth (analz H) |] \
-\ ==> K \<in> keysFor (parts (G Un H)) | Key (invKey K) \<in> parts H";
+ "[| K \<in> keysFor (parts (insert X G)); X \<in> synth (analz H) |]
+ ==> K \<in> keysFor (parts (G \<union> H)) | Key (invKey K) \<in> parts H";
by (force
dest!: parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD]
analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD]
@@ -125,10 +315,54 @@
ML
{*
+val knows_Cons = thm "knows_Cons"
+val used_Nil = thm "used_Nil"
+val used_Cons = thm "used_Cons"
+
+val Notes_imp_used = thm "Notes_imp_used";
+val Says_imp_used = thm "Says_imp_used";
+val MPair_used = thm "MPair_used";
+val parts_insert_knows_Spy = thm "parts_insert_knows_Spy";
+val knows_Spy_Says = thm "knows_Spy_Says";
+val knows_Spy_Notes = thm "knows_Spy_Notes";
+val knows_Spy_Gets = thm "knows_Spy_Gets";
+val knows_Spy_subset_knows_Spy_Says = thm "knows_Spy_subset_knows_Spy_Says";
+val knows_Spy_subset_knows_Spy_Notes = thm "knows_Spy_subset_knows_Spy_Notes";
+val knows_Spy_subset_knows_Spy_Gets = thm "knows_Spy_subset_knows_Spy_Gets";
+val Says_imp_knows_Spy = thm "Says_imp_knows_Spy";
+val Notes_imp_knows_Spy = thm "Notes_imp_knows_Spy";
+val knows_Spy_partsEs = thms "knows_Spy_partsEs";
+val spies_partsEs = thms "spies_partsEs";
+val Says_imp_spies = thm "Says_imp_spies";
+val parts_insert_spies = thm "parts_insert_spies";
+val knows_Says = thm "knows_Says";
+val knows_Notes = thm "knows_Notes";
+val knows_Gets = thm "knows_Gets";
+val knows_subset_knows_Says = thm "knows_subset_knows_Says";
+val knows_subset_knows_Notes = thm "knows_subset_knows_Notes";
+val knows_subset_knows_Gets = thm "knows_subset_knows_Gets";
+val Says_imp_knows = thm "Says_imp_knows";
+val Notes_imp_knows = thm "Notes_imp_knows";
+val Gets_imp_knows_agents = thm "Gets_imp_knows_agents";
+val knows_imp_Says_Gets_Notes_initState = thm "knows_imp_Says_Gets_Notes_initState";
+val knows_Spy_imp_Says_Notes_initState = thm "knows_Spy_imp_Says_Notes_initState";
+val parts_knows_Spy_subset_used = thm "parts_knows_Spy_subset_used";
+val usedI = thm "usedI";
+val initState_into_used = thm "initState_into_used";
+val used_Says = thm "used_Says";
+val used_Notes = thm "used_Notes";
+val used_Gets = thm "used_Gets";
+val used_nil_subset = thm "used_nil_subset";
+val analz_mono_contra = thms "analz_mono_contra";
+val knows_subset_knows_Cons = thm "knows_subset_knows_Cons";
+val initState_subset_knows = thm "initState_subset_knows";
+val keysFor_parts_insert = thm "keysFor_parts_insert";
+
+
val synth_analz_mono = thm "synth_analz_mono";
val synth_analz_mono_contra_tac =
- let val syan_impI = inst "P" "?Y ~: synth (analz (knows Spy ?evs))" impI
+ let val syan_impI = inst "P" "?Y \<notin> synth (analz (knows Spy ?evs))" impI
in
rtac syan_impI THEN'
REPEAT1 o
--- a/src/HOL/Auth/Event_lemmas.ML Sat Apr 26 12:38:17 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,232 +0,0 @@
-(* Title: HOL/Auth/Event_lemmas
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-*)
-
-
-val knows_Cons = thm "knows_Cons";
-val used_Nil = thm "used_Nil";
-val used_Cons = thm "used_Cons";
-
-
-(*Inserted by default but later removed. This declaration lets the file
- be re-loaded.*)
-Addsimps [knows_Cons, used_Nil, used_Cons];
-
-(**** Function "knows" ****)
-
-(** Simplifying parts (insert X (knows Spy evs))
- = parts {X} Un parts (knows Spy evs) -- since general case loops*)
-
-bind_thm ("parts_insert_knows_Spy",
- inst "H" "knows Spy evs" parts_insert);
-
-
-val expand_event_case = thm "event.split";
-
-Goal "knows Spy (Says A B X # evs) = insert X (knows Spy evs)";
-by (Simp_tac 1);
-qed "knows_Spy_Says";
-
-(*The point of letting the Spy see "bad" agents' notes is to prevent
- redundant case-splits on whether A=Spy and whether A:bad*)
-Goal "knows Spy (Notes A X # evs) = \
-\ (if A:bad then insert X (knows Spy evs) else knows Spy evs)";
-by (Simp_tac 1);
-qed "knows_Spy_Notes";
-
-Goal "knows Spy (Gets A X # evs) = knows Spy evs";
-by (Simp_tac 1);
-qed "knows_Spy_Gets";
-
-Goal "knows Spy evs <= knows Spy (Says A B X # evs)";
-by (simp_tac (simpset() addsimps [subset_insertI]) 1);
-qed "knows_Spy_subset_knows_Spy_Says";
-
-Goal "knows Spy evs <= knows Spy (Notes A X # evs)";
-by (Simp_tac 1);
-by (Fast_tac 1);
-qed "knows_Spy_subset_knows_Spy_Notes";
-
-Goal "knows Spy evs <= knows Spy (Gets A X # evs)";
-by (simp_tac (simpset() addsimps [subset_insertI]) 1);
-qed "knows_Spy_subset_knows_Spy_Gets";
-
-(*Spy sees what is sent on the traffic*)
-Goal "Says A B X : set evs --> X : knows Spy evs";
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
-qed_spec_mp "Says_imp_knows_Spy";
-
-Goal "Notes A X : set evs --> A: bad --> X : knows Spy evs";
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
-qed_spec_mp "Notes_imp_knows_Spy";
-
-
-(*Use with addSEs to derive contradictions from old Says events containing
- items known to be fresh*)
-bind_thms ("knows_Spy_partsEs",
- map make_elim [Says_imp_knows_Spy RS parts.Inj, parts.Body]);
-
-Addsimps [knows_Spy_Says, knows_Spy_Notes, knows_Spy_Gets];
-
-
-(*Begin lemmas about agents' knowledge*)
-
-Goal "knows A (Says A B X # evs) = insert X (knows A evs)";
-by (Simp_tac 1);
-qed "knows_Says";
-
-Goal "knows A (Notes A X # evs) = insert X (knows A evs)";
-by (Simp_tac 1);
-qed "knows_Notes";
-
-Goal "A ~= Spy --> knows A (Gets A X # evs) = insert X (knows A evs)";
-by (Simp_tac 1);
-qed "knows_Gets";
-
-
-Goal "knows A evs <= knows A (Says A' B X # evs)";
-by (simp_tac (simpset() addsimps [subset_insertI]) 1);
-qed "knows_subset_knows_Says";
-
-Goal "knows A evs <= knows A (Notes A' X # evs)";
-by (simp_tac (simpset() addsimps [subset_insertI]) 1);
-qed "knows_subset_knows_Notes";
-
-Goal "knows A evs <= knows A (Gets A' X # evs)";
-by (simp_tac (simpset() addsimps [subset_insertI]) 1);
-qed "knows_subset_knows_Gets";
-
-(*Agents know what they say*)
-Goal "Says A B X : set evs --> X : knows A evs";
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
-by (Blast_tac 1);
-qed_spec_mp "Says_imp_knows";
-
-(*Agents know what they note*)
-Goal "Notes A X : set evs --> X : knows A evs";
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
-by (Blast_tac 1);
-qed_spec_mp "Notes_imp_knows";
-
-(*Agents know what they receive*)
-Goal "A ~= Spy --> Gets A X : set evs --> X : knows A evs";
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
-qed_spec_mp "Gets_imp_knows_agents";
-
-
-(*What agents DIFFERENT FROM Spy know
- was either said, or noted, or got, or known initially*)
-Goal "[| X : knows A evs; A ~= Spy |] ==> EX B. \
-\ Says A B X : set evs | Gets A X : set evs | Notes A X : set evs | X : initState A";
-by (etac rev_mp 1);
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
-by (Blast_tac 1);
-qed_spec_mp "knows_imp_Says_Gets_Notes_initState";
-
-(*What the Spy knows -- for the time being --
- was either said or noted, or known initially*)
-Goal "[| X : knows Spy evs |] ==> EX A B. \
-\ Says A B X : set evs | Notes A X : set evs | X : initState Spy";
-by (etac rev_mp 1);
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
-by (Blast_tac 1);
-qed_spec_mp "knows_Spy_imp_Says_Notes_initState";
-
-(*END lemmas about agents' knowledge*)
-
-
-
-(**** NOTE REMOVAL--laws above are cleaner, as they don't involve "case" ****)
-Delsimps [knows_Cons];
-
-
-(*** Fresh nonces ***)
-
-Goal "parts (knows Spy evs) <= used evs";
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac
- (simpset() addsimps [parts_insert_knows_Spy]
- addsplits [expand_event_case])));
-by (ALLGOALS Blast_tac);
-qed "parts_knows_Spy_subset_used";
-
-bind_thm ("usedI", impOfSubs parts_knows_Spy_subset_used);
-AddIs [usedI];
-
-Goal "parts (initState B) <= used evs";
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac
- (simpset() addsimps [parts_insert_knows_Spy]
- addsplits [expand_event_case])));
-by (ALLGOALS Blast_tac);
-bind_thm ("initState_into_used", impOfSubs (result()));
-
-Goal "used (Says A B X # evs) = parts{X} Un used evs";
-by (Simp_tac 1);
-qed "used_Says";
-Addsimps [used_Says];
-
-Goal "used (Notes A X # evs) = parts{X} Un used evs";
-by (Simp_tac 1);
-qed "used_Notes";
-Addsimps [used_Notes];
-
-Goal "used (Gets A X # evs) = used evs";
-by (Simp_tac 1);
-qed "used_Gets";
-Addsimps [used_Gets];
-
-Goal "used [] <= used evs";
-by (Simp_tac 1);
-by (blast_tac (claset() addIs [initState_into_used]) 1);
-qed "used_nil_subset";
-
-(**** NOTE REMOVAL--laws above are cleaner, as they don't involve "case" ****)
-Delsimps [used_Nil, used_Cons];
-
-
-(*For proving theorems of the form X ~: analz (knows Spy evs) --> P
- New events added by induction to "evs" are discarded. Provided
- this information isn't needed, the proof will be much shorter, since
- it will omit complicated reasoning about analz.*)
-
-bind_thms ("analz_mono_contra",
- [knows_Spy_subset_knows_Spy_Says RS analz_mono RS contra_subsetD,
- knows_Spy_subset_knows_Spy_Notes RS analz_mono RS contra_subsetD,
- knows_Spy_subset_knows_Spy_Gets RS analz_mono RS contra_subsetD]);
-
-val analz_mono_contra_tac =
- let val analz_impI = inst "P" "?Y ~: analz (knows Spy ?evs)" impI
- in
- rtac analz_impI THEN'
- REPEAT1 o
- (dresolve_tac
- [knows_Spy_subset_knows_Spy_Says RS analz_mono RS contra_subsetD,
- knows_Spy_subset_knows_Spy_Notes RS analz_mono RS contra_subsetD,
- knows_Spy_subset_knows_Spy_Gets RS analz_mono RS contra_subsetD])
- THEN'
- mp_tac
- end;
-
-fun Reception_tac i =
- blast_tac (claset() addDs [Says_imp_knows_Spy RS parts.Inj,
- impOfSubs (parts_insert RS equalityD1),
- parts_trans,
- Says_imp_knows_Spy RS analz.Inj,
- impOfSubs analz_mono, analz_cut]
- addIs [less_SucI]) i;
-
-
-(*Compatibility for the old "spies" function*)
-bind_thms ("spies_partsEs", knows_Spy_partsEs);
-bind_thm ("Says_imp_spies", Says_imp_knows_Spy);
-bind_thm ("parts_insert_spies", parts_insert_knows_Spy);
--- a/src/HOL/Auth/KerberosIV.ML Sat Apr 26 12:38:17 2003 +0200
+++ b/src/HOL/Auth/KerberosIV.ML Sat Apr 26 12:38:42 2003 +0200
@@ -177,7 +177,7 @@
\ Key K \\<notin> used evs --> K \\<notin> keysFor (parts (spies evs))";
by (parts_induct_tac 1);
(*Fake*)
-by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
+by (force_tac (claset() addSDs [keysFor_parts_insert], simpset()) 1);
(*Others*)
by (ALLGOALS Blast_tac);
qed_spec_mp "new_keys_not_used";
--- a/src/HOL/Auth/Kerberos_BAN.ML Sat Apr 26 12:38:17 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,359 +0,0 @@
-(* Title: HOL/Auth/Kerberos_BAN
- ID: $Id$
- Author: Giampaolo Bella, Cambridge University Computer Laboratory
- Copyright 1998 University of Cambridge
-
-The Kerberos protocol, BAN version.
-
-From page 251 of
- Burrows, Abadi and Needham. A Logic of Authentication.
- Proc. Royal Soc. 426 (1989)
-
- Confidentiality (secrecy) and authentication properties rely on
- temporal checks: strong guarantees in a little abstracted - but
- very realistic - model (see .thy).
-
-Tidied by lcp.
-*)
-
-AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body];
-AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert];
-
-AddIffs [SesKeyLife_LB, AutLife_LB];
-
-
-(*A "possibility property": there are traces that reach the end.*)
-Goal "\\<exists>Timestamp K. \\<exists>evs \\<in> kerberos_ban. \
-\ Says B A (Crypt K (Number Timestamp)) \
-\ \\<in> set evs";
-by (cut_facts_tac [SesKeyLife_LB] 1);
-by (REPEAT (resolve_tac [exI,bexI] 1));
-by (rtac (kerberos_ban.Nil RS kerberos_ban.Kb1 RS kerberos_ban.Kb2 RS
- kerberos_ban.Kb3 RS kerberos_ban.Kb4) 2);
-by possibility_tac;
-by (ALLGOALS Asm_simp_tac);
-result();
-
-
-
-(**** Inductive proofs about kerberos_ban ****)
-
-(*Forwarding Lemma for reasoning about the encrypted portion of message Kb3*)
-Goal "Says S A (Crypt KA {|Timestamp, B, K, X|}) \\<in> set evs \
-\ ==> X \\<in> parts (spies evs)";
-by (Blast_tac 1);
-qed "Kb3_msg_in_parts_spies";
-
-Goal "Says Server A (Crypt (shrK A) {|Timestamp, B, K, X|}) \\<in> set evs \
-\ ==> K \\<in> parts (spies evs)";
-by (Blast_tac 1);
-qed "Oops_parts_spies";
-
-(*For proving the easier theorems about X \\<notin> parts (spies evs).*)
-fun parts_induct_tac i =
- etac kerberos_ban.induct i THEN
- ftac Oops_parts_spies (i+6) THEN
- ftac Kb3_msg_in_parts_spies (i+4) THEN
- prove_simple_subgoals_tac i;
-
-
-(*Spy never sees another agent's shared key! (unless it's bad at start)*)
-Goal "evs \\<in> kerberos_ban ==> (Key (shrK A) \\<in> parts (spies evs)) = (A \\<in> bad)";
-by (parts_induct_tac 1);
-by (ALLGOALS Blast_tac);
-qed "Spy_see_shrK";
-Addsimps [Spy_see_shrK];
-
-
-Goal "evs \\<in> kerberos_ban ==> (Key (shrK A) \\<in> analz (spies evs)) = (A \\<in> bad)";
-by Auto_tac;
-qed "Spy_analz_shrK";
-Addsimps [Spy_analz_shrK];
-
-Goal "[| Key (shrK A) \\<in> parts (spies evs); \
-\ evs \\<in> kerberos_ban |] ==> A:bad";
-by (blast_tac (claset() addDs [Spy_see_shrK]) 1);
-qed "Spy_see_shrK_D";
-
-bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
-AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
-
-
-(*Nobody can have used non-existent keys!*)
-Goal "evs \\<in> kerberos_ban ==> \
-\ Key K \\<notin> used evs --> K \\<notin> keysFor (parts (spies evs))";
-by (parts_induct_tac 1);
-(*Fake*)
-by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
-(*Kb2, Kb3, Kb4*)
-by (ALLGOALS Blast_tac);
-qed_spec_mp "new_keys_not_used";
-Addsimps [new_keys_not_used];
-
-(** Lemmas concerning the form of items passed in messages **)
-
-(*Describes the form of K, X and K' when the Server sends this message.*)
-Goal "[| Says Server A (Crypt K' {|Number Ts, Agent B, Key K, X|}) \
-\ \\<in> set evs; evs \\<in> kerberos_ban |] \
-\ ==> K \\<notin> range shrK & \
-\ X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}) & \
-\ K' = shrK A";
-by (etac rev_mp 1);
-by (etac kerberos_ban.induct 1);
-by Auto_tac;
-qed "Says_Server_message_form";
-
-
-(*If the encrypted message appears then it originated with the Server
- PROVIDED that A is NOT compromised!
-
- This shows implicitly the FRESHNESS OF THE SESSION KEY to A
-*)
-Goal "[| Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} \
-\ \\<in> parts (spies evs); \
-\ A \\<notin> bad; evs \\<in> kerberos_ban |] \
-\ ==> Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \
-\ \\<in> set evs";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (Blast_tac 1);
-qed "A_trusts_K_by_Kb2";
-
-
-(*If the TICKET appears then it originated with the Server*)
-(*FRESHNESS OF THE SESSION KEY to B*)
-Goal "[| Crypt (shrK B) {|Number Ts, Agent A, Key K|} \\<in> parts (spies evs); \
-\ B \\<notin> bad; evs \\<in> kerberos_ban |] \
-\ ==> Says Server A \
-\ (Crypt (shrK A) {|Number Ts, Agent B, Key K, \
-\ Crypt (shrK B) {|Number Ts, Agent A, Key K|}|}) \
-\ \\<in> set evs";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (Blast_tac 1);
-qed "B_trusts_K_by_Kb3";
-
-
-(*EITHER describes the form of X when the following message is sent,
- OR reduces it to the Fake case.
- Use Says_Server_message_form if applicable.*)
-Goal "[| Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \
-\ \\<in> set evs; \
-\ evs \\<in> kerberos_ban |] \
-\==> (K \\<notin> range shrK & X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}))\
-\ | X \\<in> analz (spies evs)";
-by (case_tac "A \\<in> bad" 1);
-by (fast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]
- addss (simpset())) 1);
-by (forward_tac [Says_imp_spies RS parts.Inj] 1);
-by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2,
- Says_Server_message_form]) 1);
-qed "Says_S_message_form";
-
-
-(*For proofs involving analz.*)
-val analz_spies_tac =
- ftac Says_Server_message_form 7 THEN
- ftac Says_S_message_form 5 THEN
- REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac);
-
-
-(****
- The following is to prove theorems of the form
-
- Key K \\<in> analz (insert (Key KAB) (spies evs)) ==>
- Key K \\<in> analz (spies evs)
-
- A more general formula must be proved inductively.
-
-****)
-
-
-(** Session keys are not used to encrypt other session keys **)
-
-Goal "evs \\<in> kerberos_ban ==> \
-\ \\<forall>K KK. KK <= - (range shrK) --> \
-\ (Key K \\<in> analz (Key`KK Un (spies evs))) = \
-\ (K \\<in> KK | Key K \\<in> analz (spies evs))";
-by (etac kerberos_ban.induct 1);
-by analz_spies_tac;
-by (REPEAT_FIRST (resolve_tac [allI, impI]));
-by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
-(*Takes 5 secs*)
-by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
-(*Fake*)
-by (spy_analz_tac 1);
-qed_spec_mp "analz_image_freshK";
-
-
-Goal "[| evs \\<in> kerberos_ban; KAB \\<notin> range shrK |] ==> \
-\ (Key K \\<in> analz (insert (Key KAB) (spies evs))) = \
-\ (K = KAB | Key K \\<in> analz (spies evs))";
-by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
-qed "analz_insert_freshK";
-
-
-(** The session key K uniquely identifies the message **)
-
-Goal "[| Says Server A \
-\ (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \\<in> set evs; \
-\ Says Server A' \
-\ (Crypt (shrK A') {|Number Ts', Agent B', Key K, X'|}) \\<in> set evs;\
-\ evs \\<in> kerberos_ban |] ==> A=A' & Ts=Ts' & B=B' & X = X'";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-(*Kb2: it can't be a new key*)
-by (Blast_tac 1);
-qed "unique_session_keys";
-
-
-(** Lemma: the session key sent in msg Kb2 would be EXPIRED
- if the spy could see it!
-**)
-
-Goal "[| A \\<notin> bad; B \\<notin> bad; evs \\<in> kerberos_ban |] \
-\ ==> Says Server A \
-\ (Crypt (shrK A) {|Number Ts, Agent B, Key K, \
-\ Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})\
-\ \\<in> set evs --> \
-\ Key K \\<in> analz (spies evs) --> Expired Ts evs";
-by (etac kerberos_ban.induct 1);
-by analz_spies_tac;
-by (ALLGOALS
- (asm_simp_tac (simpset() addsimps [less_SucI, analz_insert_eq,
- analz_insert_freshK] @ pushes)));
-(*Oops: PROOF FAILED if addIs below*)
-by (blast_tac (claset() addDs [unique_session_keys] addSIs [less_SucI]) 4);
-(*Kb2*)
-by (blast_tac (claset() addIs [parts_insertI, less_SucI]) 2);
-(*Fake*)
-by (spy_analz_tac 1);
-(**LEVEL 6 **)
-(*Kb3*)
-by (case_tac "Aa \\<in> bad" 1);
-by (blast_tac (claset() addDs [A_trusts_K_by_Kb2, unique_session_keys]) 2);
-by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj,
- Crypt_Spy_analz_bad, analz.Fst, analz.Snd]
- addIs [less_SucI]) 1);
-qed_spec_mp "lemma2";
-
-
-(** CONFIDENTIALITY for the SERVER:
- Spy does not see the keys sent in msg Kb2
- as long as they have NOT EXPIRED
-**)
-Goal "[| Says Server A \
-\ (Crypt K' {|Number T, Agent B, Key K, X|}) \\<in> set evs; \
-\ ~ Expired T evs; \
-\ A \\<notin> bad; B \\<notin> bad; evs \\<in> kerberos_ban \
-\ |] ==> Key K \\<notin> analz (spies evs)";
-by (ftac Says_Server_message_form 1 THEN assume_tac 1);
-by (blast_tac (claset() addIs [lemma2]) 1);
-qed "Confidentiality_S";
-
-(**** THE COUNTERPART OF CONFIDENTIALITY
- [|...; Expired Ts evs; ...|] ==> Key K \\<in> analz (spies evs)
- WOULD HOLD ONLY IF AN OOPS OCCURRED! ---> Nothing to prove! ****)
-
-
-(** CONFIDENTIALITY for ALICE: **)
-(** Also A_trusts_K_by_Kb2 RS Confidentiality_S **)
-Goal "[| Crypt (shrK A) {|Number T, Agent B, Key K, X|} \\<in> parts (spies evs);\
-\ ~ Expired T evs; \
-\ A \\<notin> bad; B \\<notin> bad; evs \\<in> kerberos_ban \
-\ |] ==> Key K \\<notin> analz (spies evs)";
-by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2, Confidentiality_S]) 1);
-qed "Confidentiality_A";
-
-
-(** CONFIDENTIALITY for BOB: **)
-(** Also B_trusts_K_by_Kb3 RS Confidentiality_S **)
-Goal "[| Crypt (shrK B) {|Number Tk, Agent A, Key K|} \
-\ \\<in> parts (spies evs); \
-\ ~ Expired Tk evs; \
-\ A \\<notin> bad; B \\<notin> bad; evs \\<in> kerberos_ban \
-\ |] ==> Key K \\<notin> analz (spies evs)";
-by (blast_tac (claset() addSDs [B_trusts_K_by_Kb3,
- Confidentiality_S]) 1);
-qed "Confidentiality_B";
-
-
-Goal "[| B \\<notin> bad; evs \\<in> kerberos_ban |] \
-\ ==> Key K \\<notin> analz (spies evs) --> \
-\ Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \
-\ \\<in> set evs --> \
-\ Crypt K (Number Ta) \\<in> parts (spies evs) --> \
-\ Says B A (Crypt K (Number Ta)) \\<in> set evs";
-by (etac kerberos_ban.induct 1);
-by (ftac Says_S_message_form 5 THEN assume_tac 5);
-by (dtac Kb3_msg_in_parts_spies 5);
-by (ftac Oops_parts_spies 7);
-by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
-(**LEVEL 6**)
-by (Blast_tac 1);
-by (Clarify_tac 1);
-(*
-Subgoal 1: contradiction from the assumptions
-Key K \\<notin> used evs2 and Crypt K (Number Ta) \\<in> parts (spies evs2)
-*)
-by (dtac Crypt_imp_invKey_keysFor 1);
-by (Asm_full_simp_tac 1);
-(* the two tactics above detect the contradiction*)
-by (case_tac "Ba \\<in> bad" 1); (*splits up the subgoal by the stated case*)
-by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS
- B_trusts_K_by_Kb3,
- unique_session_keys]) 2);
-by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS analz.Fst RS
- Crypt_Spy_analz_bad]) 1);
-val lemma_B = result();
-
-
-(*AUTHENTICATION OF B TO A*)
-Goal "[| Crypt K (Number Ta) \\<in> parts (spies evs); \
-\ Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} \
-\ \\<in> parts (spies evs); \
-\ ~ Expired Ts evs; \
-\ A \\<notin> bad; B \\<notin> bad; evs \\<in> kerberos_ban |] \
-\ ==> Says B A (Crypt K (Number Ta)) \\<in> set evs";
-by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2]
- addSIs [lemma_B RS mp RS mp RS mp]
- addSEs [Confidentiality_S RSN (2,rev_notE)]) 1);
-qed "Authentication_B";
-
-
-Goal "[| A \\<notin> bad; B \\<notin> bad; evs \\<in> kerberos_ban |] ==> \
-\ Key K \\<notin> analz (spies evs) --> \
-\ Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \
-\ \\<in> set evs --> \
-\ Crypt K {|Agent A, Number Ta|} \\<in> parts (spies evs) -->\
-\ Says A B {|X, Crypt K {|Agent A, Number Ta|}|} \
-\ \\<in> set evs";
-by (etac kerberos_ban.induct 1);
-by (ftac Says_S_message_form 5 THEN assume_tac 5);
-by (ftac Kb3_msg_in_parts_spies 5);
-by (ftac Oops_parts_spies 7);
-by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
-(**LEVEL 6**)
-by (Blast_tac 1);
-by (Clarify_tac 1);
-by (dtac Crypt_imp_invKey_keysFor 1);
-by (Asm_full_simp_tac 1);
-by (blast_tac (claset() addDs [A_trusts_K_by_Kb2, unique_session_keys]) 1);
-val lemma_A = result();
-
-
-(*AUTHENTICATION OF A TO B*)
-Goal "[| Crypt K {|Agent A, Number Ta|} \\<in> parts (spies evs); \
-\ Crypt (shrK B) {|Number Ts, Agent A, Key K|} \
-\ \\<in> parts (spies evs); \
-\ ~ Expired Ts evs; \
-\ A \\<notin> bad; B \\<notin> bad; evs \\<in> kerberos_ban |] \
-\ ==> Says A B {|Crypt (shrK B) {|Number Ts, Agent A, Key K|}, \
-\ Crypt K {|Agent A, Number Ta|}|} \\<in> set evs";
-by (blast_tac (claset() addSDs [B_trusts_K_by_Kb3]
- addSIs [lemma_A RS mp RS mp RS mp]
- addSEs [Confidentiality_S RSN (2,rev_notE)]) 1);
-qed "Authentication_A";
--- a/src/HOL/Auth/Kerberos_BAN.thy Sat Apr 26 12:38:17 2003 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.thy Sat Apr 26 12:38:42 2003 +0200
@@ -8,17 +8,23 @@
From page 251 of
Burrows, Abadi and Needham. A Logic of Authentication.
Proc. Royal Soc. 426 (1989)
+
+ Confidentiality (secrecy) and authentication properties rely on
+ temporal checks: strong guarantees in a little abstracted - but
+ very realistic - model (see .thy).
+
+Tidied and converted to Isar by lcp.
*)
-Kerberos_BAN = Shared +
+theory Kerberos_BAN = Shared:
(* Temporal modelization: session keys can be leaked
ONLY when they have expired *)
syntax
- CT :: event list=>nat
- Expired :: [nat, event list] => bool
- RecentAuth :: [nat, event list] => bool
+ CT :: "event list=>nat"
+ Expired :: "[nat, event list] => bool"
+ RecentAuth :: "[nat, event list] => bool"
consts
@@ -28,12 +34,12 @@
(*Duration of the authenticator*)
AutLife :: nat
-rules
+axioms
(*The ticket should remain fresh for two journeys on the network at least*)
- SesKeyLife_LB "2 <= SesKeyLife"
+ SesKeyLife_LB: "2 <= SesKeyLife"
(*The authenticator only for one journey*)
- AutLife_LB "Suc 0 <= AutLife"
+ AutLife_LB: "Suc 0 <= AutLife"
translations
"CT" == "length"
@@ -42,51 +48,382 @@
"RecentAuth T evs" == "CT evs <= AutLife + T"
-consts kerberos_ban :: event list set
+consts kerberos_ban :: "event list set"
inductive "kerberos_ban"
- intrs
+ intros
+
+ Nil: "[] \<in> kerberos_ban"
+
+ Fake: "[| evsf \<in> kerberos_ban; X \<in> synth (analz (spies evsf)) |]
+ ==> Says Spy B X # evsf \<in> kerberos_ban"
+
+
+ Kb1: "[| evs1 \<in> kerberos_ban |]
+ ==> Says A Server {|Agent A, Agent B|} # evs1
+ \<in> kerberos_ban"
+
+
+ Kb2: "[| evs2 \<in> kerberos_ban; Key KAB \<notin> used evs2;
+ Says A' Server {|Agent A, Agent B|} \<in> set evs2 |]
+ ==> Says Server A
+ (Crypt (shrK A)
+ {|Number (CT evs2), Agent B, Key KAB,
+ (Crypt (shrK B) {|Number (CT evs2), Agent A, Key KAB|})|})
+ # evs2 \<in> kerberos_ban"
+
+
+ Kb3: "[| evs3 \<in> kerberos_ban;
+ Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
+ \<in> set evs3;
+ Says A Server {|Agent A, Agent B|} \<in> set evs3;
+ ~ Expired Ts evs3 |]
+ ==> Says A B {|X, Crypt K {|Agent A, Number (CT evs3)|} |}
+ # evs3 \<in> kerberos_ban"
+
+
+ Kb4: "[| evs4 \<in> kerberos_ban;
+ Says A' B {|(Crypt (shrK B) {|Number Ts, Agent A, Key K|}),
+ (Crypt K {|Agent A, Number Ta|}) |}: set evs4;
+ ~ Expired Ts evs4; RecentAuth Ta evs4 |]
+ ==> Says B A (Crypt K (Number Ta)) # evs4
+ \<in> kerberos_ban"
- Nil "[] \\<in> kerberos_ban"
+ (*Old session keys may become compromised*)
+ Oops: "[| evso \<in> kerberos_ban;
+ Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
+ \<in> set evso;
+ Expired Ts evso |]
+ ==> Notes Spy {|Number Ts, Key K|} # evso \<in> kerberos_ban"
+
+
+declare Says_imp_knows_Spy [THEN parts.Inj, dest] parts.Body [dest]
+declare analz_subset_parts [THEN subsetD, dest]
+declare Fake_parts_insert [THEN subsetD, dest]
+
+declare SesKeyLife_LB [iff] AutLife_LB [iff]
+
- Fake "[| evsf \\<in> kerberos_ban; X \\<in> synth (analz (spies evsf)) |]
- ==> Says Spy B X # evsf \\<in> kerberos_ban"
+(*A "possibility property": there are traces that reach the end.*)
+lemma "\<exists>Timestamp K. \<exists>evs \<in> kerberos_ban.
+ Says B A (Crypt K (Number Timestamp))
+ \<in> set evs"
+apply (cut_tac SesKeyLife_LB)
+apply (intro exI bexI)
+apply (rule_tac [2]
+ kerberos_ban.Nil [THEN kerberos_ban.Kb1, THEN kerberos_ban.Kb2,
+ THEN kerberos_ban.Kb3, THEN kerberos_ban.Kb4], possibility)
+apply (simp_all (no_asm_simp))
+done
+
+
+(**** Inductive proofs about kerberos_ban ****)
+
+(*Forwarding Lemma for reasoning about the encrypted portion of message Kb3*)
+lemma Kb3_msg_in_parts_spies:
+ "Says S A (Crypt KA {|Timestamp, B, K, X|}) \<in> set evs
+ ==> X \<in> parts (spies evs)"
+by blast
+
+lemma Oops_parts_spies:
+ "Says Server A (Crypt (shrK A) {|Timestamp, B, K, X|}) \<in> set evs
+ ==> K \<in> parts (spies evs)"
+by blast
+
+
+(*Spy never sees another agent's shared key! (unless it's bad at start)*)
+lemma Spy_see_shrK [simp]:
+ "evs \<in> kerberos_ban ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
+apply (erule kerberos_ban.induct)
+apply (frule_tac [7] Oops_parts_spies)
+apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all)
+apply blast+
+done
- Kb1 "[| evs1 \\<in> kerberos_ban |]
- ==> Says A Server {|Agent A, Agent B|} # evs1
- \\<in> kerberos_ban"
+lemma Spy_analz_shrK [simp]:
+ "evs \<in> kerberos_ban ==> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
+apply auto
+done
+
+
+lemma Spy_see_shrK_D [dest!]:
+ "[| Key (shrK A) \<in> parts (spies evs);
+ evs \<in> kerberos_ban |] ==> A:bad"
+apply (blast dest: Spy_see_shrK)
+done
+
+lemmas Spy_analz_shrK_D = analz_subset_parts [THEN subsetD, THEN Spy_see_shrK_D, dest!]
+
+
+(*Nobody can have used non-existent keys!*)
+lemma new_keys_not_used [rule_format, simp]:
+ "evs \<in> kerberos_ban ==>
+ Key K \<notin> used evs --> K \<notin> keysFor (parts (spies evs))"
+apply (erule kerberos_ban.induct)
+apply (frule_tac [7] Oops_parts_spies)
+apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all)
+(*Fake*)
+apply (force dest!: keysFor_parts_insert)
+(*Kb2, Kb3, Kb4*)
+apply blast+
+done
+
+(** Lemmas concerning the form of items passed in messages **)
+
+(*Describes the form of K, X and K' when the Server sends this message.*)
+lemma Says_Server_message_form:
+ "[| Says Server A (Crypt K' {|Number Ts, Agent B, Key K, X|})
+ \<in> set evs; evs \<in> kerberos_ban |]
+ ==> K \<notin> range shrK &
+ X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}) &
+ K' = shrK A"
+apply (erule rev_mp)
+apply (erule kerberos_ban.induct, auto)
+done
- Kb2 "[| evs2 \\<in> kerberos_ban; Key KAB \\<notin> used evs2;
- Says A' Server {|Agent A, Agent B|} \\<in> set evs2 |]
- ==> Says Server A
- (Crypt (shrK A)
- {|Number (CT evs2), Agent B, Key KAB,
- (Crypt (shrK B) {|Number (CT evs2), Agent A, Key KAB|})|})
- # evs2 \\<in> kerberos_ban"
+(*If the encrypted message appears then it originated with the Server
+ PROVIDED that A is NOT compromised!
+
+ This shows implicitly the FRESHNESS OF THE SESSION KEY to A
+*)
+lemma A_trusts_K_by_Kb2:
+ "[| Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}
+ \<in> parts (spies evs);
+ A \<notin> bad; evs \<in> kerberos_ban |]
+ ==> Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
+ \<in> set evs"
+apply (erule rev_mp)
+apply (erule kerberos_ban.induct)
+apply (frule_tac [7] Oops_parts_spies)
+apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all)
+apply blast
+done
+
+
+(*If the TICKET appears then it originated with the Server*)
+(*FRESHNESS OF THE SESSION KEY to B*)
+lemma B_trusts_K_by_Kb3:
+ "[| Crypt (shrK B) {|Number Ts, Agent A, Key K|} \<in> parts (spies evs);
+ B \<notin> bad; evs \<in> kerberos_ban |]
+ ==> Says Server A
+ (Crypt (shrK A) {|Number Ts, Agent B, Key K,
+ Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})
+ \<in> set evs"
+apply (erule rev_mp)
+apply (erule kerberos_ban.induct)
+apply (frule_tac [7] Oops_parts_spies)
+apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all)
+apply blast
+done
+
+
+(*EITHER describes the form of X when the following message is sent,
+ OR reduces it to the Fake case.
+ Use Says_Server_message_form if applicable.*)
+lemma Says_S_message_form:
+ "[| Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
+ \<in> set evs;
+ evs \<in> kerberos_ban |]
+ ==> (K \<notin> range shrK & X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}))
+ | X \<in> analz (spies evs)"
+apply (case_tac "A \<in> bad")
+apply (force dest!: Says_imp_spies [THEN analz.Inj])
+apply (frule Says_imp_spies [THEN parts.Inj])
+apply (blast dest!: A_trusts_K_by_Kb2 Says_Server_message_form)
+done
+
- Kb3 "[| evs3 \\<in> kerberos_ban;
- Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
- \\<in> set evs3;
- Says A Server {|Agent A, Agent B|} \\<in> set evs3;
- ~ Expired Ts evs3 |]
- ==> Says A B {|X, Crypt K {|Agent A, Number (CT evs3)|} |}
- # evs3 \\<in> kerberos_ban"
+(****
+ The following is to prove theorems of the form
+
+ Key K \<in> analz (insert (Key KAB) (spies evs)) ==>
+ Key K \<in> analz (spies evs)
+
+ A more general formula must be proved inductively.
+
+****)
+
+
+(** Session keys are not used to encrypt other session keys **)
+
+lemma analz_image_freshK [rule_format (no_asm)]:
+ "evs \<in> kerberos_ban ==>
+ \<forall>K KK. KK <= - (range shrK) -->
+ (Key K \<in> analz (Key`KK Un (spies evs))) =
+ (K \<in> KK | Key K \<in> analz (spies evs))"
+apply (erule kerberos_ban.induct)
+apply (drule_tac [7] Says_Server_message_form)
+apply (erule_tac [5] Says_S_message_form [THEN disjE], analz_freshK, spy_analz)
+done
+
+
+
+lemma analz_insert_freshK:
+ "[| evs \<in> kerberos_ban; KAB \<notin> range shrK |] ==>
+ (Key K \<in> analz (insert (Key KAB) (spies evs))) =
+ (K = KAB | Key K \<in> analz (spies evs))"
+by (simp only: analz_image_freshK analz_image_freshK_simps)
+
+
+(** The session key K uniquely identifies the message **)
+
+lemma unique_session_keys:
+ "[| Says Server A
+ (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \<in> set evs;
+ Says Server A'
+ (Crypt (shrK A') {|Number Ts', Agent B', Key K, X'|}) \<in> set evs;
+ evs \<in> kerberos_ban |] ==> A=A' & Ts=Ts' & B=B' & X = X'"
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule kerberos_ban.induct)
+apply (frule_tac [7] Oops_parts_spies)
+apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all)
+(*Kb2: it can't be a new key*)
+apply blast
+done
+
+
+(** Lemma: the session key sent in msg Kb2 would be EXPIRED
+ if the spy could see it!
+**)
+
+lemma lemma2 [rule_format (no_asm)]:
+ "[| A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |]
+ ==> Says Server A
+ (Crypt (shrK A) {|Number Ts, Agent B, Key K,
+ Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})
+ \<in> set evs -->
+ Key K \<in> analz (spies evs) --> Expired Ts evs"
+apply (erule kerberos_ban.induct)
+apply (frule_tac [7] Says_Server_message_form)
+apply (frule_tac [5] Says_S_message_form [THEN disjE])
+apply (simp_all (no_asm_simp) add: less_SucI analz_insert_eq analz_insert_freshK pushes)
+txt{*Fake*}
+apply spy_analz
+txt{*Kb2*}
+apply (blast intro: parts_insertI less_SucI)
+txt{*Kb3*}
+apply (case_tac "Aa \<in> bad")
+ prefer 2 apply (blast dest: A_trusts_K_by_Kb2 unique_session_keys)
+apply (blast dest: Says_imp_spies [THEN analz.Inj] Crypt_Spy_analz_bad elim!: MPair_analz intro: less_SucI)
+txt{*Oops: PROOF FAILED if addIs below*}
+apply (blast dest: unique_session_keys intro!: less_SucI)
+done
- Kb4 "[| evs4 \\<in> kerberos_ban;
- Says A' B {|(Crypt (shrK B) {|Number Ts, Agent A, Key K|}),
- (Crypt K {|Agent A, Number Ta|}) |}: set evs4;
- ~ Expired Ts evs4; RecentAuth Ta evs4 |]
- ==> Says B A (Crypt K (Number Ta)) # evs4
- \\<in> kerberos_ban"
+(** CONFIDENTIALITY for the SERVER:
+ Spy does not see the keys sent in msg Kb2
+ as long as they have NOT EXPIRED
+**)
+lemma Confidentiality_S:
+ "[| Says Server A
+ (Crypt K' {|Number T, Agent B, Key K, X|}) \<in> set evs;
+ ~ Expired T evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban
+ |] ==> Key K \<notin> analz (spies evs)"
+apply (frule Says_Server_message_form, assumption)
+apply (blast intro: lemma2)
+done
+
+(**** THE COUNTERPART OF CONFIDENTIALITY
+ [|...; Expired Ts evs; ...|] ==> Key K \<in> analz (spies evs)
+ WOULD HOLD ONLY IF AN OOPS OCCURRED! ---> Nothing to prove! ****)
+
+
+(** CONFIDENTIALITY for ALICE: **)
+(** Also A_trusts_K_by_Kb2 RS Confidentiality_S **)
+lemma Confidentiality_A:
+ "[| Crypt (shrK A) {|Number T, Agent B, Key K, X|} \<in> parts (spies evs);
+ ~ Expired T evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban
+ |] ==> Key K \<notin> analz (spies evs)"
+apply (blast dest!: A_trusts_K_by_Kb2 Confidentiality_S)
+done
+
+
+(** CONFIDENTIALITY for BOB: **)
+(** Also B_trusts_K_by_Kb3 RS Confidentiality_S **)
+lemma Confidentiality_B:
+ "[| Crypt (shrK B) {|Number Tk, Agent A, Key K|}
+ \<in> parts (spies evs);
+ ~ Expired Tk evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban
+ |] ==> Key K \<notin> analz (spies evs)"
+apply (blast dest!: B_trusts_K_by_Kb3 Confidentiality_S)
+done
+
- (*Old session keys may become compromised*)
- Oops "[| evso \\<in> kerberos_ban;
- Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
- \\<in> set evso;
- Expired Ts evso |]
- ==> Notes Spy {|Number Ts, Key K|} # evso \\<in> kerberos_ban"
+lemma lemma_B [rule_format]:
+ "[| B \<notin> bad; evs \<in> kerberos_ban |]
+ ==> Key K \<notin> analz (spies evs) -->
+ Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
+ \<in> set evs -->
+ Crypt K (Number Ta) \<in> parts (spies evs) -->
+ Says B A (Crypt K (Number Ta)) \<in> set evs"
+apply (erule kerberos_ban.induct)
+apply (frule_tac [7] Oops_parts_spies)
+apply (frule_tac [5] Says_S_message_form)
+apply (drule_tac [6] Kb3_msg_in_parts_spies, analz_mono_contra)
+apply (simp_all (no_asm_simp) add: all_conj_distrib)
+txt{*Fake*}
+apply blast
+txt{*Kb2*}
+apply (force dest: Crypt_imp_invKey_keysFor)
+txt{*Kb4*}
+apply (blast dest: B_trusts_K_by_Kb3 unique_session_keys
+ Says_imp_spies [THEN analz.Inj] Crypt_Spy_analz_bad)
+done
+
+
+(*AUTHENTICATION OF B TO A*)
+lemma Authentication_B:
+ "[| Crypt K (Number Ta) \<in> parts (spies evs);
+ Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}
+ \<in> parts (spies evs);
+ ~ Expired Ts evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |]
+ ==> Says B A (Crypt K (Number Ta)) \<in> set evs"
+by (blast dest!: A_trusts_K_by_Kb2
+ intro!: lemma_B elim!: Confidentiality_S [THEN [2] rev_notE])
+
+
+
+lemma lemma_A [rule_format]:
+ "[| A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |]
+ ==>
+ Key K \<notin> analz (spies evs) -->
+ Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
+ \<in> set evs -->
+ Crypt K {|Agent A, Number Ta|} \<in> parts (spies evs) -->
+ Says A B {|X, Crypt K {|Agent A, Number Ta|}|}
+ \<in> set evs"
+apply (erule kerberos_ban.induct)
+apply (frule_tac [7] Oops_parts_spies)
+apply (frule_tac [5] Says_S_message_form)
+apply (frule_tac [6] Kb3_msg_in_parts_spies, analz_mono_contra)
+apply (simp_all (no_asm_simp) add: all_conj_distrib)
+txt{*Fake*}
+apply blast
+txt{*Kb2*}
+apply (force dest: Crypt_imp_invKey_keysFor)
+txt{*Kb3*}
+apply (blast dest: A_trusts_K_by_Kb2 unique_session_keys)
+done
+
+
+(*AUTHENTICATION OF A TO B*)
+lemma Authentication_A:
+ "[| Crypt K {|Agent A, Number Ta|} \<in> parts (spies evs);
+ Crypt (shrK B) {|Number Ts, Agent A, Key K|}
+ \<in> parts (spies evs);
+ ~ Expired Ts evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |]
+ ==> Says A B {|Crypt (shrK B) {|Number Ts, Agent A, Key K|},
+ Crypt K {|Agent A, Number Ta|}|} \<in> set evs"
+by (blast dest!: B_trusts_K_by_Kb3
+ intro!: lemma_A
+ elim!: Confidentiality_S [THEN [2] rev_notE])
end
--- a/src/HOL/Auth/Message.thy Sat Apr 26 12:38:17 2003 +0200
+++ b/src/HOL/Auth/Message.thy Sat Apr 26 12:38:42 2003 +0200
@@ -7,11 +7,10 @@
Inductive relations "parts", "analz" and "synth"
*)
-theory Message = Main
-files ("Message_lemmas.ML"):
+theory Message = Main:
(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
-lemma [simp] : "A Un (B Un A) = B Un A"
+lemma [simp] : "A \<union> (B \<union> A) = B \<union> A"
by blast
types
@@ -83,6 +82,238 @@
done
+(*Equations hold because constructors are injective; cannot prove for all f*)
+lemma Friend_image_eq [simp]: "(Friend x \<in> Friend`A) = (x:A)"
+by auto
+
+lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x\<in>A)"
+by auto
+
+lemma Nonce_Key_image_eq [simp]: "(Nonce x \<notin> Key`A)"
+by auto
+
+
+(** Inverse of keys **)
+
+lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
+apply safe
+apply (drule_tac f = invKey in arg_cong, simp)
+done
+
+
+subsection{*keysFor operator*}
+
+lemma keysFor_empty [simp]: "keysFor {} = {}"
+by (unfold keysFor_def, blast)
+
+lemma keysFor_Un [simp]: "keysFor (H \<union> H') = keysFor H \<union> keysFor H'"
+by (unfold keysFor_def, blast)
+
+lemma keysFor_UN [simp]: "keysFor (\<Union>i\<in>A. H i) = (\<Union>i\<in>A. keysFor (H i))"
+by (unfold keysFor_def, blast)
+
+(*Monotonicity*)
+lemma keysFor_mono: "G\<subseteq>H ==> keysFor(G) \<subseteq> keysFor(H)"
+by (unfold keysFor_def, blast)
+
+lemma keysFor_insert_Agent [simp]: "keysFor (insert (Agent A) H) = keysFor H"
+by (unfold keysFor_def, auto)
+
+lemma keysFor_insert_Nonce [simp]: "keysFor (insert (Nonce N) H) = keysFor H"
+by (unfold keysFor_def, auto)
+
+lemma keysFor_insert_Number [simp]: "keysFor (insert (Number N) H) = keysFor H"
+by (unfold keysFor_def, auto)
+
+lemma keysFor_insert_Key [simp]: "keysFor (insert (Key K) H) = keysFor H"
+by (unfold keysFor_def, auto)
+
+lemma keysFor_insert_Hash [simp]: "keysFor (insert (Hash X) H) = keysFor H"
+by (unfold keysFor_def, auto)
+
+lemma keysFor_insert_MPair [simp]: "keysFor (insert {|X,Y|} H) = keysFor H"
+by (unfold keysFor_def, auto)
+
+lemma keysFor_insert_Crypt [simp]:
+ "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"
+apply (unfold keysFor_def, auto)
+done
+
+lemma keysFor_image_Key [simp]: "keysFor (Key`E) = {}"
+by (unfold keysFor_def, auto)
+
+lemma Crypt_imp_invKey_keysFor: "Crypt K X \<in> H ==> invKey K \<in> keysFor H"
+by (unfold keysFor_def, blast)
+
+
+subsection{*Inductive relation "parts"*}
+
+lemma MPair_parts:
+ "[| {|X,Y|} \<in> parts H;
+ [| X \<in> parts H; Y \<in> parts H |] ==> P |] ==> P"
+by (blast dest: parts.Fst parts.Snd)
+
+declare MPair_parts [elim!] parts.Body [dest!]
+text{*NB These two rules are UNSAFE in the formal sense, as they discard the
+ compound message. They work well on THIS FILE.
+ @{text MPair_parts} is left as SAFE because it speeds up proofs.
+ The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*}
+
+lemma parts_increasing: "H \<subseteq> parts(H)"
+by blast
+
+lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD, standard]
+
+lemma parts_empty [simp]: "parts{} = {}"
+apply safe
+apply (erule parts.induct, blast+)
+done
+
+lemma parts_emptyE [elim!]: "X\<in> parts{} ==> P"
+by simp
+
+(*WARNING: loops if H = {Y}, therefore must not be repeated!*)
+lemma parts_singleton: "X\<in> parts H ==> \<exists>Y\<in>H. X\<in> parts {Y}"
+by (erule parts.induct, blast+)
+
+
+(** Unions **)
+
+lemma parts_Un_subset1: "parts(G) \<union> parts(H) \<subseteq> parts(G \<union> H)"
+by (intro Un_least parts_mono Un_upper1 Un_upper2)
+
+lemma parts_Un_subset2: "parts(G \<union> H) \<subseteq> parts(G) \<union> parts(H)"
+apply (rule subsetI)
+apply (erule parts.induct, blast+)
+done
+
+lemma parts_Un [simp]: "parts(G \<union> H) = parts(G) \<union> parts(H)"
+by (intro equalityI parts_Un_subset1 parts_Un_subset2)
+
+lemma parts_insert: "parts (insert X H) = parts {X} \<union> parts H"
+apply (subst insert_is_Un [of _ H])
+apply (simp only: parts_Un)
+done
+
+(*TWO inserts to avoid looping. This rewrite is better than nothing.
+ Not suitable for Addsimps: its behaviour can be strange.*)
+lemma parts_insert2: "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
+apply (simp add: Un_assoc)
+apply (simp add: parts_insert [symmetric])
+done
+
+lemma parts_UN_subset1: "(\<Union>x\<in>A. parts(H x)) \<subseteq> parts(\<Union>x\<in>A. H x)"
+by (intro UN_least parts_mono UN_upper)
+
+lemma parts_UN_subset2: "parts(\<Union>x\<in>A. H x) \<subseteq> (\<Union>x\<in>A. parts(H x))"
+apply (rule subsetI)
+apply (erule parts.induct, blast+)
+done
+
+lemma parts_UN [simp]: "parts(\<Union>x\<in>A. H x) = (\<Union>x\<in>A. parts(H x))"
+by (intro equalityI parts_UN_subset1 parts_UN_subset2)
+
+(*Added to simplify arguments to parts, analz and synth.
+ NOTE: the UN versions are no longer used!*)
+
+
+text{*This allows @{text blast} to simplify occurrences of
+ @{term "parts(G\<union>H)"} in the assumption.*}
+declare parts_Un [THEN equalityD1, THEN subsetD, THEN UnE, elim!]
+
+
+lemma parts_insert_subset: "insert X (parts H) \<subseteq> parts(insert X H)"
+by (blast intro: parts_mono [THEN [2] rev_subsetD])
+
+(** Idempotence and transitivity **)
+
+lemma parts_partsD [dest!]: "X\<in> parts (parts H) ==> X\<in> parts H"
+by (erule parts.induct, blast+)
+
+lemma parts_idem [simp]: "parts (parts H) = parts H"
+by blast
+
+lemma parts_trans: "[| X\<in> parts G; G \<subseteq> parts H |] ==> X\<in> parts H"
+by (drule parts_mono, blast)
+
+(*Cut*)
+lemma parts_cut: "[| Y\<in> parts (insert X G); X\<in> parts H |]
+ ==> Y\<in> parts (G \<union> H)"
+apply (erule parts_trans, auto)
+done
+
+lemma parts_cut_eq [simp]: "X\<in> parts H ==> parts (insert X H) = parts H"
+by (force dest!: parts_cut intro: parts_insertI)
+
+
+(** Rewrite rules for pulling out atomic messages **)
+
+lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset]
+
+
+lemma parts_insert_Agent [simp]: "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"
+apply (rule parts_insert_eq_I)
+apply (erule parts.induct, auto)
+done
+
+lemma parts_insert_Nonce [simp]: "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"
+apply (rule parts_insert_eq_I)
+apply (erule parts.induct, auto)
+done
+
+lemma parts_insert_Number [simp]: "parts (insert (Number N) H) = insert (Number N) (parts H)"
+apply (rule parts_insert_eq_I)
+apply (erule parts.induct, auto)
+done
+
+lemma parts_insert_Key [simp]: "parts (insert (Key K) H) = insert (Key K) (parts H)"
+apply (rule parts_insert_eq_I)
+apply (erule parts.induct, auto)
+done
+
+lemma parts_insert_Hash [simp]: "parts (insert (Hash X) H) = insert (Hash X) (parts H)"
+apply (rule parts_insert_eq_I)
+apply (erule parts.induct, auto)
+done
+
+lemma parts_insert_Crypt [simp]: "parts (insert (Crypt K X) H) =
+ insert (Crypt K X) (parts (insert X H))"
+apply (rule equalityI)
+apply (rule subsetI)
+apply (erule parts.induct, auto)
+apply (erule parts.induct)
+apply (blast intro: parts.Body)+
+done
+
+lemma parts_insert_MPair [simp]: "parts (insert {|X,Y|} H) =
+ insert {|X,Y|} (parts (insert X (insert Y H)))"
+apply (rule equalityI)
+apply (rule subsetI)
+apply (erule parts.induct, auto)
+apply (erule parts.induct)
+apply (blast intro: parts.Fst parts.Snd)+
+done
+
+lemma parts_image_Key [simp]: "parts (Key`N) = Key`N"
+apply auto
+apply (erule parts.induct, auto)
+done
+
+
+(*In any message, there is an upper bound N on its greatest nonce.*)
+lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n --> Nonce n \<notin> parts {msg}"
+apply (induct_tac "msg")
+apply (simp_all (no_asm_simp) add: exI parts_insert2)
+(*MPair case: blast_tac works out the necessary sum itself!*)
+prefer 2 apply (blast elim!: add_leE)
+(*Nonce case*)
+apply (rule_tac x = "N + Suc nat" in exI)
+apply (auto elim!: add_leE)
+done
+
+
+subsection{*Inductive relation "analz"*}
+
(** Inductive definition of "analz" -- what can be broken down from a set of
messages, including keys. A form of downward closure. Pairs can
be taken apart; messages decrypted with known keys. **)
@@ -104,6 +335,211 @@
apply (auto dest: Fst Snd)
done
+text{*Making it safe speeds up proofs*}
+lemma MPair_analz [elim!]:
+ "[| {|X,Y|} \<in> analz H;
+ [| X \<in> analz H; Y \<in> analz H |] ==> P
+ |] ==> P"
+by (blast dest: analz.Fst analz.Snd)
+
+lemma analz_increasing: "H \<subseteq> analz(H)"
+by blast
+
+lemma analz_subset_parts: "analz H \<subseteq> parts H"
+apply (rule subsetI)
+apply (erule analz.induct, blast+)
+done
+
+lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
+
+
+lemma parts_analz [simp]: "parts (analz H) = parts H"
+apply (rule equalityI)
+apply (rule analz_subset_parts [THEN parts_mono, THEN subset_trans], simp)
+apply (blast intro: analz_increasing [THEN parts_mono, THEN subsetD])
+done
+
+lemma analz_parts [simp]: "analz (parts H) = parts H"
+apply auto
+apply (erule analz.induct, auto)
+done
+
+lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard]
+
+(** General equational properties **)
+
+lemma analz_empty [simp]: "analz{} = {}"
+apply safe
+apply (erule analz.induct, blast+)
+done
+
+(*Converse fails: we can analz more from the union than from the
+ separate parts, as a key in one might decrypt a message in the other*)
+lemma analz_Un: "analz(G) \<union> analz(H) \<subseteq> analz(G \<union> H)"
+by (intro Un_least analz_mono Un_upper1 Un_upper2)
+
+lemma analz_insert: "insert X (analz H) \<subseteq> analz(insert X H)"
+by (blast intro: analz_mono [THEN [2] rev_subsetD])
+
+(** Rewrite rules for pulling out atomic messages **)
+
+lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert]
+
+lemma analz_insert_Agent [simp]: "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"
+apply (rule analz_insert_eq_I)
+apply (erule analz.induct, auto)
+done
+
+lemma analz_insert_Nonce [simp]: "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"
+apply (rule analz_insert_eq_I)
+apply (erule analz.induct, auto)
+done
+
+lemma analz_insert_Number [simp]: "analz (insert (Number N) H) = insert (Number N) (analz H)"
+apply (rule analz_insert_eq_I)
+apply (erule analz.induct, auto)
+done
+
+lemma analz_insert_Hash [simp]: "analz (insert (Hash X) H) = insert (Hash X) (analz H)"
+apply (rule analz_insert_eq_I)
+apply (erule analz.induct, auto)
+done
+
+(*Can only pull out Keys if they are not needed to decrypt the rest*)
+lemma analz_insert_Key [simp]:
+ "K \<notin> keysFor (analz H) ==>
+ analz (insert (Key K) H) = insert (Key K) (analz H)"
+apply (unfold keysFor_def)
+apply (rule analz_insert_eq_I)
+apply (erule analz.induct, auto)
+done
+
+lemma analz_insert_MPair [simp]: "analz (insert {|X,Y|} H) =
+ insert {|X,Y|} (analz (insert X (insert Y H)))"
+apply (rule equalityI)
+apply (rule subsetI)
+apply (erule analz.induct, auto)
+apply (erule analz.induct)
+apply (blast intro: analz.Fst analz.Snd)+
+done
+
+(*Can pull out enCrypted message if the Key is not known*)
+lemma analz_insert_Crypt:
+ "Key (invKey K) \<notin> analz H
+ ==> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)"
+apply (rule analz_insert_eq_I)
+apply (erule analz.induct, auto)
+
+done
+
+lemma lemma1: "Key (invKey K) \<in> analz H ==>
+ analz (insert (Crypt K X) H) \<subseteq>
+ insert (Crypt K X) (analz (insert X H))"
+apply (rule subsetI)
+apply (erule_tac xa = x in analz.induct, auto)
+done
+
+lemma lemma2: "Key (invKey K) \<in> analz H ==>
+ insert (Crypt K X) (analz (insert X H)) \<subseteq>
+ analz (insert (Crypt K X) H)"
+apply auto
+apply (erule_tac xa = x in analz.induct, auto)
+apply (blast intro: analz_insertI analz.Decrypt)
+done
+
+lemma analz_insert_Decrypt: "Key (invKey K) \<in> analz H ==>
+ analz (insert (Crypt K X) H) =
+ insert (Crypt K X) (analz (insert X H))"
+by (intro equalityI lemma1 lemma2)
+
+(*Case analysis: either the message is secure, or it is not!
+ Effective, but can cause subgoals to blow up!
+ Use with split_if; apparently split_tac does not cope with patterns
+ such as "analz (insert (Crypt K X) H)" *)
+lemma analz_Crypt_if [simp]:
+ "analz (insert (Crypt K X) H) =
+ (if (Key (invKey K) \<in> analz H)
+ then insert (Crypt K X) (analz (insert X H))
+ else insert (Crypt K X) (analz H))"
+by (simp add: analz_insert_Crypt analz_insert_Decrypt)
+
+
+(*This rule supposes "for the sake of argument" that we have the key.*)
+lemma analz_insert_Crypt_subset: "analz (insert (Crypt K X) H) \<subseteq>
+ insert (Crypt K X) (analz (insert X H))"
+apply (rule subsetI)
+apply (erule analz.induct, auto)
+done
+
+
+lemma analz_image_Key [simp]: "analz (Key`N) = Key`N"
+apply auto
+apply (erule analz.induct, auto)
+done
+
+
+(** Idempotence and transitivity **)
+
+lemma analz_analzD [dest!]: "X\<in> analz (analz H) ==> X\<in> analz H"
+by (erule analz.induct, blast+)
+
+lemma analz_idem [simp]: "analz (analz H) = analz H"
+by blast
+
+lemma analz_trans: "[| X\<in> analz G; G \<subseteq> analz H |] ==> X\<in> analz H"
+by (drule analz_mono, blast)
+
+(*Cut; Lemma 2 of Lowe*)
+lemma analz_cut: "[| Y\<in> analz (insert X H); X\<in> analz H |] ==> Y\<in> analz H"
+by (erule analz_trans, blast)
+
+(*Cut can be proved easily by induction on
+ "Y: analz (insert X H) ==> X: analz H --> Y: analz H"
+*)
+
+(*This rewrite rule helps in the simplification of messages that involve
+ the forwarding of unknown components (X). Without it, removing occurrences
+ of X can be very complicated. *)
+lemma analz_insert_eq: "X\<in> analz H ==> analz (insert X H) = analz H"
+by (blast intro: analz_cut analz_insertI)
+
+
+(** A congruence rule for "analz" **)
+
+lemma analz_subset_cong: "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H'
+ |] ==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
+apply clarify
+apply (erule analz.induct)
+apply (best intro: analz_mono [THEN subsetD])+
+done
+
+lemma analz_cong: "[| analz G = analz G'; analz H = analz H'
+ |] ==> analz (G \<union> H) = analz (G' \<union> H')"
+apply (intro equalityI analz_subset_cong, simp_all)
+done
+
+
+lemma analz_insert_cong: "analz H = analz H' ==> analz(insert X H) = analz(insert X H')"
+by (force simp only: insert_def intro!: analz_cong)
+
+(*If there are no pairs or encryptions then analz does nothing*)
+lemma analz_trivial: "[| \<forall>X Y. {|X,Y|} \<notin> H; \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
+apply safe
+apply (erule analz.induct, blast+)
+done
+
+(*These two are obsolete (with a single Spy) but cost little to prove...*)
+lemma analz_UN_analz_lemma: "X\<in> analz (\<Union>i\<in>A. analz (H i)) ==> X\<in> analz (\<Union>i\<in>A. H i)"
+apply (erule analz.induct)
+apply (blast intro: analz_mono [THEN [2] rev_subsetD])+
+done
+
+lemma analz_UN_analz [simp]: "analz (\<Union>i\<in>A. analz (H i)) = analz (\<Union>i\<in>A. H i)"
+by (blast intro: analz_UN_analz_lemma analz_mono [THEN [2] rev_subsetD])
+
+
+subsection{*Inductive relation "synth"*}
+
(** Inductive definition of "synth" -- what can be built up from a set of
messages. A form of upward closure. Pairs can be built, messages
encrypted with known keys. Agent names are public domain.
@@ -133,7 +569,376 @@
inductive_cases MPair_synth [elim!]: "{|X,Y|} \<in> synth H"
inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"
-use "Message_lemmas.ML"
+
+lemma synth_increasing: "H \<subseteq> synth(H)"
+by blast
+
+(** Unions **)
+
+(*Converse fails: we can synth more from the union than from the
+ separate parts, building a compound message using elements of each.*)
+lemma synth_Un: "synth(G) \<union> synth(H) \<subseteq> synth(G \<union> H)"
+by (intro Un_least synth_mono Un_upper1 Un_upper2)
+
+lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)"
+by (blast intro: synth_mono [THEN [2] rev_subsetD])
+
+(** Idempotence and transitivity **)
+
+lemma synth_synthD [dest!]: "X\<in> synth (synth H) ==> X\<in> synth H"
+by (erule synth.induct, blast+)
+
+lemma synth_idem: "synth (synth H) = synth H"
+by blast
+
+lemma synth_trans: "[| X\<in> synth G; G \<subseteq> synth H |] ==> X\<in> synth H"
+by (drule synth_mono, blast)
+
+(*Cut; Lemma 2 of Lowe*)
+lemma synth_cut: "[| Y\<in> synth (insert X H); X\<in> synth H |] ==> Y\<in> synth H"
+by (erule synth_trans, blast)
+
+lemma Agent_synth [simp]: "Agent A \<in> synth H"
+by blast
+
+lemma Number_synth [simp]: "Number n \<in> synth H"
+by blast
+
+lemma Nonce_synth_eq [simp]: "(Nonce N \<in> synth H) = (Nonce N \<in> H)"
+by blast
+
+lemma Key_synth_eq [simp]: "(Key K \<in> synth H) = (Key K \<in> H)"
+by blast
+
+lemma Crypt_synth_eq [simp]: "Key K \<notin> H ==> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)"
+by blast
+
+
+lemma keysFor_synth [simp]:
+ "keysFor (synth H) = keysFor H \<union> invKey`{K. Key K \<in> H}"
+apply (unfold keysFor_def, blast)
+done
+
+
+(*** Combinations of parts, analz and synth ***)
+
+lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H"
+apply (rule equalityI)
+apply (rule subsetI)
+apply (erule parts.induct)
+apply (blast intro: synth_increasing [THEN parts_mono, THEN subsetD]
+ parts.Fst parts.Snd parts.Body)+
+done
+
+lemma analz_analz_Un [simp]: "analz (analz G \<union> H) = analz (G \<union> H)"
+apply (intro equalityI analz_subset_cong)+
+apply simp_all
+done
+
+lemma analz_synth_Un [simp]: "analz (synth G \<union> H) = analz (G \<union> H) \<union> synth G"
+apply (rule equalityI)
+apply (rule subsetI)
+apply (erule analz.induct)
+prefer 5 apply (blast intro: analz_mono [THEN [2] rev_subsetD])
+apply (blast intro: analz.Fst analz.Snd analz.Decrypt)+
+done
+
+lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"
+apply (cut_tac H = "{}" in analz_synth_Un)
+apply (simp (no_asm_use))
+done
+
+
+(** For reasoning about the Fake rule in traces **)
+
+lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
+by (rule subset_trans [OF parts_mono parts_Un_subset2], blast)
+
+(*More specifically for Fake. Very occasionally we could do with a version
+ of the form parts{X} \<subseteq> synth (analz H) \<union> parts H *)
+lemma Fake_parts_insert: "X \<in> synth (analz H) ==>
+ parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
+apply (drule parts_insert_subset_Un)
+apply (simp (no_asm_use))
+apply blast
+done
+
+(*H is sometimes (Key ` KK \<union> spies evs), so can't put G=H*)
+lemma Fake_analz_insert: "X\<in> synth (analz G) ==>
+ analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
+apply (rule subsetI)
+apply (subgoal_tac "x \<in> analz (synth (analz G) \<union> H) ")
+prefer 2 apply (blast intro: analz_mono [THEN [2] rev_subsetD] analz_mono [THEN synth_mono, THEN [2] rev_subsetD])
+apply (simp (no_asm_use))
+apply blast
+done
+
+lemma analz_conj_parts [simp]: "(X \<in> analz H & X \<in> parts H) = (X \<in> analz H)"
+by (blast intro: analz_subset_parts [THEN [2] rev_subsetD])
+
+lemma analz_disj_parts [simp]: "(X \<in> analz H | X \<in> parts H) = (X \<in> parts H)"
+by (blast intro: analz_subset_parts [THEN [2] rev_subsetD])
+
+(*Without this equation, other rules for synth and analz would yield
+ redundant cases*)
+lemma MPair_synth_analz [iff]:
+ "({|X,Y|} \<in> synth (analz H)) =
+ (X \<in> synth (analz H) & Y \<in> synth (analz H))"
+by blast
+
+lemma Crypt_synth_analz: "[| Key K \<in> analz H; Key (invKey K) \<in> analz H |]
+ ==> (Crypt K X \<in> synth (analz H)) = (X \<in> synth (analz H))"
+by blast
+
+
+lemma Hash_synth_analz [simp]: "X \<notin> synth (analz H)
+ ==> (Hash{|X,Y|} \<in> synth (analz H)) = (Hash{|X,Y|} \<in> analz H)"
+by blast
+
+
+subsection{*HPair: a combination of Hash and MPair*}
+
+(*** Freeness ***)
+
+lemma Agent_neq_HPair: "Agent A ~= Hash[X] Y"
+by (unfold HPair_def, simp)
+
+lemma Nonce_neq_HPair: "Nonce N ~= Hash[X] Y"
+by (unfold HPair_def, simp)
+
+lemma Number_neq_HPair: "Number N ~= Hash[X] Y"
+by (unfold HPair_def, simp)
+
+lemma Key_neq_HPair: "Key K ~= Hash[X] Y"
+by (unfold HPair_def, simp)
+
+lemma Hash_neq_HPair: "Hash Z ~= Hash[X] Y"
+by (unfold HPair_def, simp)
+
+lemma Crypt_neq_HPair: "Crypt K X' ~= Hash[X] Y"
+by (unfold HPair_def, simp)
+
+lemmas HPair_neqs = Agent_neq_HPair Nonce_neq_HPair Number_neq_HPair
+ Key_neq_HPair Hash_neq_HPair Crypt_neq_HPair
+
+declare HPair_neqs [iff]
+declare HPair_neqs [symmetric, iff]
+
+lemma HPair_eq [iff]: "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)"
+by (simp add: HPair_def)
+
+lemma MPair_eq_HPair [iff]: "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)"
+by (simp add: HPair_def)
+
+lemma HPair_eq_MPair [iff]: "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)"
+by (auto simp add: HPair_def)
+
+
+(*** Specialized laws, proved in terms of those for Hash and MPair ***)
+
+lemma keysFor_insert_HPair [simp]: "keysFor (insert (Hash[X] Y) H) = keysFor H"
+by (simp add: HPair_def)
+
+lemma parts_insert_HPair [simp]:
+ "parts (insert (Hash[X] Y) H) =
+ insert (Hash[X] Y) (insert (Hash{|X,Y|}) (parts (insert Y H)))"
+by (simp add: HPair_def)
+
+lemma analz_insert_HPair [simp]:
+ "analz (insert (Hash[X] Y) H) =
+ insert (Hash[X] Y) (insert (Hash{|X,Y|}) (analz (insert Y H)))"
+by (simp add: HPair_def)
+
+lemma HPair_synth_analz [simp]:
+ "X \<notin> synth (analz H)
+ ==> (Hash[X] Y \<in> synth (analz H)) =
+ (Hash {|X, Y|} \<in> analz H & Y \<in> synth (analz H))"
+by (simp add: HPair_def)
+
+
+(*We do NOT want Crypt... messages broken up in protocols!!*)
+declare parts.Body [rule del]
+
+
+ML
+{*
+(*ML bindings for definitions and axioms*)
+
+val invKey = thm "invKey"
+val keysFor_def = thm "keysFor_def"
+val HPair_def = thm "HPair_def"
+val symKeys_def = thm "symKeys_def"
+
+structure parts =
+ struct
+ val induct = thm "parts.induct"
+ val Inj = thm "parts.Inj"
+ val Fst = thm "parts.Fst"
+ val Snd = thm "parts.Snd"
+ val Body = thm "parts.Body"
+ end
+
+structure analz =
+ struct
+ val induct = thm "analz.induct"
+ val Inj = thm "analz.Inj"
+ val Fst = thm "analz.Fst"
+ val Snd = thm "analz.Snd"
+ val Decrypt = thm "analz.Decrypt"
+ end
+
+
+(** Rewrites to push in Key and Crypt messages, so that other messages can
+ be pulled out using the analz_insert rules **)
+
+fun insComm x y = inst "x" x (inst "y" y insert_commute);
+
+bind_thms ("pushKeys",
+ map (insComm "Key ?K")
+ ["Agent ?C", "Nonce ?N", "Number ?N",
+ "Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"]);
+
+bind_thms ("pushCrypts",
+ map (insComm "Crypt ?X ?K")
+ ["Agent ?C", "Nonce ?N", "Number ?N",
+ "Hash ?X'", "MPair ?X' ?Y"]);
+*}
+
+text{*Cannot be added with @{text "[simp]"} -- messages should not always be
+ re-ordered. *}
+lemmas pushes = pushKeys pushCrypts
+
+
+subsection{*Tactics useful for many protocol proofs*}
+ML
+{*
+val parts_mono = thm "parts_mono";
+val analz_mono = thm "analz_mono";
+val Key_image_eq = thm "Key_image_eq";
+val Nonce_Key_image_eq = thm "Nonce_Key_image_eq";
+val keysFor_Un = thm "keysFor_Un";
+val keysFor_mono = thm "keysFor_mono";
+val keysFor_image_Key = thm "keysFor_image_Key";
+val Crypt_imp_invKey_keysFor = thm "Crypt_imp_invKey_keysFor";
+val MPair_parts = thm "MPair_parts";
+val parts_increasing = thm "parts_increasing";
+val parts_insertI = thm "parts_insertI";
+val parts_empty = thm "parts_empty";
+val parts_emptyE = thm "parts_emptyE";
+val parts_singleton = thm "parts_singleton";
+val parts_Un_subset1 = thm "parts_Un_subset1";
+val parts_Un_subset2 = thm "parts_Un_subset2";
+val parts_insert = thm "parts_insert";
+val parts_insert2 = thm "parts_insert2";
+val parts_UN_subset1 = thm "parts_UN_subset1";
+val parts_UN_subset2 = thm "parts_UN_subset2";
+val parts_UN = thm "parts_UN";
+val parts_insert_subset = thm "parts_insert_subset";
+val parts_partsD = thm "parts_partsD";
+val parts_trans = thm "parts_trans";
+val parts_cut = thm "parts_cut";
+val parts_cut_eq = thm "parts_cut_eq";
+val parts_insert_eq_I = thm "parts_insert_eq_I";
+val parts_image_Key = thm "parts_image_Key";
+val MPair_analz = thm "MPair_analz";
+val analz_increasing = thm "analz_increasing";
+val analz_subset_parts = thm "analz_subset_parts";
+val not_parts_not_analz = thm "not_parts_not_analz";
+val parts_analz = thm "parts_analz";
+val analz_parts = thm "analz_parts";
+val analz_insertI = thm "analz_insertI";
+val analz_empty = thm "analz_empty";
+val analz_Un = thm "analz_Un";
+val analz_insert_Crypt_subset = thm "analz_insert_Crypt_subset";
+val analz_image_Key = thm "analz_image_Key";
+val analz_analzD = thm "analz_analzD";
+val analz_trans = thm "analz_trans";
+val analz_cut = thm "analz_cut";
+val analz_insert_eq = thm "analz_insert_eq";
+val analz_subset_cong = thm "analz_subset_cong";
+val analz_cong = thm "analz_cong";
+val analz_insert_cong = thm "analz_insert_cong";
+val analz_trivial = thm "analz_trivial";
+val analz_UN_analz = thm "analz_UN_analz";
+val synth_mono = thm "synth_mono";
+val synth_increasing = thm "synth_increasing";
+val synth_Un = thm "synth_Un";
+val synth_insert = thm "synth_insert";
+val synth_synthD = thm "synth_synthD";
+val synth_trans = thm "synth_trans";
+val synth_cut = thm "synth_cut";
+val Agent_synth = thm "Agent_synth";
+val Number_synth = thm "Number_synth";
+val Nonce_synth_eq = thm "Nonce_synth_eq";
+val Key_synth_eq = thm "Key_synth_eq";
+val Crypt_synth_eq = thm "Crypt_synth_eq";
+val keysFor_synth = thm "keysFor_synth";
+val parts_synth = thm "parts_synth";
+val analz_analz_Un = thm "analz_analz_Un";
+val analz_synth_Un = thm "analz_synth_Un";
+val analz_synth = thm "analz_synth";
+val parts_insert_subset_Un = thm "parts_insert_subset_Un";
+val Fake_parts_insert = thm "Fake_parts_insert";
+val Fake_analz_insert = thm "Fake_analz_insert";
+val analz_conj_parts = thm "analz_conj_parts";
+val analz_disj_parts = thm "analz_disj_parts";
+val MPair_synth_analz = thm "MPair_synth_analz";
+val Crypt_synth_analz = thm "Crypt_synth_analz";
+val Hash_synth_analz = thm "Hash_synth_analz";
+val pushes = thms "pushes";
+
+
+(*Prove base case (subgoal i) and simplify others. A typical base case
+ concerns Crypt K X \<notin> Key`shrK`bad and cannot be proved by rewriting
+ alone.*)
+fun prove_simple_subgoals_tac i =
+ force_tac (claset(), simpset() addsimps [image_eq_UN]) i THEN
+ ALLGOALS Asm_simp_tac
+
+(*Analysis of Fake cases. Also works for messages that forward unknown parts,
+ but this application is no longer necessary if analz_insert_eq is used.
+ Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
+ DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
+
+(*Apply rules to break down assumptions of the form
+ Y \<in> parts(insert X H) and Y \<in> analz(insert X H)
+*)
+val Fake_insert_tac =
+ dresolve_tac [impOfSubs Fake_analz_insert,
+ impOfSubs Fake_parts_insert] THEN'
+ eresolve_tac [asm_rl, thm"synth.Inj"];
+
+fun Fake_insert_simp_tac ss i =
+ REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
+
+fun atomic_spy_analz_tac (cs,ss) = SELECT_GOAL
+ (Fake_insert_simp_tac ss 1
+ THEN
+ IF_UNSOLVED (Blast.depth_tac
+ (cs addIs [analz_insertI,
+ impOfSubs analz_subset_parts]) 4 1))
+
+(*The explicit claset and simpset arguments help it work with Isar*)
+fun gen_spy_analz_tac (cs,ss) i =
+ DETERM
+ (SELECT_GOAL
+ (EVERY
+ [ (*push in occurrences of X...*)
+ (REPEAT o CHANGED)
+ (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
+ (*...allowing further simplifications*)
+ simp_tac ss 1,
+ REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
+ DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i)
+
+fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i
+*}
+
+(*By default only o_apply is built-in. But in the presence of eta-expansion
+ this means that some terms displayed as (f o g) will be rewritten, and others
+ will not!*)
+declare o_def [simp]
+
lemma Crypt_notin_image_Key [simp]: "Crypt K X \<notin> Key ` A"
by auto
@@ -174,7 +979,7 @@
done
lemma Fake_parts_sing:
- "X \<in> synth (analz H) ==> parts{X} \<subseteq> synth (analz H) Un parts H";
+ "X \<in> synth (analz H) ==> parts{X} \<subseteq> synth (analz H) \<union> parts H";
apply (rule subset_trans)
apply (erule_tac [2] Fake_parts_insert)
apply (simp add: parts_mono)
@@ -200,4 +1005,5 @@
Fake_insert_simp_tac (Simplifier.get_local_simpset ctxt) 1)) *}
"for debugging spy_analz"
+
end
--- a/src/HOL/Auth/Message_lemmas.ML Sat Apr 26 12:38:17 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,902 +0,0 @@
-(* Title: HOL/Auth/Message
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-
-Datatypes of agents and messages;
-Inductive relations "parts", "analz" and "synth"
-*)
-
-(*ML bindings for definitions and axioms*)
-val invKey = thm "invKey";
-val keysFor_def = thm "keysFor_def";
-val parts_mono = thm "parts_mono";
-val analz_mono = thm "analz_mono";
-val synth_mono = thm "synth_mono";
-val HPair_def = thm "HPair_def";
-val symKeys_def = thm "symKeys_def";
-
-structure parts =
- struct
- val induct = thm "parts.induct";
- val Inj = thm "parts.Inj";
- val Fst = thm "parts.Fst";
- val Snd = thm "parts.Snd";
- val Body = thm "parts.Body";
- end;
-
-structure analz =
- struct
- val induct = thm "analz.induct";
- val Inj = thm "analz.Inj";
- val Fst = thm "analz.Fst";
- val Snd = thm "analz.Snd";
- val Decrypt = thm "analz.Decrypt";
- end;
-
-structure synth =
- struct
- val induct = thm "synth.induct";
- val Inj = thm "synth.Inj";
- val Agent = thm "synth.Agent";
- val Number = thm "synth.Number";
- val Hash = thm "synth.Hash";
- val Crypt = thm "synth.Crypt";
- end;
-
-
-(*Equations hold because constructors are injective; cannot prove for all f*)
-Goal "(Friend x \\<in> Friend`A) = (x:A)";
-by Auto_tac;
-qed "Friend_image_eq";
-
-Goal "(Key x \\<in> Key`A) = (x\\<in>A)";
-by Auto_tac;
-qed "Key_image_eq";
-
-Goal "(Nonce x \\<notin> Key`A)";
-by Auto_tac;
-qed "Nonce_Key_image_eq";
-Addsimps [Friend_image_eq, Key_image_eq, Nonce_Key_image_eq];
-
-
-(** Inverse of keys **)
-
-Goal "(invKey K = invKey K') = (K=K')";
-by Safe_tac;
-by (rtac box_equals 1);
-by (REPEAT (rtac invKey 2));
-by (Asm_simp_tac 1);
-qed "invKey_eq";
-
-Addsimps [invKey_eq];
-
-
-(**** keysFor operator ****)
-
-Goalw [keysFor_def] "keysFor {} = {}";
-by (Blast_tac 1);
-qed "keysFor_empty";
-
-Goalw [keysFor_def] "keysFor (H Un H') = keysFor H Un keysFor H'";
-by (Blast_tac 1);
-qed "keysFor_Un";
-
-Goalw [keysFor_def] "keysFor (\\<Union>i\\<in>A. H i) = (\\<Union>i\\<in>A. keysFor (H i))";
-by (Blast_tac 1);
-qed "keysFor_UN";
-
-(*Monotonicity*)
-Goalw [keysFor_def] "G\\<subseteq>H ==> keysFor(G) \\<subseteq> keysFor(H)";
-by (Blast_tac 1);
-qed "keysFor_mono";
-
-Goalw [keysFor_def] "keysFor (insert (Agent A) H) = keysFor H";
-by Auto_tac;
-qed "keysFor_insert_Agent";
-
-Goalw [keysFor_def] "keysFor (insert (Nonce N) H) = keysFor H";
-by Auto_tac;
-qed "keysFor_insert_Nonce";
-
-Goalw [keysFor_def] "keysFor (insert (Number N) H) = keysFor H";
-by Auto_tac;
-qed "keysFor_insert_Number";
-
-Goalw [keysFor_def] "keysFor (insert (Key K) H) = keysFor H";
-by Auto_tac;
-qed "keysFor_insert_Key";
-
-Goalw [keysFor_def] "keysFor (insert (Hash X) H) = keysFor H";
-by Auto_tac;
-qed "keysFor_insert_Hash";
-
-Goalw [keysFor_def] "keysFor (insert {|X,Y|} H) = keysFor H";
-by Auto_tac;
-qed "keysFor_insert_MPair";
-
-Goalw [keysFor_def]
- "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)";
-by Auto_tac;
-qed "keysFor_insert_Crypt";
-
-Addsimps [keysFor_empty, keysFor_Un, keysFor_UN,
- keysFor_insert_Agent, keysFor_insert_Nonce,
- keysFor_insert_Number, keysFor_insert_Key,
- keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt];
-AddSEs [keysFor_Un RS equalityD1 RS subsetD RS UnE,
- keysFor_UN RS equalityD1 RS subsetD RS UN_E];
-
-Goalw [keysFor_def] "keysFor (Key`E) = {}";
-by Auto_tac;
-qed "keysFor_image_Key";
-Addsimps [keysFor_image_Key];
-
-Goalw [keysFor_def] "Crypt K X \\<in> H ==> invKey K \\<in> keysFor H";
-by (Blast_tac 1);
-qed "Crypt_imp_invKey_keysFor";
-
-
-(**** Inductive relation "parts" ****)
-
-val major::prems =
-Goal "[| {|X,Y|} \\<in> parts H; \
-\ [| X \\<in> parts H; Y \\<in> parts H |] ==> P \
-\ |] ==> P";
-by (cut_facts_tac [major] 1);
-by (resolve_tac prems 1);
-by (REPEAT (eresolve_tac [asm_rl, parts.Fst, parts.Snd] 1));
-qed "MPair_parts";
-
-AddSEs [MPair_parts, make_elim parts.Body];
-(*NB These two rules are UNSAFE in the formal sense, as they discard the
- compound message. They work well on THIS FILE.
- MPair_parts is left as SAFE because it speeds up proofs.
- The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*)
-
-Goal "H \\<subseteq> parts(H)";
-by (Blast_tac 1);
-qed "parts_increasing";
-
-bind_thm ("parts_insertI", impOfSubs (subset_insertI RS parts_mono));
-
-Goal "parts{} = {}";
-by Safe_tac;
-by (etac parts.induct 1);
-by (ALLGOALS Blast_tac);
-qed "parts_empty";
-Addsimps [parts_empty];
-
-Goal "X\\<in> parts{} ==> P";
-by (Asm_full_simp_tac 1);
-qed "parts_emptyE";
-AddSEs [parts_emptyE];
-
-(*WARNING: loops if H = {Y}, therefore must not be repeated!*)
-Goal "X\\<in> parts H ==> \\<exists>Y\\<in>H. X\\<in> parts {Y}";
-by (etac parts.induct 1);
-by (ALLGOALS Blast_tac);
-qed "parts_singleton";
-
-
-(** Unions **)
-
-Goal "parts(G) Un parts(H) \\<subseteq> parts(G Un H)";
-by (REPEAT (ares_tac [Un_least, parts_mono, Un_upper1, Un_upper2] 1));
-val parts_Un_subset1 = result();
-
-Goal "parts(G Un H) \\<subseteq> parts(G) Un parts(H)";
-by (rtac subsetI 1);
-by (etac parts.induct 1);
-by (ALLGOALS Blast_tac);
-val parts_Un_subset2 = result();
-
-Goal "parts(G Un H) = parts(G) Un parts(H)";
-by (REPEAT (ares_tac [equalityI, parts_Un_subset1, parts_Un_subset2] 1));
-qed "parts_Un";
-
-Goal "parts (insert X H) = parts {X} Un parts H";
-by (stac (read_instantiate [("A","H")] insert_is_Un) 1);
-by (simp_tac (HOL_ss addsimps [parts_Un]) 1);
-qed "parts_insert";
-
-(*TWO inserts to avoid looping. This rewrite is better than nothing.
- Not suitable for Addsimps: its behaviour can be strange.*)
-Goal "parts (insert X (insert Y H)) = parts {X} Un parts {Y} Un parts H";
-by (simp_tac (simpset() addsimps [Un_assoc]) 1);
-by (simp_tac (simpset() addsimps [parts_insert RS sym]) 1);
-qed "parts_insert2";
-
-Goal "(\\<Union>x\\<in>A. parts(H x)) \\<subseteq> parts(\\<Union>x\\<in>A. H x)";
-by (REPEAT (ares_tac [UN_least, parts_mono, UN_upper] 1));
-val parts_UN_subset1 = result();
-
-Goal "parts(\\<Union>x\\<in>A. H x) \\<subseteq> (\\<Union>x\\<in>A. parts(H x))";
-by (rtac subsetI 1);
-by (etac parts.induct 1);
-by (ALLGOALS Blast_tac);
-val parts_UN_subset2 = result();
-
-Goal "parts(\\<Union>x\\<in>A. H x) = (\\<Union>x\\<in>A. parts(H x))";
-by (REPEAT (ares_tac [equalityI, parts_UN_subset1, parts_UN_subset2] 1));
-qed "parts_UN";
-
-(*Added to simplify arguments to parts, analz and synth.
- NOTE: the UN versions are no longer used!*)
-Addsimps [parts_Un, parts_UN];
-AddSEs [parts_Un RS equalityD1 RS subsetD RS UnE,
- parts_UN RS equalityD1 RS subsetD RS UN_E];
-
-Goal "insert X (parts H) \\<subseteq> parts(insert X H)";
-by (blast_tac (claset() addIs [impOfSubs parts_mono]) 1);
-qed "parts_insert_subset";
-
-(** Idempotence and transitivity **)
-
-Goal "X\\<in> parts (parts H) ==> X\\<in> parts H";
-by (etac parts.induct 1);
-by (ALLGOALS Blast_tac);
-qed "parts_partsD";
-AddSDs [parts_partsD];
-
-Goal "parts (parts H) = parts H";
-by (Blast_tac 1);
-qed "parts_idem";
-Addsimps [parts_idem];
-
-Goal "[| X\\<in> parts G; G \\<subseteq> parts H |] ==> X\\<in> parts H";
-by (dtac parts_mono 1);
-by (Blast_tac 1);
-qed "parts_trans";
-
-(*Cut*)
-Goal "[| Y\\<in> parts (insert X G); X\\<in> parts H |] \
-\ ==> Y\\<in> parts (G Un H)";
-by (etac parts_trans 1);
-by Auto_tac;
-qed "parts_cut";
-
-Goal "X\\<in> parts H ==> parts (insert X H) = parts H";
-by (fast_tac (claset() addSDs [parts_cut]
- addIs [parts_insertI]
- addss (simpset())) 1);
-qed "parts_cut_eq";
-
-Addsimps [parts_cut_eq];
-
-
-(** Rewrite rules for pulling out atomic messages **)
-
-fun parts_tac i =
- EVERY [rtac ([subsetI, parts_insert_subset] MRS equalityI) i,
- etac parts.induct i,
- Auto_tac];
-
-Goal "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)";
-by (parts_tac 1);
-qed "parts_insert_Agent";
-
-Goal "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)";
-by (parts_tac 1);
-qed "parts_insert_Nonce";
-
-Goal "parts (insert (Number N) H) = insert (Number N) (parts H)";
-by (parts_tac 1);
-qed "parts_insert_Number";
-
-Goal "parts (insert (Key K) H) = insert (Key K) (parts H)";
-by (parts_tac 1);
-qed "parts_insert_Key";
-
-Goal "parts (insert (Hash X) H) = insert (Hash X) (parts H)";
-by (parts_tac 1);
-qed "parts_insert_Hash";
-
-Goal "parts (insert (Crypt K X) H) = \
-\ insert (Crypt K X) (parts (insert X H))";
-by (rtac equalityI 1);
-by (rtac subsetI 1);
-by (etac parts.induct 1);
-by Auto_tac;
-by (etac parts.induct 1);
-by (ALLGOALS (blast_tac (claset() addIs [parts.Body])));
-qed "parts_insert_Crypt";
-
-Goal "parts (insert {|X,Y|} H) = \
-\ insert {|X,Y|} (parts (insert X (insert Y H)))";
-by (rtac equalityI 1);
-by (rtac subsetI 1);
-by (etac parts.induct 1);
-by Auto_tac;
-by (etac parts.induct 1);
-by (ALLGOALS (blast_tac (claset() addIs [parts.Fst, parts.Snd])));
-qed "parts_insert_MPair";
-
-Addsimps [parts_insert_Agent, parts_insert_Nonce,
- parts_insert_Number, parts_insert_Key,
- parts_insert_Hash, parts_insert_Crypt, parts_insert_MPair];
-
-
-Goal "parts (Key`N) = Key`N";
-by Auto_tac;
-by (etac parts.induct 1);
-by Auto_tac;
-qed "parts_image_Key";
-Addsimps [parts_image_Key];
-
-
-(*In any message, there is an upper bound N on its greatest nonce.*)
-Goal "\\<exists>N. \\<forall>n. N\\<le>n --> Nonce n \\<notin> parts {msg}";
-by (induct_tac "msg" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [exI, parts_insert2])));
-(*MPair case: blast_tac works out the necessary sum itself!*)
-by (blast_tac (claset() addSEs [add_leE]) 2);
-(*Nonce case*)
-by (res_inst_tac [("x","N + Suc nat")] exI 1);
-by (auto_tac (claset() addSEs [add_leE], simpset()));
-qed "msg_Nonce_supply";
-
-
-(**** Inductive relation "analz" ****)
-
-val major::prems =
-Goal "[| {|X,Y|} \\<in> analz H; \
-\ [| X \\<in> analz H; Y \\<in> analz H |] ==> P \
-\ |] ==> P";
-by (cut_facts_tac [major] 1);
-by (resolve_tac prems 1);
-by (REPEAT (eresolve_tac [asm_rl, analz.Fst, analz.Snd] 1));
-qed "MPair_analz";
-
-AddSEs [MPair_analz]; (*Making it safe speeds up proofs*)
-
-Goal "H \\<subseteq> analz(H)";
-by (Blast_tac 1);
-qed "analz_increasing";
-
-Goal "analz H \\<subseteq> parts H";
-by (rtac subsetI 1);
-by (etac analz.induct 1);
-by (ALLGOALS Blast_tac);
-qed "analz_subset_parts";
-
-bind_thm ("not_parts_not_analz", analz_subset_parts RS contra_subsetD);
-
-
-Goal "parts (analz H) = parts H";
-by (rtac equalityI 1);
-by (rtac (analz_subset_parts RS parts_mono RS subset_trans) 1);
-by (Simp_tac 1);
-by (blast_tac (claset() addIs [analz_increasing RS parts_mono RS subsetD]) 1);
-qed "parts_analz";
-Addsimps [parts_analz];
-
-Goal "analz (parts H) = parts H";
-by Auto_tac;
-by (etac analz.induct 1);
-by Auto_tac;
-qed "analz_parts";
-Addsimps [analz_parts];
-
-bind_thm ("analz_insertI", impOfSubs (subset_insertI RS analz_mono));
-
-(** General equational properties **)
-
-Goal "analz{} = {}";
-by Safe_tac;
-by (etac analz.induct 1);
-by (ALLGOALS Blast_tac);
-qed "analz_empty";
-Addsimps [analz_empty];
-
-(*Converse fails: we can analz more from the union than from the
- separate parts, as a key in one might decrypt a message in the other*)
-Goal "analz(G) Un analz(H) \\<subseteq> analz(G Un H)";
-by (REPEAT (ares_tac [Un_least, analz_mono, Un_upper1, Un_upper2] 1));
-qed "analz_Un";
-
-Goal "insert X (analz H) \\<subseteq> analz(insert X H)";
-by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
-qed "analz_insert";
-
-(** Rewrite rules for pulling out atomic messages **)
-
-fun analz_tac i =
- EVERY [rtac ([subsetI, analz_insert] MRS equalityI) i,
- etac analz.induct i,
- Auto_tac];
-
-Goal "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)";
-by (analz_tac 1);
-qed "analz_insert_Agent";
-
-Goal "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)";
-by (analz_tac 1);
-qed "analz_insert_Nonce";
-
-Goal "analz (insert (Number N) H) = insert (Number N) (analz H)";
-by (analz_tac 1);
-qed "analz_insert_Number";
-
-Goal "analz (insert (Hash X) H) = insert (Hash X) (analz H)";
-by (analz_tac 1);
-qed "analz_insert_Hash";
-
-(*Can only pull out Keys if they are not needed to decrypt the rest*)
-Goalw [keysFor_def]
- "K \\<notin> keysFor (analz H) ==> \
-\ analz (insert (Key K) H) = insert (Key K) (analz H)";
-by (analz_tac 1);
-qed "analz_insert_Key";
-
-Goal "analz (insert {|X,Y|} H) = \
-\ insert {|X,Y|} (analz (insert X (insert Y H)))";
-by (rtac equalityI 1);
-by (rtac subsetI 1);
-by (etac analz.induct 1);
-by Auto_tac;
-by (etac analz.induct 1);
-by (ALLGOALS (blast_tac (claset() addIs [analz.Fst, analz.Snd])));
-qed "analz_insert_MPair";
-
-(*Can pull out enCrypted message if the Key is not known*)
-Goal "Key (invKey K) \\<notin> analz H ==> \
-\ analz (insert (Crypt K X) H) = \
-\ insert (Crypt K X) (analz H)";
-by (analz_tac 1);
-qed "analz_insert_Crypt";
-
-Goal "Key (invKey K) \\<in> analz H ==> \
-\ analz (insert (Crypt K X) H) \\<subseteq> \
-\ insert (Crypt K X) (analz (insert X H))";
-by (rtac subsetI 1);
-by (eres_inst_tac [("xa","x")] analz.induct 1);
-by Auto_tac;
-val lemma1 = result();
-
-Goal "Key (invKey K) \\<in> analz H ==> \
-\ insert (Crypt K X) (analz (insert X H)) \\<subseteq> \
-\ analz (insert (Crypt K X) H)";
-by Auto_tac;
-by (eres_inst_tac [("xa","x")] analz.induct 1);
-by Auto_tac;
-by (blast_tac (claset() addIs [analz_insertI, analz.Decrypt]) 1);
-val lemma2 = result();
-
-Goal "Key (invKey K) \\<in> analz H ==> \
-\ analz (insert (Crypt K X) H) = \
-\ insert (Crypt K X) (analz (insert X H))";
-by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1));
-qed "analz_insert_Decrypt";
-
-(*Case analysis: either the message is secure, or it is not!
- Effective, but can cause subgoals to blow up!
- Use with split_if; apparently split_tac does not cope with patterns
- such as "analz (insert (Crypt K X) H)" *)
-Goal "analz (insert (Crypt K X) H) = \
-\ (if (Key (invKey K) \\<in> analz H) \
-\ then insert (Crypt K X) (analz (insert X H)) \
-\ else insert (Crypt K X) (analz H))";
-by (case_tac "Key (invKey K) \\<in> analz H " 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [analz_insert_Crypt,
- analz_insert_Decrypt])));
-qed "analz_Crypt_if";
-
-Addsimps [analz_insert_Agent, analz_insert_Nonce,
- analz_insert_Number, analz_insert_Key,
- analz_insert_Hash, analz_insert_MPair, analz_Crypt_if];
-
-(*This rule supposes "for the sake of argument" that we have the key.*)
-Goal "analz (insert (Crypt K X) H) \\<subseteq> \
-\ insert (Crypt K X) (analz (insert X H))";
-by (rtac subsetI 1);
-by (etac analz.induct 1);
-by Auto_tac;
-qed "analz_insert_Crypt_subset";
-
-
-Goal "analz (Key`N) = Key`N";
-by Auto_tac;
-by (etac analz.induct 1);
-by Auto_tac;
-qed "analz_image_Key";
-
-Addsimps [analz_image_Key];
-
-
-(** Idempotence and transitivity **)
-
-Goal "X\\<in> analz (analz H) ==> X\\<in> analz H";
-by (etac analz.induct 1);
-by (ALLGOALS Blast_tac);
-qed "analz_analzD";
-AddSDs [analz_analzD];
-
-Goal "analz (analz H) = analz H";
-by (Blast_tac 1);
-qed "analz_idem";
-Addsimps [analz_idem];
-
-Goal "[| X\\<in> analz G; G \\<subseteq> analz H |] ==> X\\<in> analz H";
-by (dtac analz_mono 1);
-by (Blast_tac 1);
-qed "analz_trans";
-
-(*Cut; Lemma 2 of Lowe*)
-Goal "[| Y\\<in> analz (insert X H); X\\<in> analz H |] ==> Y\\<in> analz H";
-by (etac analz_trans 1);
-by (Blast_tac 1);
-qed "analz_cut";
-
-(*Cut can be proved easily by induction on
- "Y: analz (insert X H) ==> X: analz H --> Y: analz H"
-*)
-
-(*This rewrite rule helps in the simplification of messages that involve
- the forwarding of unknown components (X). Without it, removing occurrences
- of X can be very complicated. *)
-Goal "X\\<in> analz H ==> analz (insert X H) = analz H";
-by (blast_tac (claset() addIs [analz_cut, analz_insertI]) 1);
-qed "analz_insert_eq";
-
-
-(** A congruence rule for "analz" **)
-
-Goal "[| analz G \\<subseteq> analz G'; analz H \\<subseteq> analz H' \
-\ |] ==> analz (G Un H) \\<subseteq> analz (G' Un H')";
-by (Clarify_tac 1);
-by (etac analz.induct 1);
-by (ALLGOALS (best_tac (claset() addIs [analz_mono RS subsetD])));
-qed "analz_subset_cong";
-
-Goal "[| analz G = analz G'; analz H = analz H' \
-\ |] ==> analz (G Un H) = analz (G' Un H')";
-by (REPEAT_FIRST (ares_tac [equalityI, analz_subset_cong]
- ORELSE' etac equalityE));
-qed "analz_cong";
-
-
-Goal "analz H = analz H' ==> analz(insert X H) = analz(insert X H')";
-by (asm_simp_tac (simpset() addsimps [insert_def] delsimps [singleton_conv]
- setloop (rtac analz_cong)) 1);
-qed "analz_insert_cong";
-
-(*If there are no pairs or encryptions then analz does nothing*)
-Goal "[| \\<forall>X Y. {|X,Y|} \\<notin> H; \\<forall>X K. Crypt K X \\<notin> H |] ==> analz H = H";
-by Safe_tac;
-by (etac analz.induct 1);
-by (ALLGOALS Blast_tac);
-qed "analz_trivial";
-
-(*These two are obsolete (with a single Spy) but cost little to prove...*)
-Goal "X\\<in> analz (\\<Union>i\\<in>A. analz (H i)) ==> X\\<in> analz (\\<Union>i\\<in>A. H i)";
-by (etac analz.induct 1);
-by (ALLGOALS (blast_tac (claset() addIs [impOfSubs analz_mono])));
-val lemma = result();
-
-Goal "analz (\\<Union>i\\<in>A. analz (H i)) = analz (\\<Union>i\\<in>A. H i)";
-by (blast_tac (claset() addIs [lemma, impOfSubs analz_mono]) 1);
-qed "analz_UN_analz";
-Addsimps [analz_UN_analz];
-
-
-(**** Inductive relation "synth" ****)
-
-Goal "H \\<subseteq> synth(H)";
-by (Blast_tac 1);
-qed "synth_increasing";
-
-(** Unions **)
-
-(*Converse fails: we can synth more from the union than from the
- separate parts, building a compound message using elements of each.*)
-Goal "synth(G) Un synth(H) \\<subseteq> synth(G Un H)";
-by (REPEAT (ares_tac [Un_least, synth_mono, Un_upper1, Un_upper2] 1));
-qed "synth_Un";
-
-Goal "insert X (synth H) \\<subseteq> synth(insert X H)";
-by (blast_tac (claset() addIs [impOfSubs synth_mono]) 1);
-qed "synth_insert";
-
-(** Idempotence and transitivity **)
-
-Goal "X\\<in> synth (synth H) ==> X\\<in> synth H";
-by (etac synth.induct 1);
-by (ALLGOALS Blast_tac);
-qed "synth_synthD";
-AddSDs [synth_synthD];
-
-Goal "synth (synth H) = synth H";
-by (Blast_tac 1);
-qed "synth_idem";
-
-Goal "[| X\\<in> synth G; G \\<subseteq> synth H |] ==> X\\<in> synth H";
-by (dtac synth_mono 1);
-by (Blast_tac 1);
-qed "synth_trans";
-
-(*Cut; Lemma 2 of Lowe*)
-Goal "[| Y\\<in> synth (insert X H); X\\<in> synth H |] ==> Y\\<in> synth H";
-by (etac synth_trans 1);
-by (Blast_tac 1);
-qed "synth_cut";
-
-Goal "Agent A \\<in> synth H";
-by (Blast_tac 1);
-qed "Agent_synth";
-
-Goal "Number n \\<in> synth H";
-by (Blast_tac 1);
-qed "Number_synth";
-
-Goal "(Nonce N \\<in> synth H) = (Nonce N \\<in> H)";
-by (Blast_tac 1);
-qed "Nonce_synth_eq";
-
-Goal "(Key K \\<in> synth H) = (Key K \\<in> H)";
-by (Blast_tac 1);
-qed "Key_synth_eq";
-
-Goal "Key K \\<notin> H ==> (Crypt K X \\<in> synth H) = (Crypt K X \\<in> H)";
-by (Blast_tac 1);
-qed "Crypt_synth_eq";
-
-Addsimps [Agent_synth, Number_synth,
- Nonce_synth_eq, Key_synth_eq, Crypt_synth_eq];
-
-
-Goalw [keysFor_def]
- "keysFor (synth H) = keysFor H Un invKey`{K. Key K \\<in> H}";
-by (Blast_tac 1);
-qed "keysFor_synth";
-Addsimps [keysFor_synth];
-
-
-(*** Combinations of parts, analz and synth ***)
-
-Goal "parts (synth H) = parts H Un synth H";
-by (rtac equalityI 1);
-by (rtac subsetI 1);
-by (etac parts.induct 1);
-by (ALLGOALS
- (blast_tac (claset() addIs [synth_increasing RS parts_mono RS subsetD,
- parts.Fst, parts.Snd, parts.Body])));
-qed "parts_synth";
-Addsimps [parts_synth];
-
-Goal "analz (analz G Un H) = analz (G Un H)";
-by (REPEAT_FIRST (resolve_tac [equalityI, analz_subset_cong]));
-by (ALLGOALS Simp_tac);
-qed "analz_analz_Un";
-
-Goal "analz (synth G Un H) = analz (G Un H) Un synth G";
-by (rtac equalityI 1);
-by (rtac subsetI 1);
-by (etac analz.induct 1);
-by (blast_tac (claset() addIs [impOfSubs analz_mono]) 5);
-by (ALLGOALS
- (blast_tac (claset() addIs [analz.Fst, analz.Snd, analz.Decrypt])));
-qed "analz_synth_Un";
-
-Goal "analz (synth H) = analz H Un synth H";
-by (cut_inst_tac [("H","{}")] analz_synth_Un 1);
-by (Full_simp_tac 1);
-qed "analz_synth";
-Addsimps [analz_analz_Un, analz_synth_Un, analz_synth];
-
-
-(** For reasoning about the Fake rule in traces **)
-
-Goal "X\\<in> G ==> parts(insert X H) \\<subseteq> parts G Un parts H";
-by (rtac ([parts_mono, parts_Un_subset2] MRS subset_trans) 1);
-by (Blast_tac 1);
-qed "parts_insert_subset_Un";
-
-(*More specifically for Fake. Very occasionally we could do with a version
- of the form parts{X} \\<subseteq> synth (analz H) Un parts H *)
-Goal "X\\<in> synth (analz H) ==> \
-\ parts (insert X H) \\<subseteq> synth (analz H) Un parts H";
-by (dtac parts_insert_subset_Un 1);
-by (Full_simp_tac 1);
-by (Blast_tac 1);
-qed "Fake_parts_insert";
-
-(*H is sometimes (Key ` KK Un spies evs), so can't put G=H*)
-Goal "X\\<in> synth (analz G) ==> \
-\ analz (insert X H) \\<subseteq> synth (analz G) Un analz (G Un H)";
-by (rtac subsetI 1);
-by (subgoal_tac "x \\<in> analz (synth (analz G) Un H)" 1);
-by (blast_tac (claset() addIs [impOfSubs analz_mono,
- impOfSubs (analz_mono RS synth_mono)]) 2);
-by (Full_simp_tac 1);
-by (Blast_tac 1);
-qed "Fake_analz_insert";
-
-Goal "(X\\<in> analz H & X\\<in> parts H) = (X\\<in> analz H)";
-by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1);
-val analz_conj_parts = result();
-
-Goal "(X\\<in> analz H | X\\<in> parts H) = (X\\<in> parts H)";
-by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1);
-val analz_disj_parts = result();
-
-AddIffs [analz_conj_parts, analz_disj_parts];
-
-(*Without this equation, other rules for synth and analz would yield
- redundant cases*)
-Goal "({|X,Y|} \\<in> synth (analz H)) = \
-\ (X \\<in> synth (analz H) & Y \\<in> synth (analz H))";
-by (Blast_tac 1);
-qed "MPair_synth_analz";
-
-AddIffs [MPair_synth_analz];
-
-Goal "[| Key K \\<in> analz H; Key (invKey K) \\<in> analz H |] \
-\ ==> (Crypt K X \\<in> synth (analz H)) = (X \\<in> synth (analz H))";
-by (Blast_tac 1);
-qed "Crypt_synth_analz";
-
-
-Goal "X \\<notin> synth (analz H) \
-\ ==> (Hash{|X,Y|} \\<in> synth (analz H)) = (Hash{|X,Y|} \\<in> analz H)";
-by (Blast_tac 1);
-qed "Hash_synth_analz";
-Addsimps [Hash_synth_analz];
-
-
-(**** HPair: a combination of Hash and MPair ****)
-
-(*** Freeness ***)
-
-Goalw [HPair_def] "Agent A ~= Hash[X] Y";
-by (Simp_tac 1);
-qed "Agent_neq_HPair";
-
-Goalw [HPair_def] "Nonce N ~= Hash[X] Y";
-by (Simp_tac 1);
-qed "Nonce_neq_HPair";
-
-Goalw [HPair_def] "Number N ~= Hash[X] Y";
-by (Simp_tac 1);
-qed "Number_neq_HPair";
-
-Goalw [HPair_def] "Key K ~= Hash[X] Y";
-by (Simp_tac 1);
-qed "Key_neq_HPair";
-
-Goalw [HPair_def] "Hash Z ~= Hash[X] Y";
-by (Simp_tac 1);
-qed "Hash_neq_HPair";
-
-Goalw [HPair_def] "Crypt K X' ~= Hash[X] Y";
-by (Simp_tac 1);
-qed "Crypt_neq_HPair";
-
-val HPair_neqs = [Agent_neq_HPair, Nonce_neq_HPair, Number_neq_HPair,
- Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair];
-
-AddIffs HPair_neqs;
-AddIffs (HPair_neqs RL [not_sym]);
-
-Goalw [HPair_def] "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)";
-by (Simp_tac 1);
-qed "HPair_eq";
-
-Goalw [HPair_def] "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)";
-by (Simp_tac 1);
-qed "MPair_eq_HPair";
-
-Goalw [HPair_def] "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)";
-by Auto_tac;
-qed "HPair_eq_MPair";
-
-AddIffs [HPair_eq, MPair_eq_HPair, HPair_eq_MPair];
-
-
-(*** Specialized laws, proved in terms of those for Hash and MPair ***)
-
-Goalw [HPair_def] "keysFor (insert (Hash[X] Y) H) = keysFor H";
-by (Simp_tac 1);
-qed "keysFor_insert_HPair";
-
-Goalw [HPair_def]
- "parts (insert (Hash[X] Y) H) = \
-\ insert (Hash[X] Y) (insert (Hash{|X,Y|}) (parts (insert Y H)))";
-by (Simp_tac 1);
-qed "parts_insert_HPair";
-
-Goalw [HPair_def]
- "analz (insert (Hash[X] Y) H) = \
-\ insert (Hash[X] Y) (insert (Hash{|X,Y|}) (analz (insert Y H)))";
-by (Simp_tac 1);
-qed "analz_insert_HPair";
-
-Goalw [HPair_def] "X \\<notin> synth (analz H) \
-\ ==> (Hash[X] Y \\<in> synth (analz H)) = \
-\ (Hash {|X, Y|} \\<in> analz H & Y \\<in> synth (analz H))";
-by (Simp_tac 1);
-by (Blast_tac 1);
-qed "HPair_synth_analz";
-
-Addsimps [keysFor_insert_HPair, parts_insert_HPair, analz_insert_HPair,
- HPair_synth_analz, HPair_synth_analz];
-
-
-(*We do NOT want Crypt... messages broken up in protocols!!*)
-Delrules [make_elim parts.Body];
-
-
-(** Rewrites to push in Key and Crypt messages, so that other messages can
- be pulled out using the analz_insert rules **)
-
-fun insComm x y = inst "x" x (inst "y" y insert_commute);
-
-val pushKeys = map (insComm "Key ?K")
- ["Agent ?C", "Nonce ?N", "Number ?N",
- "Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"];
-
-val pushCrypts = map (insComm "Crypt ?X ?K")
- ["Agent ?C", "Nonce ?N", "Number ?N",
- "Hash ?X'", "MPair ?X' ?Y"];
-
-(*Cannot be added with Addsimps -- we don't always want to re-order messages*)
-bind_thms ("pushes", pushKeys@pushCrypts);
-
-
-(*** Tactics useful for many protocol proofs ***)
-
-(*Prove base case (subgoal i) and simplify others. A typical base case
- concerns Crypt K X \\<notin> Key`shrK`bad and cannot be proved by rewriting
- alone.*)
-fun prove_simple_subgoals_tac i =
- force_tac (claset(), simpset() addsimps [image_eq_UN]) i THEN
- ALLGOALS Asm_simp_tac;
-
-fun Fake_parts_insert_tac i =
- blast_tac (claset() addIs [parts_insertI]
- addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]) i;
-
-(*Apply rules to break down assumptions of the form
- Y \\<in> parts(insert X H) and Y \\<in> analz(insert X H)
-*)
-val Fake_insert_tac =
- dresolve_tac [impOfSubs Fake_analz_insert,
- impOfSubs Fake_parts_insert] THEN'
- eresolve_tac [asm_rl, synth.Inj];
-
-fun Fake_insert_simp_tac ss i =
- REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
-
-
-(*Analysis of Fake cases. Also works for messages that forward unknown parts,
- but this application is no longer necessary if analz_insert_eq is used.
- Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
- DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
-
-fun atomic_spy_analz_tac (cs,ss) = SELECT_GOAL
- (Fake_insert_simp_tac ss 1
- THEN
- IF_UNSOLVED (Blast.depth_tac
- (cs addIs [analz_insertI,
- impOfSubs analz_subset_parts]) 4 1));
-
-(*The explicit claset and simpset arguments help it work with Isar*)
-fun gen_spy_analz_tac (cs,ss) i =
- DETERM
- (SELECT_GOAL
- (EVERY
- [ (*push in occurrences of X...*)
- (REPEAT o CHANGED)
- (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
- (*...allowing further simplifications*)
- simp_tac ss 1,
- REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
- DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i);
-
-fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i;
-
-(*By default only o_apply is built-in. But in the presence of eta-expansion
- this means that some terms displayed as (f o g) will be rewritten, and others
- will not!*)
-Addsimps [o_def];
--- a/src/HOL/Auth/NS_Public.thy Sat Apr 26 12:38:17 2003 +0200
+++ b/src/HOL/Auth/NS_Public.thy Sat Apr 26 12:38:42 2003 +0200
@@ -50,7 +50,8 @@
apply (intro exI bexI)
apply (rule_tac [2] ns_public.Nil [THEN ns_public.NS1, THEN ns_public.NS2,
THEN ns_public.NS3])
-by possibility
+apply possibility
+done
(**** Inductive proofs about ns_public ****)
--- a/src/HOL/Auth/NS_Shared.thy Sat Apr 26 12:38:17 2003 +0200
+++ b/src/HOL/Auth/NS_Shared.thy Sat Apr 26 12:38:42 2003 +0200
@@ -16,60 +16,60 @@
inductive "ns_shared"
intros
(*Initial trace is empty*)
- Nil: "[] \\<in> ns_shared"
+ Nil: "[] \<in> ns_shared"
(*The spy MAY say anything he CAN say. We do not expect him to
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
- Fake: "\\<lbrakk>evsf \\<in> ns_shared; X \\<in> synth (analz (spies evsf))\\<rbrakk>
- \\<Longrightarrow> Says Spy B X # evsf \\<in> ns_shared"
+ Fake: "\<lbrakk>evsf \<in> ns_shared; X \<in> synth (analz (spies evsf))\<rbrakk>
+ \<Longrightarrow> Says Spy B X # evsf \<in> ns_shared"
(*Alice initiates a protocol run, requesting to talk to any B*)
- NS1: "\\<lbrakk>evs1 \\<in> ns_shared; Nonce NA \\<notin> used evs1\\<rbrakk>
- \\<Longrightarrow> Says A Server \\<lbrace>Agent A, Agent B, Nonce NA\\<rbrace> # evs1 \\<in> ns_shared"
+ NS1: "\<lbrakk>evs1 \<in> ns_shared; Nonce NA \<notin> used evs1\<rbrakk>
+ \<Longrightarrow> Says A Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> # evs1 \<in> ns_shared"
(*Server's response to Alice's message.
!! It may respond more than once to A's request !!
Server doesn't know who the true sender is, hence the A' in
the sender field.*)
- NS2: "\\<lbrakk>evs2 \\<in> ns_shared; Key KAB \\<notin> used evs2;
- Says A' Server \\<lbrace>Agent A, Agent B, Nonce NA\\<rbrace> \\<in> set evs2\\<rbrakk>
- \\<Longrightarrow> Says Server A
+ NS2: "\<lbrakk>evs2 \<in> ns_shared; Key KAB \<notin> used evs2;
+ Says A' Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in> set evs2\<rbrakk>
+ \<Longrightarrow> Says Server A
(Crypt (shrK A)
- \\<lbrace>Nonce NA, Agent B, Key KAB,
- (Crypt (shrK B) \\<lbrace>Key KAB, Agent A\\<rbrace>)\\<rbrace>)
- # evs2 \\<in> ns_shared"
+ \<lbrace>Nonce NA, Agent B, Key KAB,
+ (Crypt (shrK B) \<lbrace>Key KAB, Agent A\<rbrace>)\<rbrace>)
+ # evs2 \<in> ns_shared"
(*We can't assume S=Server. Agent A "remembers" her nonce.
- Need A \\<noteq> Server because we allow messages to self.*)
- NS3: "\\<lbrakk>evs3 \\<in> ns_shared; A \\<noteq> Server;
- Says S A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs3;
- Says A Server \\<lbrace>Agent A, Agent B, Nonce NA\\<rbrace> \\<in> set evs3\\<rbrakk>
- \\<Longrightarrow> Says A B X # evs3 \\<in> ns_shared"
+ Need A \<noteq> Server because we allow messages to self.*)
+ NS3: "\<lbrakk>evs3 \<in> ns_shared; A \<noteq> Server;
+ Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs3;
+ Says A Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in> set evs3\<rbrakk>
+ \<Longrightarrow> Says A B X # evs3 \<in> ns_shared"
(*Bob's nonce exchange. He does not know who the message came
from, but responds to A because she is mentioned inside.*)
- NS4: "\\<lbrakk>evs4 \\<in> ns_shared; Nonce NB \\<notin> used evs4;
- Says A' B (Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>) \\<in> set evs4\\<rbrakk>
- \\<Longrightarrow> Says B A (Crypt K (Nonce NB)) # evs4 \\<in> ns_shared"
+ NS4: "\<lbrakk>evs4 \<in> ns_shared; Nonce NB \<notin> used evs4;
+ Says A' B (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>) \<in> set evs4\<rbrakk>
+ \<Longrightarrow> Says B A (Crypt K (Nonce NB)) # evs4 \<in> ns_shared"
(*Alice responds with Nonce NB if she has seen the key before.
Maybe should somehow check Nonce NA again.
We do NOT send NB-1 or similar as the Spy cannot spoof such things.
Letting the Spy add or subtract 1 lets him send all nonces.
Instead we distinguish the messages by sending the nonce twice.*)
- NS5: "\\<lbrakk>evs5 \\<in> ns_shared;
- Says B' A (Crypt K (Nonce NB)) \\<in> set evs5;
- Says S A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>)
- \\<in> set evs5\\<rbrakk>
- \\<Longrightarrow> Says A B (Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace>) # evs5 \\<in> ns_shared"
+ NS5: "\<lbrakk>evs5 \<in> ns_shared;
+ Says B' A (Crypt K (Nonce NB)) \<in> set evs5;
+ Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
+ \<in> set evs5\<rbrakk>
+ \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) # evs5 \<in> ns_shared"
(*This message models possible leaks of session keys.
The two Nonces identify the protocol run: the rule insists upon
the true senders in order to make them accurate.*)
- Oops: "\\<lbrakk>evso \\<in> ns_shared; Says B A (Crypt K (Nonce NB)) \\<in> set evso;
- Says Server A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>)
- \\<in> set evso\\<rbrakk>
- \\<Longrightarrow> Notes Spy \\<lbrace>Nonce NA, Nonce NB, Key K\\<rbrace> # evso \\<in> ns_shared"
+ Oops: "\<lbrakk>evso \<in> ns_shared; Says B A (Crypt K (Nonce NB)) \<in> set evso;
+ Says Server A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
+ \<in> set evso\<rbrakk>
+ \<Longrightarrow> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> ns_shared"
declare Says_imp_knows_Spy [THEN parts.Inj, dest]
@@ -79,9 +79,9 @@
declare image_eq_UN [simp] (*accelerates proofs involving nested images*)
-(*A "possibility property": there are traces that reach the end*)
-lemma "A \\<noteq> Server \\<Longrightarrow> \\<exists>N K. \\<exists>evs \\<in> ns_shared.
- Says A B (Crypt K \\<lbrace>Nonce N, Nonce N\\<rbrace>) \\<in> set evs"
+text{*A "possibility property": there are traces that reach the end*}
+lemma "A \<noteq> Server \<Longrightarrow> \<exists>N K. \<exists>evs \<in> ns_shared.
+ Says A B (Crypt K \<lbrace>Nonce N, Nonce N\<rbrace>) \<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2] ns_shared.Nil
[THEN ns_shared.NS1, THEN ns_shared.NS2, THEN ns_shared.NS3,
@@ -89,94 +89,94 @@
done
(*This version is similar, while instantiating ?K and ?N to epsilon-terms
-lemma "A \\<noteq> Server \\<Longrightarrow> \\<exists>evs \\<in> ns_shared.
- Says A B (Crypt ?K \\<lbrace>Nonce ?N, Nonce ?N\\<rbrace>) \\<in> set evs"
+lemma "A \<noteq> Server \<Longrightarrow> \<exists>evs \<in> ns_shared.
+ Says A B (Crypt ?K \<lbrace>Nonce ?N, Nonce ?N\<rbrace>) \<in> set evs"
*)
-(**** Inductive proofs about ns_shared ****)
+subsection{*Inductive proofs about @{term ns_shared}*}
-(** Forwarding lemmas, to aid simplification **)
+subsubsection{*Forwarding lemmas, to aid simplification*}
-(*For reasoning about the encrypted portion of message NS3*)
+text{*For reasoning about the encrypted portion of message NS3*}
lemma NS3_msg_in_parts_spies:
- "Says S A (Crypt KA \\<lbrace>N, B, K, X\\<rbrace>) \\<in> set evs \\<Longrightarrow> X \\<in> parts (spies evs)"
+ "Says S A (Crypt KA \<lbrace>N, B, K, X\<rbrace>) \<in> set evs \<Longrightarrow> X \<in> parts (spies evs)"
by blast
-(*For reasoning about the Oops message*)
+text{*For reasoning about the Oops message*}
lemma Oops_parts_spies:
- "Says Server A (Crypt (shrK A) \\<lbrace>NA, B, K, X\\<rbrace>) \\<in> set evs
- \\<Longrightarrow> K \\<in> parts (spies evs)"
+ "Says Server A (Crypt (shrK A) \<lbrace>NA, B, K, X\<rbrace>) \<in> set evs
+ \<Longrightarrow> K \<in> parts (spies evs)"
by blast
-(** Theorems of the form X \\<notin> parts (spies evs) imply that NOBODY
- sends messages containing X! **)
+text{*Theorems of the form @{term "X \<notin> parts (spies evs)"} imply that NOBODY
+ sends messages containing @{term X}*}
-(*Spy never sees another agent's shared key! (unless it's bad at start)*)
+text{*Spy never sees another agent's shared key! (unless it's bad at start)*}
lemma Spy_see_shrK [simp]:
- "evs \\<in> ns_shared \\<Longrightarrow> (Key (shrK A) \\<in> parts (spies evs)) = (A \\<in> bad)"
+ "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all, blast+)
done
lemma Spy_analz_shrK [simp]:
- "evs \\<in> ns_shared \\<Longrightarrow> (Key (shrK A) \\<in> analz (spies evs)) = (A \\<in> bad)"
+ "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
by auto
-(*Nobody can have used non-existent keys!*)
+text{*Nobody can have used non-existent keys!*}
lemma new_keys_not_used [rule_format, simp]:
- "evs \\<in> ns_shared \\<Longrightarrow> Key K \\<notin> used evs \\<longrightarrow> K \\<notin> keysFor (parts (spies evs))"
+ "evs \<in> ns_shared \<Longrightarrow> Key K \<notin> used evs \<longrightarrow> K \<notin> keysFor (parts (spies evs))"
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
-(*Fake, NS2, NS4, NS5*)
-apply (blast dest!: keysFor_parts_insert)+
+txt{*Fake, NS2, NS4, NS5*}
+apply (force dest!: keysFor_parts_insert, blast+)
done
-(** Lemmas concerning the form of items passed in messages **)
+subsubsection{*Lemmas concerning the form of items passed in messages*}
-(*Describes the form of K, X and K' when the Server sends this message.*)
+text{*Describes the form of K, X and K' when the Server sends this message.*}
lemma Says_Server_message_form:
- "\\<lbrakk>Says Server A (Crypt K' \\<lbrace>N, Agent B, Key K, X\\<rbrace>) \\<in> set evs;
- evs \\<in> ns_shared\\<rbrakk>
- \\<Longrightarrow> K \\<notin> range shrK \\<and>
- X = (Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>) \\<and>
+ "\<lbrakk>Says Server A (Crypt K' \<lbrace>N, Agent B, Key K, X\<rbrace>) \<in> set evs;
+ evs \<in> ns_shared\<rbrakk>
+ \<Longrightarrow> K \<notin> range shrK \<and>
+ X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>) \<and>
K' = shrK A"
by (erule rev_mp, erule ns_shared.induct, auto)
-(*If the encrypted message appears then it originated with the Server*)
+text{*If the encrypted message appears then it originated with the Server*}
lemma A_trusts_NS2:
- "\\<lbrakk>Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace> \\<in> parts (spies evs);
- A \\<notin> bad; evs \\<in> ns_shared\\<rbrakk>
- \\<Longrightarrow> Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs"
+ "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
+ A \<notin> bad; evs \<in> ns_shared\<rbrakk>
+ \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs"
apply (erule rev_mp)
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto)
done
lemma cert_A_form:
- "\\<lbrakk>Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace> \\<in> parts (spies evs);
- A \\<notin> bad; evs \\<in> ns_shared\\<rbrakk>
- \\<Longrightarrow> K \\<notin> range shrK \\<and> X = (Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>)"
+ "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
+ A \<notin> bad; evs \<in> ns_shared\<rbrakk>
+ \<Longrightarrow> K \<notin> range shrK \<and> X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>)"
by (blast dest!: A_trusts_NS2 Says_Server_message_form)
(*EITHER describes the form of X when the following message is sent,
OR reduces it to the Fake case.
Use Says_Server_message_form if applicable.*)
lemma Says_S_message_form:
- "\\<lbrakk>Says S A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs;
- evs \\<in> ns_shared\\<rbrakk>
- \\<Longrightarrow> (K \\<notin> range shrK \\<and> X = (Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>))
- \\<or> X \\<in> analz (spies evs)"
+ "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
+ evs \<in> ns_shared\<rbrakk>
+ \<Longrightarrow> (K \<notin> range shrK \<and> X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>))
+ \<or> X \<in> analz (spies evs)"
by (blast dest: Says_imp_knows_Spy cert_A_form analz.Inj)
(*Alternative version also provable
lemma Says_S_message_form2:
- "\\<lbrakk>Says S A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs;
- evs \\<in> ns_shared\\<rbrakk>
- \\<Longrightarrow> Says Server A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs
- \\<or> X \\<in> analz (spies evs)"
-apply (case_tac "A \\<in> bad")
+ "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
+ evs \<in> ns_shared\<rbrakk>
+ \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs
+ \<or> X \<in> analz (spies evs)"
+apply (case_tac "A \<in> bad")
apply (force dest!: Says_imp_knows_Spy [THEN analz.Inj])
by (blast dest!: A_trusts_NS2 Says_Server_message_form)
*)
@@ -185,35 +185,35 @@
(****
SESSION KEY COMPROMISE THEOREM. To prove theorems of the form
- Key K \\<in> analz (insert (Key KAB) (spies evs)) \\<Longrightarrow>
- Key K \\<in> analz (spies evs)
+ Key K \<in> analz (insert (Key KAB) (spies evs)) \<Longrightarrow>
+ Key K \<in> analz (spies evs)
A more general formula must be proved inductively.
****)
-(*NOT useful in this form, but it says that session keys are not used
+text{*NOT useful in this form, but it says that session keys are not used
to encrypt messages containing other keys, in the actual protocol.
- We require that agents should behave like this subsequently also.*)
-lemma "\\<lbrakk>evs \\<in> ns_shared; Kab \\<notin> range shrK\\<rbrakk> \\<Longrightarrow>
- (Crypt KAB X) \\<in> parts (spies evs) \\<and>
- Key K \\<in> parts {X} \\<longrightarrow> Key K \\<in> parts (spies evs)"
+ We require that agents should behave like this subsequently also.*}
+lemma "\<lbrakk>evs \<in> ns_shared; Kab \<notin> range shrK\<rbrakk> \<Longrightarrow>
+ (Crypt KAB X) \<in> parts (spies evs) \<and>
+ Key K \<in> parts {X} \<longrightarrow> Key K \<in> parts (spies evs)"
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
-(*Fake*)
+txt{*Fake*}
apply (blast dest: parts_insert_subset_Un)
-(*Base, NS4 and NS5*)
+txt{*Base, NS4 and NS5*}
apply auto
done
-(** Session keys are not used to encrypt other session keys **)
+subsubsection{*Session keys are not used to encrypt other session keys*}
-(*The equality makes the induction hypothesis easier to apply*)
+text{*The equality makes the induction hypothesis easier to apply*}
lemma analz_image_freshK [rule_format]:
- "evs \\<in> ns_shared \\<Longrightarrow>
- \\<forall>K KK. KK \\<subseteq> - (range shrK) \\<longrightarrow>
- (Key K \\<in> analz (Key`KK \\<union> (spies evs))) =
- (K \\<in> KK \\<or> Key K \\<in> analz (spies evs))"
+ "evs \<in> ns_shared \<Longrightarrow>
+ \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow>
+ (Key K \<in> analz (Key`KK \<union> (spies evs))) =
+ (K \<in> KK \<or> Key K \<in> analz (spies evs))"
apply (erule ns_shared.induct, force)
apply (drule_tac [7] Says_Server_message_form)
apply (erule_tac [4] Says_S_message_form [THEN disjE], analz_freshK, spy_analz)
@@ -221,97 +221,100 @@
lemma analz_insert_freshK:
- "\\<lbrakk>evs \\<in> ns_shared; KAB \\<notin> range shrK\\<rbrakk> \\<Longrightarrow>
- (Key K \\<in> analz (insert (Key KAB) (spies evs))) =
- (K = KAB \\<or> Key K \\<in> analz (spies evs))"
+ "\<lbrakk>evs \<in> ns_shared; KAB \<notin> range shrK\<rbrakk> \<Longrightarrow>
+ (Key K \<in> analz (insert (Key KAB) (spies evs))) =
+ (K = KAB \<or> Key K \<in> analz (spies evs))"
by (simp only: analz_image_freshK analz_image_freshK_simps)
-(** The session key K uniquely identifies the message **)
+subsubsection{*The session key K uniquely identifies the message*}
-(*In messages of this form, the session key uniquely identifies the rest*)
+text{*In messages of this form, the session key uniquely identifies the rest*}
lemma unique_session_keys:
- "\\<lbrakk>Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs;
- Says Server A' (Crypt (shrK A') \\<lbrace>NA', Agent B', Key K, X'\\<rbrace>) \\<in> set evs;
- evs \\<in> ns_shared\\<rbrakk> \\<Longrightarrow> A=A' \\<and> NA=NA' \\<and> B=B' \\<and> X = X'"
+ "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
+ Says Server A' (Crypt (shrK A') \<lbrace>NA', Agent B', Key K, X'\<rbrace>) \<in> set evs;
+ evs \<in> ns_shared\<rbrakk> \<Longrightarrow> A=A' \<and> NA=NA' \<and> B=B' \<and> X = X'"
apply (erule rev_mp, erule rev_mp, erule ns_shared.induct, simp_all, blast+)
done
-(** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
+subsubsection{*Crucial secrecy property: Spy does not see the keys sent in msg NS2*}
-(*Beware of [rule_format] and the universal quantifier!*)
+text{*Beware of [rule_format] and the universal quantifier!*}
lemma secrecy_lemma:
- "\\<lbrakk>Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K,
- Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>\\<rbrace>)
- \\<in> set evs;
- A \\<notin> bad; B \\<notin> bad; evs \\<in> ns_shared\\<rbrakk>
- \\<Longrightarrow> (\\<forall>NB. Notes Spy \\<lbrace>NA, NB, Key K\\<rbrace> \\<notin> set evs) \\<longrightarrow>
- Key K \\<notin> analz (spies evs)"
+ "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
+ Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
+ \<in> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> ns_shared\<rbrakk>
+ \<Longrightarrow> (\<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs) \<longrightarrow>
+ Key K \<notin> analz (spies evs)"
apply (erule rev_mp)
apply (erule ns_shared.induct, force)
apply (frule_tac [7] Says_Server_message_form)
apply (frule_tac [4] Says_S_message_form)
apply (erule_tac [5] disjE)
-apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs, spy_analz) (*Fake*)
-apply blast (*NS2*)
-(*NS3, Server sub-case*) (**LEVEL 8 **)
+apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs, spy_analz)
+txt{*NS2*}
+apply blast
+txt{*NS3, Server sub-case*}
apply (blast dest!: Crypt_Spy_analz_bad A_trusts_NS2
dest: Says_imp_knows_Spy analz.Inj unique_session_keys)
-(*NS3, Spy sub-case; also Oops*)
+txt{*NS3, Spy sub-case; also Oops*}
apply (blast dest: unique_session_keys)+
done
-(*Final version: Server's message in the most abstract form*)
+text{*Final version: Server's message in the most abstract form*}
lemma Spy_not_see_encrypted_key:
- "\\<lbrakk>Says Server A (Crypt K' \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs;
- \\<forall>NB. Notes Spy \\<lbrace>NA, NB, Key K\\<rbrace> \\<notin> set evs;
- A \\<notin> bad; B \\<notin> bad; evs \\<in> ns_shared\\<rbrakk>
- \\<Longrightarrow> Key K \\<notin> analz (spies evs)"
+ "\<lbrakk>Says Server A (Crypt K' \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
+ \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> ns_shared\<rbrakk>
+ \<Longrightarrow> Key K \<notin> analz (spies evs)"
by (blast dest: Says_Server_message_form secrecy_lemma)
-(**** Guarantees available at various stages of protocol ***)
+subsection{*Guarantees available at various stages of protocol*}
-(*If the encrypted message appears then it originated with the Server*)
+text{*If the encrypted message appears then it originated with the Server*}
lemma B_trusts_NS3:
- "\\<lbrakk>Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace> \\<in> parts (spies evs);
- B \\<notin> bad; evs \\<in> ns_shared\\<rbrakk>
- \\<Longrightarrow> \\<exists>NA. Says Server A
- (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K,
- Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>\\<rbrace>)
- \\<in> set evs"
+ "\<lbrakk>Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
+ B \<notin> bad; evs \<in> ns_shared\<rbrakk>
+ \<Longrightarrow> \<exists>NA. Says Server A
+ (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
+ Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
+ \<in> set evs"
apply (erule rev_mp)
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto)
done
lemma A_trusts_NS4_lemma [rule_format]:
- "evs \\<in> ns_shared \\<Longrightarrow>
- Key K \\<notin> analz (spies evs) \\<longrightarrow>
- Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs \\<longrightarrow>
- Crypt K (Nonce NB) \\<in> parts (spies evs) \\<longrightarrow>
- Says B A (Crypt K (Nonce NB)) \\<in> set evs"
+ "evs \<in> ns_shared \<Longrightarrow>
+ Key K \<notin> analz (spies evs) \<longrightarrow>
+ Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow>
+ Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
+ Says B A (Crypt K (Nonce NB)) \<in> set evs"
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
-apply (analz_mono_contra, simp_all, blast) (*Fake*)
+apply (analz_mono_contra, simp_all, blast)
(*NS2: contradiction from the assumptions
- Key K \\<notin> used evs2 and Crypt K (Nonce NB) \\<in> parts (spies evs2) *)
-apply (force dest!: Crypt_imp_keysFor, blast) (*NS3*)
-(*NS4*)
+ Key K \<notin> used evs2 and Crypt K (Nonce NB) \<in> parts (spies evs2) *)
+apply (force dest!: Crypt_imp_keysFor)
+txt{*NS3*}
+apply blast
+txt{*NS4*}
apply (blast dest!: B_trusts_NS3
dest: Says_imp_knows_Spy [THEN analz.Inj]
Crypt_Spy_analz_bad unique_session_keys)
done
-(*This version no longer assumes that K is secure*)
+text{*This version no longer assumes that K is secure*}
lemma A_trusts_NS4:
- "\\<lbrakk>Crypt K (Nonce NB) \\<in> parts (spies evs);
- Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace> \\<in> parts (spies evs);
- \\<forall>NB. Notes Spy \\<lbrace>NA, NB, Key K\\<rbrace> \\<notin> set evs;
- A \\<notin> bad; B \\<notin> bad; evs \\<in> ns_shared\\<rbrakk>
- \\<Longrightarrow> Says B A (Crypt K (Nonce NB)) \\<in> set evs"
+ "\<lbrakk>Crypt K (Nonce NB) \<in> parts (spies evs);
+ Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
+ \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> ns_shared\<rbrakk>
+ \<Longrightarrow> Says B A (Crypt K (Nonce NB)) \<in> set evs"
by (blast intro: A_trusts_NS4_lemma
dest: A_trusts_NS2 Spy_not_see_encrypted_key)
@@ -319,16 +322,18 @@
component X in some instance of NS4. Perhaps an interesting property,
but not needed (after all) for the proofs below.*)
theorem NS4_implies_NS3 [rule_format]:
- "evs \\<in> ns_shared \\<Longrightarrow>
- Key K \\<notin> analz (spies evs) \\<longrightarrow>
- Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs \\<longrightarrow>
- Crypt K (Nonce NB) \\<in> parts (spies evs) \\<longrightarrow>
- (\\<exists>A'. Says A' B X \\<in> set evs)"
+ "evs \<in> ns_shared \<Longrightarrow>
+ Key K \<notin> analz (spies evs) \<longrightarrow>
+ Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow>
+ Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
+ (\<exists>A'. Says A' B X \<in> set evs)"
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra)
-apply (simp_all add: ex_disj_distrib, blast) (*Fake*)
-apply (blast dest!: new_keys_not_used Crypt_imp_keysFor) (*NS2*)
-apply blast (*NS3*)
-(*NS4*)
+apply (simp_all add: ex_disj_distrib, blast)
+txt{*NS2*}
+apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
+txt{*NS3*}
+apply blast
+txt{*NS4*}
apply (blast dest!: B_trusts_NS3
dest: Says_imp_knows_Spy [THEN analz.Inj]
unique_session_keys Crypt_Spy_analz_bad)
@@ -336,30 +341,32 @@
lemma B_trusts_NS5_lemma [rule_format]:
- "\\<lbrakk>B \\<notin> bad; evs \\<in> ns_shared\\<rbrakk> \\<Longrightarrow>
- Key K \\<notin> analz (spies evs) \\<longrightarrow>
+ "\<lbrakk>B \<notin> bad; evs \<in> ns_shared\<rbrakk> \<Longrightarrow>
+ Key K \<notin> analz (spies evs) \<longrightarrow>
Says Server A
- (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K,
- Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>\\<rbrace>) \\<in> set evs \\<longrightarrow>
- Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace> \\<in> parts (spies evs) \\<longrightarrow>
- Says A B (Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace>) \\<in> set evs"
-apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra, simp_all, blast) (*Fake*)
-apply (blast dest!: new_keys_not_used Crypt_imp_keysFor) (*NS2*)
-apply (blast dest!: cert_A_form) (*NS3*)
-(*NS5*)
+ (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
+ Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>) \<in> set evs \<longrightarrow>
+ Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow>
+ Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
+apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra, simp_all, blast)
+txt{*NS2*}
+apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
+txt{*NS3*}
+apply (blast dest!: cert_A_form)
+txt{*NS5*}
apply (blast dest!: A_trusts_NS2
dest: Says_imp_knows_Spy [THEN analz.Inj]
unique_session_keys Crypt_Spy_analz_bad)
done
-(*Very strong Oops condition reveals protocol's weakness*)
+text{*Very strong Oops condition reveals protocol's weakness*}
lemma B_trusts_NS5:
- "\\<lbrakk>Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace> \\<in> parts (spies evs);
- Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace> \\<in> parts (spies evs);
- \\<forall>NA NB. Notes Spy \\<lbrace>NA, NB, Key K\\<rbrace> \\<notin> set evs;
- A \\<notin> bad; B \\<notin> bad; evs \\<in> ns_shared\\<rbrakk>
- \\<Longrightarrow> Says A B (Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace>) \\<in> set evs"
+ "\<lbrakk>Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs);
+ Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
+ \<forall>NA NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> ns_shared\<rbrakk>
+ \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
by (blast intro: B_trusts_NS5_lemma
dest: B_trusts_NS3 Spy_not_see_encrypted_key)
--- a/src/HOL/Auth/Public.thy Sat Apr 26 12:38:17 2003 +0200
+++ b/src/HOL/Auth/Public.thy Sat Apr 26 12:38:42 2003 +0200
@@ -55,42 +55,28 @@
keys are private!) *)
privateKey_neq_publicKey [iff]: "privateKey b A \<noteq> publicKey c A'"
+declare privateKey_neq_publicKey [THEN not_sym, iff]
-
-(*** Basic properties of pubK & priK ***)
+subsection{*Basic properties of @{term pubK} and @{term priK}*}
lemma [iff]: "(publicKey b A = publicKey c A') = (b=c & A=A')"
by (blast dest!: injective_publicKey)
-lemma [iff]:
- "(privateKey b A = privateKey c A') = (b=c & A=A')"
-apply (rule iffI)
-apply (drule_tac f = "invKey" in arg_cong)
-apply (auto );
-done
-
-declare privateKey_neq_publicKey [THEN not_sym, iff]
-
lemma not_symKeys_pubK [iff]: "publicKey b A \<notin> symKeys"
-apply (simp add: symKeys_def)
-done
+by (simp add: symKeys_def)
lemma not_symKeys_priK [iff]: "privateKey b A \<notin> symKeys"
-apply (simp add: symKeys_def)
-done
+by (simp add: symKeys_def)
lemma symKey_neq_priEK: "K \<in> symKeys ==> K \<noteq> priEK A"
by auto
lemma symKeys_neq_imp_neq: "(K \<in> symKeys) \<noteq> (K' \<in> symKeys) ==> K \<noteq> K'"
-apply blast
-done
+by blast
lemma symKeys_invKey_iff [iff]: "(invKey K \<in> symKeys) = (K \<in> symKeys)"
-apply (unfold symKeys_def)
-apply auto
-done
+by (unfold symKeys_def, auto)
lemma analz_symKeys_Decrypt:
"[| Crypt K X \<in> analz H; K \<in> symKeys; Key K \<in> analz H |]
@@ -102,8 +88,7 @@
subsection{*"Image" equations that hold for injective functions*}
lemma invKey_image_eq [simp]: "(invKey x \<in> invKey`A) = (x \<in> A)"
-apply auto
-done
+by auto
(*holds because invKey is injective*)
lemma publicKey_image_eq [simp]:
@@ -111,16 +96,14 @@
by auto
lemma privateKey_notin_image_publicKey [simp]: "privateKey b x \<notin> publicKey c ` AA"
-apply auto
-done
+by auto
lemma privateKey_image_eq [simp]:
"(privateKey b A \<in> invKey ` publicKey c ` AS) = (b=c & A\<in>AS)"
by auto
lemma publicKey_notin_image_privateKey [simp]: "publicKey b A \<notin> invKey ` publicKey c ` AS"
-apply auto
-done
+by auto
subsection{*Symmetric Keys*}
@@ -140,14 +123,12 @@
declare inj_shrK [THEN inj_eq, iff]
lemma priK_neq_shrK [iff]: "shrK A \<noteq> privateKey b C"
-apply (simp add: symKeys_neq_imp_neq)
-done
+by (simp add: symKeys_neq_imp_neq)
declare priK_neq_shrK [THEN not_sym, simp]
lemma pubK_neq_shrK [iff]: "shrK A \<noteq> publicKey b C"
-apply (simp add: symKeys_neq_imp_neq)
-done
+by (simp add: symKeys_neq_imp_neq)
declare pubK_neq_shrK [THEN not_sym, simp]
@@ -242,29 +223,23 @@
(*Agents see their own shared keys!*)
lemma shrK_in_initState [iff]: "Key (shrK A) \<in> initState A"
-apply (induct_tac "A")
-apply auto
-done
+by (induct_tac "A", auto)
lemma shrK_in_knows [iff]: "Key (shrK A) \<in> knows A evs"
by (simp add: initState_subset_knows [THEN subsetD])
lemma shrK_in_used [iff]: "Key (shrK A) \<in> used evs"
-apply (rule initState_into_used)
-apply blast
-done
+by (rule initState_into_used, blast)
(** Fresh keys never clash with long-term shared keys **)
(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
from long-term shared keys*)
lemma Key_not_used: "Key K \<notin> used evs ==> K \<notin> range shrK"
-apply blast
-done
+by blast
lemma shrK_neq: "Key K \<notin> used evs ==> shrK B \<noteq> K"
-apply blast
-done
+by blast
@@ -272,15 +247,11 @@
text{*Agents see their own private keys!*}
lemma priK_in_initState [iff]: "Key (privateKey b A) \<in> initState A"
-apply (induct_tac "A")
-apply auto
-done
+by (induct_tac "A", auto)
text{*Agents see all public keys!*}
lemma publicKey_in_initState [iff]: "Key (publicKey b A) \<in> initState B"
-apply (case_tac "B")
-apply auto
-done
+by (case_tac "B", auto)
text{*All public keys are visible*}
lemma spies_pubK [iff]: "Key (publicKey b A) \<in> spies evs"
@@ -318,13 +289,10 @@
subsection{*Fresh Nonces*}
lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState B)"
-apply (induct_tac "B")
-apply auto
-done
+by (induct_tac "B", auto)
lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []"
-apply (simp add: used_Nil)
-done
+by (simp add: used_Nil)
subsection{*Supply fresh nonces for possibility theorems*}
@@ -332,32 +300,27 @@
text{*In any trace, there is an upper bound N on the greatest nonce in use*}
lemma Nonce_supply_lemma: "EX N. ALL n. N<=n --> Nonce n \<notin> used evs"
apply (induct_tac "evs")
-apply (rule_tac x = "0" in exI)
+apply (rule_tac x = 0 in exI)
apply (simp_all (no_asm_simp) add: used_Cons split add: event.split)
apply safe
apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
done
lemma Nonce_supply1: "EX N. Nonce N \<notin> used evs"
-apply (rule Nonce_supply_lemma [THEN exE])
-apply blast
-done
+by (rule Nonce_supply_lemma [THEN exE], blast)
lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs"
apply (rule Nonce_supply_lemma [THEN exE])
-apply (rule someI)
-apply fast
+apply (rule someI, fast)
done
subsection{*Specialized rewriting for the analz_image_... theorems*}
lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} Un H"
-apply blast
-done
+by blast
lemma insert_Key_image: "insert (Key K) (Key`KK \<union> C) = Key ` (insert K KK) \<union> C"
-apply blast
-done
+by blast
ML
{*
@@ -388,8 +351,7 @@
by (simp add: symKeys_def)
lemma Crypt_imp_keysFor :"[|K \<in> symKeys; Crypt K X \<in> H|] ==> K \<in> keysFor H"
-apply (drule Crypt_imp_invKey_keysFor, simp)
-done
+by (drule Crypt_imp_invKey_keysFor, simp)
subsection{*Specialized Methods for Possibility Theorems*}
@@ -419,20 +381,35 @@
+lemmas analz_image_freshK_simps =
+ simp_thms mem_simps --{*these two allow its use with @{text "only:"}*}
+ disj_comms
+ image_insert [THEN sym] image_Un [THEN sym] empty_subsetI insert_subset
+ analz_insert_eq Un_upper2 [THEN analz_mono, THEN [2] rev_subsetD]
+ insert_Key_singleton
+ Key_not_used insert_Key_image Un_assoc [THEN sym]
+
ML
{*
-bind_thms ("analz_image_freshK_simps",
- simp_thms @ mem_simps @ (*these two allow its use with only:*)
- disj_comms @
- [image_insert RS sym, image_Un RS sym, empty_subsetI, insert_subset,
- analz_insert_eq, impOfSubs (Un_upper2 RS analz_mono),
- insert_Key_singleton,
- Key_not_used, insert_Key_image, Un_assoc RS sym]);
-
val analz_image_freshK_ss =
simpset() delsimps [image_insert, image_Un]
delsimps [imp_disjL] (*reduces blow-up*)
- addsimps analz_image_freshK_simps;
+ addsimps thms"analz_image_freshK_simps"
*}
+axioms
+ Key_supply_ax: "finite KK ==> \<exists>K\<in>symKeys. K \<notin> KK & Key K \<notin> used evs"
+ --{*Unlike the corresponding property of nonces, this cannot be proved.
+ We have infinitely many agents and there is nothing to stop their
+ long-term keys from exhausting all the natural numbers. The axiom
+ assumes that their keys are dispersed so as to leave room for infinitely
+ many fresh session keys. We could, alternatively, restrict agents to
+ an unspecified finite number. We could however replace @{term"used evs"}
+ by @{term "used []"}.*}
+
+
+lemma Key_supply1: "\<exists>K\<in>symKeys. Key K \<notin> used evs"
+by (rule Finites.emptyI [THEN Key_supply_ax, THEN bexE], blast)
+
+
end
--- a/src/HOL/Auth/Shared.thy Sat Apr 26 12:38:17 2003 +0200
+++ b/src/HOL/Auth/Shared.thy Sat Apr 26 12:38:42 2003 +0200
@@ -8,8 +8,7 @@
Shared, long-term keys; initial states of agents
*)
-theory Shared = Event
-files ("Shared_lemmas.ML"):
+theory Shared = Event:
consts
shrK :: "agent => key" (*symmetric keys*)
@@ -25,16 +24,264 @@
initState_Spy: "initState Spy = Key`shrK`bad"
+subsection{*Basic properties of shrK*}
+
+(*Injectiveness: Agents' long-term keys are distinct.*)
+declare inj_shrK [THEN inj_eq, iff]
+
+lemma invKey_K [simp]: "invKey K = K"
+apply (insert isSym_keys)
+apply (simp add: symKeys_def)
+done
+
+
+lemma analz_Decrypt' [dest]:
+ "[| Crypt K X \<in> analz H; Key K \<in> analz H |] ==> X \<in> analz H"
+by auto
+
+text{*Now cancel the @{text dest} attribute given to
+ @{text analz.Decrypt} in its declaration.*}
+ML
+{*
+Delrules [analz.Decrypt];
+*}
+
+text{*Rewrites should not refer to @{term "initState(Friend i)"} because
+ that expression is not in normal form.*}
+
+lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}"
+apply (unfold keysFor_def)
+apply (induct_tac "C", auto)
+done
+
+(*Specialized to shared-key model: no @{term invKey}*)
+lemma keysFor_parts_insert:
+ "[| K \<in> keysFor (parts (insert X G)); X \<in> synth (analz H) |] \
+\ ==> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H";
+by (force dest: Event.keysFor_parts_insert)
+
+lemma Crypt_imp_keysFor: "Crypt K X \<in> H ==> K \<in> keysFor H"
+by (drule Crypt_imp_invKey_keysFor, simp)
+
+
+subsection{*Function "knows"*}
+
+(*Spy sees shared keys of agents!*)
+lemma Spy_knows_Spy_bad [intro!]: "A: bad ==> Key (shrK A) \<in> knows Spy evs"
+apply (induct_tac "evs")
+apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
+done
+
+(*For case analysis on whether or not an agent is compromised*)
+lemma Crypt_Spy_analz_bad: "[| Crypt (shrK A) X \<in> analz (knows Spy evs); A: bad |]
+ ==> X \<in> analz (knows Spy evs)"
+apply (force dest!: analz.Decrypt)
+done
+
+
+(** Fresh keys never clash with long-term shared keys **)
+
+(*Agents see their own shared keys!*)
+lemma shrK_in_initState [iff]: "Key (shrK A) \<in> initState A"
+by (induct_tac "A", auto)
+
+lemma shrK_in_used [iff]: "Key (shrK A) \<in> used evs"
+by (rule initState_into_used, blast)
+
+(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
+ from long-term shared keys*)
+lemma Key_not_used [simp]: "Key K \<notin> used evs ==> K \<notin> range shrK"
+by blast
+
+lemma shrK_neq [simp]: "Key K \<notin> used evs ==> shrK B \<noteq> K"
+by blast
+
+declare shrK_neq [THEN not_sym, simp]
+
+
+subsection{*Fresh nonces*}
+
+lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState B)"
+by (induct_tac "B", auto)
+
+lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []"
+apply (simp (no_asm) add: used_Nil)
+done
+
+
+subsection{*Supply fresh nonces for possibility theorems.*}
+
+(*In any trace, there is an upper bound N on the greatest nonce in use.*)
+lemma Nonce_supply_lemma: "\<exists>N. ALL n. N<=n --> Nonce n \<notin> used evs"
+apply (induct_tac "evs")
+apply (rule_tac x = 0 in exI)
+apply (simp_all (no_asm_simp) add: used_Cons split add: event.split)
+apply safe
+apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
+done
+
+lemma Nonce_supply1: "\<exists>N. Nonce N \<notin> used evs"
+by (rule Nonce_supply_lemma [THEN exE], blast)
+
+lemma Nonce_supply2: "\<exists>N N'. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' & N \<noteq> N'"
+apply (cut_tac evs = evs in Nonce_supply_lemma)
+apply (cut_tac evs = "evs'" in Nonce_supply_lemma, clarify)
+apply (rule_tac x = N in exI)
+apply (rule_tac x = "Suc (N+Na) " in exI)
+apply (simp (no_asm_simp) add: less_not_refl3 le_add1 le_add2 less_Suc_eq_le)
+done
+
+lemma Nonce_supply3: "\<exists>N N' N''. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' &
+ Nonce N'' \<notin> used evs'' & N \<noteq> N' & N' \<noteq> N'' & N \<noteq> N''"
+apply (cut_tac evs = evs in Nonce_supply_lemma)
+apply (cut_tac evs = "evs'" in Nonce_supply_lemma)
+apply (cut_tac evs = "evs''" in Nonce_supply_lemma, clarify)
+apply (rule_tac x = N in exI)
+apply (rule_tac x = "Suc (N+Na) " in exI)
+apply (rule_tac x = "Suc (Suc (N+Na+Nb))" in exI)
+apply (simp (no_asm_simp) add: less_not_refl3 le_add1 le_add2 less_Suc_eq_le)
+done
+
+lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs"
+apply (rule Nonce_supply_lemma [THEN exE])
+apply (rule someI, blast)
+done
+
+subsection{*Supply fresh keys for possibility theorems.*}
+
axioms
- (*Unlike the corresponding property of nonces, this cannot be proved.
+ Key_supply_ax: "finite KK ==> \<exists>K. K \<notin> KK & Key K \<notin> used evs"
+ --{*Unlike the corresponding property of nonces, this cannot be proved.
We have infinitely many agents and there is nothing to stop their
long-term keys from exhausting all the natural numbers. The axiom
assumes that their keys are dispersed so as to leave room for infinitely
many fresh session keys. We could, alternatively, restrict agents to
- an unspecified finite number.*)
- Key_supply_ax: "finite KK ==> EX K. K ~: KK & Key K ~: used evs"
+ an unspecified finite number. We could however replace @{term"used evs"}
+ by @{term "used []"}.*}
+
+lemma Key_supply1: "\<exists>K. Key K \<notin> used evs"
+by (rule Finites.emptyI [THEN Key_supply_ax, THEN exE], blast)
+
+lemma Key_supply2: "\<exists>K K'. Key K \<notin> used evs & Key K' \<notin> used evs' & K \<noteq> K'"
+apply (cut_tac evs = evs in Finites.emptyI [THEN Key_supply_ax])
+apply (erule exE)
+apply (cut_tac evs="evs'" in Finites.emptyI [THEN Finites.insertI, THEN Key_supply_ax], auto)
+done
+
+lemma Key_supply3: "\<exists>K K' K''. Key K \<notin> used evs & Key K' \<notin> used evs' &
+ Key K'' \<notin> used evs'' & K \<noteq> K' & K' \<noteq> K'' & K \<noteq> K''"
+apply (cut_tac evs = evs in Finites.emptyI [THEN Key_supply_ax])
+apply (erule exE)
+(*Blast_tac requires instantiation of the keys for some reason*)
+apply (cut_tac evs="evs'" and a1 = K in Finites.emptyI [THEN Finites.insertI, THEN Key_supply_ax])
+apply (erule exE)
+apply (cut_tac evs = "evs''" and a1 = Ka and a2 = K
+ in Finites.emptyI [THEN Finites.insertI, THEN Finites.insertI, THEN Key_supply_ax], blast)
+done
+
+lemma Key_supply: "Key (@ K. Key K \<notin> used evs) \<notin> used evs"
+apply (rule Finites.emptyI [THEN Key_supply_ax, THEN exE])
+apply (rule someI, blast)
+done
+
+subsection{*Tactics for possibility theorems*}
+
+ML
+{*
+val inj_shrK = thm "inj_shrK";
+val isSym_keys = thm "isSym_keys";
+val Key_supply_ax = thm "Key_supply_ax";
+val Key_supply = thm "Key_supply";
+val Nonce_supply = thm "Nonce_supply";
+val invKey_K = thm "invKey_K";
+val analz_Decrypt' = thm "analz_Decrypt'";
+val keysFor_parts_initState = thm "keysFor_parts_initState";
+val keysFor_parts_insert = thm "keysFor_parts_insert";
+val Crypt_imp_keysFor = thm "Crypt_imp_keysFor";
+val Spy_knows_Spy_bad = thm "Spy_knows_Spy_bad";
+val Crypt_Spy_analz_bad = thm "Crypt_Spy_analz_bad";
+val shrK_in_initState = thm "shrK_in_initState";
+val shrK_in_used = thm "shrK_in_used";
+val Key_not_used = thm "Key_not_used";
+val shrK_neq = thm "shrK_neq";
+val Nonce_notin_initState = thm "Nonce_notin_initState";
+val Nonce_notin_used_empty = thm "Nonce_notin_used_empty";
+val Nonce_supply_lemma = thm "Nonce_supply_lemma";
+val Nonce_supply1 = thm "Nonce_supply1";
+val Nonce_supply2 = thm "Nonce_supply2";
+val Nonce_supply3 = thm "Nonce_supply3";
+val Nonce_supply = thm "Nonce_supply";
+val Key_supply1 = thm "Key_supply1";
+val Key_supply2 = thm "Key_supply2";
+val Key_supply3 = thm "Key_supply3";
+val Key_supply = thm "Key_supply";
+*}
+
-use "Shared_lemmas.ML"
+ML
+{*
+(*Omitting used_Says makes the tactic much faster: it leaves expressions
+ such as Nonce ?N \<notin> used evs that match Nonce_supply*)
+fun gen_possibility_tac ss state = state |>
+ (REPEAT
+ (ALLGOALS (simp_tac (ss delsimps [used_Says, used_Notes, used_Gets]
+ setSolver safe_solver))
+ THEN
+ REPEAT_FIRST (eq_assume_tac ORELSE'
+ resolve_tac [refl, conjI, Nonce_supply, Key_supply])))
+
+(*Tactic for possibility theorems (ML script version)*)
+fun possibility_tac state = gen_possibility_tac (simpset()) state
+
+(*For harder protocols (such as Recur) where we have to set up some
+ nonces and keys initially*)
+fun basic_possibility_tac st = st |>
+ REPEAT
+ (ALLGOALS (asm_simp_tac (simpset() setSolver safe_solver))
+ THEN
+ REPEAT_FIRST (resolve_tac [refl, conjI]))
+*}
+
+subsection{*Specialized rewriting for analz_insert_freshK*}
+
+lemma subset_Compl_range: "A <= - (range shrK) ==> shrK x \<notin> A"
+by blast
+
+lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} \<union> H"
+by blast
+
+lemma insert_Key_image: "insert (Key K) (Key`KK \<union> C) = Key ` (insert K KK) \<union> C"
+by blast
+
+(** Reverse the normal simplification of "image" to build up (not break down)
+ the set of keys. Use analz_insert_eq with (Un_upper2 RS analz_mono) to
+ erase occurrences of forwarded message components (X). **)
+
+lemmas analz_image_freshK_simps =
+ simp_thms mem_simps --{*these two allow its use with @{text "only:"}*}
+ disj_comms
+ image_insert [THEN sym] image_Un [THEN sym] empty_subsetI insert_subset
+ analz_insert_eq Un_upper2 [THEN analz_mono, THEN [2] rev_subsetD]
+ insert_Key_singleton subset_Compl_range
+ Key_not_used insert_Key_image Un_assoc [THEN sym]
+
+(*Lemma for the trivial direction of the if-and-only-if*)
+lemma analz_image_freshK_lemma:
+ "(Key K \<in> analz (Key`nE \<union> H)) --> (K \<in> nE | Key K \<in> analz H) ==>
+ (Key K \<in> analz (Key`nE \<union> H)) = (K \<in> nE | Key K \<in> analz H)"
+by (blast intro: analz_mono [THEN [2] rev_subsetD])
+
+ML
+{*
+val analz_image_freshK_lemma = thm "analz_image_freshK_lemma";
+
+val analz_image_freshK_ss =
+ simpset() delsimps [image_insert, image_Un]
+ delsimps [imp_disjL] (*reduces blow-up*)
+ addsimps thms "analz_image_freshK_simps"
+*}
+
+
(*Lets blast_tac perform this step without needing the simplifier*)
lemma invKey_shrK_iff [iff]:
--- a/src/HOL/Auth/Yahalom.thy Sat Apr 26 12:38:17 2003 +0200
+++ b/src/HOL/Auth/Yahalom.thy Sat Apr 26 12:38:42 2003 +0200
@@ -150,8 +150,10 @@
"evs \<in> yahalom ==> Key K \<notin> used evs --> K \<notin> keysFor (parts (knows Spy evs))"
apply (erule yahalom.induct, force,
frule_tac [6] YM4_parts_knows_Spy, simp_all)
-(*Fake, YM3, YM4*)
-apply (blast dest!: keysFor_parts_insert)+
+txt{*Fake*}
+apply (force dest!: keysFor_parts_insert)
+txt{*YM3, YM4*}
+apply blast+
done
--- a/src/HOL/Auth/Yahalom2.thy Sat Apr 26 12:38:17 2003 +0200
+++ b/src/HOL/Auth/Yahalom2.thy Sat Apr 26 12:38:42 2003 +0200
@@ -137,8 +137,10 @@
"evs \<in> yahalom ==> Key K \<notin> used evs --> K \<notin> keysFor (parts (knows Spy evs))"
apply (erule yahalom.induct, force,
frule_tac [6] YM4_parts_knows_Spy, simp_all)
-(*Fake, YM3, YM4*)
-apply (blast dest!: keysFor_parts_insert)+
+txt{*Fake*}
+apply (force dest!: keysFor_parts_insert)
+txt{*YM3, YM4*}
+apply blast+
done
@@ -394,7 +396,7 @@
apply (force dest!: Crypt_imp_keysFor)
(*YM4: was Crypt K (Nonce NB) the very last message? If so, apply unicity
of session keys; if not, use ind. hyp.*)
-apply (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys )
+apply (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys )
done
--- a/src/HOL/Auth/Yahalom_Bad.thy Sat Apr 26 12:38:17 2003 +0200
+++ b/src/HOL/Auth/Yahalom_Bad.thy Sat Apr 26 12:38:42 2003 +0200
@@ -128,8 +128,10 @@
"evs \<in> yahalom ==> Key K \<notin> used evs --> K \<notin> keysFor (parts (knows Spy evs))"
apply (erule yahalom.induct, force,
frule_tac [6] YM4_parts_knows_Spy, simp_all)
-(*Fake, YM3, YM4*)
-apply (blast dest!: keysFor_parts_insert)+
+txt{*Fake*}
+apply (force dest!: keysFor_parts_insert)
+txt{*YM3, YM4*}
+apply blast+
done
--- a/src/HOL/IsaMakefile Sat Apr 26 12:38:17 2003 +0200
+++ b/src/HOL/IsaMakefile Sat Apr 26 12:38:42 2003 +0200
@@ -363,14 +363,13 @@
HOL-Auth: HOL $(LOG)/HOL-Auth.gz
$(LOG)/HOL-Auth.gz: $(OUT)/HOL \
- Auth/CertifiedEmail.thy Auth/Event_lemmas.ML Auth/Event.thy \
- Auth/Message_lemmas.ML Auth/Message.thy Auth/NS_Public.thy \
- Auth/NS_Public_Bad.thy \
+ Auth/CertifiedEmail.thy Auth/Event.thy \
+ Auth/Message.thy Auth/NS_Public.thy Auth/NS_Public_Bad.thy \
Auth/NS_Shared.thy Auth/OtwayRees.thy Auth/OtwayRees_AN.thy \
Auth/OtwayRees_Bad.thy Auth/Public.thy Auth/ROOT.ML \
- Auth/Recur.thy Auth/Shared_lemmas.ML Auth/Shared.thy \
+ Auth/Recur.thy Auth/Shared.thy \
Auth/TLS.thy Auth/WooLam.thy \
- Auth/Kerberos_BAN.ML Auth/Kerberos_BAN.thy \
+ Auth/Kerberos_BAN.thy \
Auth/KerberosIV.ML Auth/KerberosIV.thy \
Auth/Yahalom.thy Auth/Yahalom2.thy Auth/Yahalom_Bad.thy \
Auth/Guard/Analz.thy Auth/Guard/Extensions.thy Auth/Guard/GuardK.thy \