# HG changeset patch
# User paulson
# Date 1051612600 -7200
# Node ID 8c23dea4648e5a5b021fcc62761879e55e5d3610
# Parent  b224c2fd4288046419a266b7ad9c824972e713ab
better guarantees

diff -r b224c2fd4288 -r 8c23dea4648e src/HOL/Auth/CertifiedEmail.thy
--- a/src/HOL/Auth/CertifiedEmail.thy	Mon Apr 28 17:52:52 2003 +0200
+++ b/src/HOL/Auth/CertifiedEmail.thy	Tue Apr 29 12:36:40 2003 +0200
@@ -105,8 +105,7 @@
 apply (rule_tac [2] certified_mail.Nil
                     [THEN certified_mail.CM1, THEN certified_mail.Reception,
                      THEN certified_mail.CM2, 
-                     THEN certified_mail.CM3], possibility, possibility) 
-apply auto 
+                     THEN certified_mail.CM3], possibility, possibility, auto) 
 done
 
 
@@ -177,6 +176,28 @@
      ==> (Key (privateKey b A) \<in> parts (spies evs)) = (A \<in> bad)"
 by (blast intro: Spy_dont_know_private_keys parts.Inj)
 
+lemma Spy_dont_know_TTPDecKey [simp]:
+     "evs \<in> certified_mail ==> Key TTPDecKey \<notin> parts(knows Spy evs)"
+by auto
+
+lemma Spy_dont_know_TTPDecKey_analz [simp]:
+     "evs \<in> certified_mail ==> Key TTPDecKey \<notin> analz(knows Spy evs)" 
+by (force dest!: analz_subset_parts[THEN subsetD])
+
+lemma Spy_dont_know_TTPSigKey [simp]:
+     "evs \<in> certified_mail ==> Key TTPSigKey \<notin> parts(knows Spy evs)"
+by auto
+
+lemma Spy_dont_know_TTPSigKey_analz [simp]:
+     "evs \<in> certified_mail ==> Key TTPSigKey \<notin> analz(knows Spy evs)" 
+by (force dest!: analz_subset_parts[THEN subsetD])
+
+text{*Thus, prove any goal that assumes that @{term Spy} knows a private key
+belonging to @{term TTP}*}
+declare Spy_dont_know_TTPDecKey [THEN [2] rev_notE, elim!]
+declare Spy_dont_know_TTPSigKey [THEN [2] rev_notE, elim!]
+
+
 
 lemma CM3_k_parts_knows_Spy:
  "[| evs \<in> certified_mail;
@@ -247,20 +268,6 @@
 done
 
 
-lemma Spy_dont_know_TTPDecKey [simp]:
-     "evs \<in> certified_mail ==> Key TTPDecKey \<notin> parts(knows Spy evs)"
-by auto
-
-lemma Spy_dont_know_TTPDecKey_analz [simp]:
-     "evs \<in> certified_mail ==> Key TTPDecKey \<notin> analz(knows Spy evs)" 
-by (force dest!: analz_subset_parts[THEN subsetD])
-
-
-lemma Spy_knows_TTPVerKey [simp]:
-     "Key (invKey TTPSigKey) \<in> analz(knows Spy evs)"
-by simp
-
-
 subsection{*Proving Confidentiality Results*}
 
 lemma analz_image_freshK [rule_format]:
@@ -324,7 +331,7 @@
 txt{*Message 2*}
 apply (simp add: parts_insert2, clarify) 
 apply (drule parts_cut, assumption, simp) 
-apply (blast dest: parts_knows_Spy_subset_used [THEN subsetD]) 
+apply (blast intro: usedI) 
 txt{*Message 3*} 
 apply (blast dest: Notes_SSL_imp_used used_parts_subset_parts) 
 done 
@@ -402,9 +409,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
+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:
       "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO, 
@@ -413,7 +422,7 @@
          S2TTP = Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R, hs|};
 	 evs \<in> certified_mail;
          S\<noteq>Spy|]
-      ==> R \<in> bad & Says TTP S (Crypt TTPSigKey S2TTP) \<in> set evs"
+      ==> R \<in> bad & Gets S (Crypt TTPSigKey S2TTP) \<in> set evs"
 apply (erule rev_mp)
 apply (erule rev_mp)
 apply (erule ssubst)
@@ -454,7 +463,7 @@
          hs = Hash {|Number cleartext, Nonce q, response S R q, 
                      Crypt K (Number m)|};
          S\<noteq>Spy;  evs \<in> certified_mail|]
-      ==> Says TTP S (Crypt TTPSigKey S2TTP) \<in> set evs"
+      ==> Gets S (Crypt TTPSigKey S2TTP) \<in> set evs"
 apply (erule rev_mp)
 apply (erule rev_mp)
 apply (erule ssubst)
@@ -468,42 +477,35 @@
 done
 
 
-lemma Says_TTP_imp_Notes:
-  "[|Says TTP S (Crypt TTPSigKey S2TTP) \<in> set evs;
-     S2TTP = Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R,
-	         Hash {|Number cleartext, Nonce q, r, em|}|};
-     evs \<in> certified_mail|]
-   ==> Notes TTP
-	   {|Agent R, Agent TTP, S2TTP, Key (RPwd R),
-	     Hash {|Number cleartext, Nonce q, r, em|}|}
-	  \<in> set evs"
-apply (erule rev_mp)
-apply (erule ssubst) 
-apply (erule certified_mail.induct, simp_all)
-done
-
-
-
 text{*Recipient's guarantee: if @{term R} sends message 2, and
-     @{term S} gets a delivery certificate, then @{term R}
+     a delivery certificate exists, then @{term R}
      receives the necessary key.*}
 theorem R_guarantee:
-  "[|Notes TTP {|Agent R, Agent TTP, S2TTP, Key(RPwd R), hr|} \<in> set evs;
-     Says TTP S (Crypt TTPSigKey S2TTP) \<in> set evs;
-     S2TTP = Crypt TTPEncKey {|Agent S, Number AO, Key K, Agent R,
-	         Hash {|Number cleartext, Nonce q, r, em|}|};
+  "[|Crypt TTPSigKey S2TTP \<in> used evs;
+     S2TTP = Crypt TTPEncKey
+               {|Agent S, Number AO, Key K, Agent R, 
+                 Hash {|Number cleartext, Nonce q, r, em|}|};
      hr = Hash {|Number cleartext, Nonce q, r, em|};
      R\<noteq>Spy;  evs \<in> certified_mail|]
   ==> Notes R {|Agent TTP, Agent R, Key K, hr|} \<in> set evs"
 apply (erule rev_mp)
-apply (erule rev_mp)
 apply (erule ssubst)
 apply (erule ssubst)
 apply (erule certified_mail.induct, simp_all)
+txt{*Fake*} 
+apply (blast dest: Fake_parts_sing[THEN subsetD]
+             dest!: analz_subset_parts[THEN subsetD])  
+txt{*Fake SSL*}
+apply (blast dest: Fake_parts_sing[THEN subsetD]
+            dest!: analz_subset_parts[THEN subsetD])  
 txt{*Message 2*}
-apply clarify
-apply (drule Says_TTP_imp_Notes [OF _ refl], assumption)
-apply simp  
+apply (drule CM2_S2TTP_parts_knows_Spy, assumption)
+apply (force dest: parts_cut)
+txt{*Message 3*}
+apply (frule_tac hr_form, assumption)
+apply (elim disjE exE, simp_all) 
+apply (blast dest: Fake_parts_sing[THEN subsetD]
+             dest!: analz_subset_parts[THEN subsetD]) 
 done
 
 end