--- a/src/HOL/Auth/CertifiedEmail.thy Wed Sep 28 11:14:26 2005 +0200
+++ b/src/HOL/Auth/CertifiedEmail.thy Wed Sep 28 11:15:33 2005 +0200
@@ -397,11 +397,11 @@
text{*A Sender's guarantee:
If Spy gets the key then @{term R} is bad and @{term S} moreover
gets his return receipt (and therefore has no grounds for complaint).*}
-theorem Spy_see_encrypted_key_imp:
+theorem S_fairness_bad_R:
"[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
Number cleartext, Nonce q, S2TTP|} \<in> set evs;
S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|};
- Key K \<in> analz(spies evs);
+ Key K \<in> analz (spies evs);
evs \<in> certified_mail;
S\<noteq>Spy|]
==> R \<in> bad & Gets S (Crypt (priSK TTP) S2TTP) \<in> set evs"
@@ -432,34 +432,33 @@
evs \<in> certified_mail;
S\<noteq>Spy; R \<notin> bad|]
==> Key K \<notin> analz(spies evs)"
-by (blast dest: Spy_see_encrypted_key_imp)
+by (blast dest: S_fairness_bad_R)
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:
- "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
- Number cleartext, Nonce q, S2TTP|} \<in> set evs;
- S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|};
- Notes R {|Agent TTP, Agent R, Key K, hs|} \<in> set evs;
- S\<noteq>Spy; evs \<in> certified_mail|]
- ==> Gets S (Crypt (priSK TTP) S2TTP) \<in> set evs"
+ "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
+ Number cleartext, Nonce q, S2TTP|} \<in> set evs;
+ S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|};
+ Notes R {|Agent TTP, Agent R, Key K, hs|} \<in> set evs;
+ S\<noteq>Spy; evs \<in> certified_mail|]
+ ==> Gets S (Crypt (priSK TTP) S2TTP) \<in> set evs"
apply (erule rev_mp)
apply (erule ssubst)
apply (erule rev_mp)
apply (erule certified_mail.induct, simp_all)
txt{*Message 1*}
apply (blast dest: Notes_imp_used)
-txt{*Message 3*}
-apply (blast dest: Notes_SSL_imp_used S2TTP_sender Key_unique
- Spy_see_encrypted_key_imp)
+txt{*Message 3*}
+apply (blast dest: Notes_SSL_imp_used S2TTP_sender Key_unique S_fairness_bad_R)
done
-text{*Recipient's guarantee: if @{term R} sends message 2, and
- a delivery certificate exists, then @{term R}
- receives the necessary key.*}
-theorem R_guarantee:
+text{*If @{term R} sends message 2, and a delivery certificate exists,
+ then @{term R} receives the necessary key. This result is also important
+ to @{term S}, as it confirms the validity of the return receipt.*}
+theorem RR_validity:
"[|Crypt (priSK TTP) S2TTP \<in> used evs;
S2TTP = Crypt (pubEK TTP)
{|Agent S, Number AO, Key K, Agent R,
--- a/src/HOL/Auth/Guard/Analz.thy Wed Sep 28 11:14:26 2005 +0200
+++ b/src/HOL/Auth/Guard/Analz.thy Wed Sep 28 11:15:33 2005 +0200
@@ -237,11 +237,6 @@
X:analz (kparts {Z} Un kparts H)"
by (rule analz_sub, auto)
-lemma Key_analz_kparts_insert: "Key K:analz (kparts {Z} Un H)
-==> Key K:analz (insert Z H)"
-apply (subgoal_tac "Key K:analz ({Z} Un H)", simp)
-by (rule_tac in_analz_subset_cong, auto dest: analz_kparts_analz)
-
lemma Nonce_kparts_synth [rule_format]: "Y:synth (analz G)
==> Nonce n:kparts {Y} --> Nonce n:analz G"
by (erule synth.induct, auto)
--- a/src/HOL/Auth/Guard/Extensions.thy Wed Sep 28 11:14:26 2005 +0200
+++ b/src/HOL/Auth/Guard/Extensions.thy Wed Sep 28 11:15:33 2005 +0200
@@ -151,7 +151,8 @@
by (rule parts_insert_substI, simp)
lemma parts_parts: "[| X:parts {Y}; Y:parts G |] ==> X:parts G"
-by (drule_tac x=Y in in_sub, drule parts_mono, auto)
+by (frule parts_cut, auto)
+
lemma parts_parts_parts: "[| X:parts {Y}; Y:parts {Z}; Z:parts G |] ==> X:parts G"
by (auto dest: parts_parts)
--- a/src/HOL/Auth/Message.thy Wed Sep 28 11:14:26 2005 +0200
+++ b/src/HOL/Auth/Message.thy Wed Sep 28 11:15:33 2005 +0200
@@ -240,6 +240,12 @@
lemma parts_idem [simp]: "parts (parts H) = parts H"
by blast
+lemma parts_subset_iff [simp]: "(parts G \<subseteq> parts H) = (G \<subseteq> parts H)"
+apply (rule iffI)
+apply (iprover intro: subset_trans parts_increasing)
+apply (frule parts_mono, simp)
+done
+
lemma parts_trans: "[| X\<in> parts G; G \<subseteq> parts H |] ==> X\<in> parts H"
by (drule parts_mono, blast)
@@ -288,13 +294,11 @@
done
lemma parts_insert_Crypt [simp]:
- "parts (insert (Crypt K X) H) =
- insert (Crypt K X) (parts (insert X H))"
+ "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)+
+apply (blast intro: parts.Body)
done
lemma parts_insert_MPair [simp]:
@@ -303,7 +307,6 @@
apply (rule equalityI)
apply (rule subsetI)
apply (erule parts.induct, auto)
-apply (erule parts.induct)
apply (blast intro: parts.Fst parts.Snd)+
done
@@ -507,6 +510,12 @@
lemma analz_idem [simp]: "analz (analz H) = analz H"
by blast
+lemma analz_subset_iff [simp]: "(analz G \<subseteq> analz H) = (G \<subseteq> analz H)"
+apply (rule iffI)
+apply (iprover intro: subset_trans analz_increasing)
+apply (frule analz_mono, simp)
+done
+
lemma analz_trans: "[| X\<in> analz G; G \<subseteq> analz H |] ==> X\<in> analz H"
by (drule analz_mono, blast)
@@ -528,16 +537,15 @@
text{*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])+
+ "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H' |]
+ ==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
+apply simp
+apply (iprover intro: conjI subset_trans analz_mono Un_upper1 Un_upper2)
done
lemma analz_cong:
- "[| analz G = analz G'; analz H = analz H'
- |] ==> analz (G \<union> H) = analz (G' \<union> H')"
+ "[| analz G = analz G'; analz H = analz H' |]
+ ==> analz (G \<union> H) = analz (G' \<union> H')"
by (intro equalityI analz_subset_cong, simp_all)
lemma analz_insert_cong:
@@ -613,6 +621,12 @@
lemma synth_idem: "synth (synth H) = synth H"
by blast
+lemma synth_subset_iff [simp]: "(synth G \<subseteq> synth H) = (G \<subseteq> synth H)"
+apply (rule iffI)
+apply (iprover intro: subset_trans synth_increasing)
+apply (frule synth_mono, simp add: synth_idem)
+done
+
lemma synth_trans: "[| X\<in> synth G; G \<subseteq> synth H |] ==> X\<in> synth H"
by (drule synth_mono, blast)
@@ -896,7 +910,7 @@
by auto
lemma synth_analz_mono: "G\<subseteq>H ==> synth (analz(G)) \<subseteq> synth (analz(H))"
-by (simp add: synth_mono analz_mono)
+by (iprover intro: synth_mono analz_mono)
lemma Fake_analz_eq [simp]:
"X \<in> synth(analz H) ==> synth (analz (insert X H)) = synth (analz H)"
@@ -904,7 +918,9 @@
apply (simp add: synth_increasing[THEN Un_absorb2])
apply (drule synth_mono)
apply (simp add: synth_idem)
-apply (blast intro: synth_analz_mono [THEN [2] rev_subsetD])
+apply (rule equalityI)
+apply (simp add: );
+apply (rule synth_analz_mono, blast)
done
text{*Two generalizations of @{text analz_insert_eq}*}
@@ -922,8 +938,9 @@
lemma Fake_parts_sing:
"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)
+ apply (erule_tac [2] Fake_parts_insert)
+apply (rule parts_mono)
+apply (blast intro: elim:);
done
lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]