# HG changeset patch # User paulson # Date 1127898933 -7200 # Node ID a04b5b43625e7b0baff84b06085a4766d7bd1875 # Parent 91d3604ec4b5143f97d1e4982d2176bb3daa7c27 streamlined theory; conformance to recent publication diff -r 91d3604ec4b5 -r a04b5b43625e src/HOL/Auth/CertifiedEmail.thy --- 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|} \ set evs; S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|}; - Key K \ analz(spies evs); + Key K \ analz (spies evs); evs \ certified_mail; S\Spy|] ==> R \ bad & Gets S (Crypt (priSK TTP) S2TTP) \ set evs" @@ -432,34 +432,33 @@ evs \ certified_mail; S\Spy; R \ bad|] ==> Key K \ 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|} \ set evs; - S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|}; - Notes R {|Agent TTP, Agent R, Key K, hs|} \ set evs; - S\Spy; evs \ certified_mail|] - ==> Gets S (Crypt (priSK TTP) S2TTP) \ set evs" + "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO, + Number cleartext, Nonce q, S2TTP|} \ set evs; + S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|}; + Notes R {|Agent TTP, Agent R, Key K, hs|} \ set evs; + S\Spy; evs \ certified_mail|] + ==> Gets S (Crypt (priSK TTP) S2TTP) \ 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 \ used evs; S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, diff -r 91d3604ec4b5 -r a04b5b43625e src/HOL/Auth/Guard/Analz.thy --- 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) diff -r 91d3604ec4b5 -r a04b5b43625e src/HOL/Auth/Guard/Extensions.thy --- 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) diff -r 91d3604ec4b5 -r a04b5b43625e src/HOL/Auth/Message.thy --- 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 \ parts H) = (G \ parts H)" +apply (rule iffI) +apply (iprover intro: subset_trans parts_increasing) +apply (frule parts_mono, simp) +done + lemma parts_trans: "[| X\ parts G; G \ parts H |] ==> X\ 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 \ analz H) = (G \ analz H)" +apply (rule iffI) +apply (iprover intro: subset_trans analz_increasing) +apply (frule analz_mono, simp) +done + lemma analz_trans: "[| X\ analz G; G \ analz H |] ==> X\ analz H" by (drule analz_mono, blast) @@ -528,16 +537,15 @@ text{*A congruence rule for "analz" *} lemma analz_subset_cong: - "[| analz G \ analz G'; analz H \ analz H' - |] ==> analz (G \ H) \ analz (G' \ H')" -apply clarify -apply (erule analz.induct) -apply (best intro: analz_mono [THEN subsetD])+ + "[| analz G \ analz G'; analz H \ analz H' |] + ==> analz (G \ H) \ analz (G' \ 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 \ H) = analz (G' \ H')" + "[| analz G = analz G'; analz H = analz H' |] + ==> analz (G \ H) = analz (G' \ 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 \ synth H) = (G \ 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\ synth G; G \ synth H |] ==> X\ synth H" by (drule synth_mono, blast) @@ -896,7 +910,7 @@ by auto lemma synth_analz_mono: "G\H ==> synth (analz(G)) \ synth (analz(H))" -by (simp add: synth_mono analz_mono) +by (iprover intro: synth_mono analz_mono) lemma Fake_analz_eq [simp]: "X \ 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 \ synth (analz H) ==> parts{X} \ synth (analz H) \ 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]