# HG changeset patch
# User paulson
# Date 1090326263 -7200
# Node ID 58d216b32199b4f515932d033fe5db3301e82a95
# Parent  02be3516e90b56d59c80107dc75beca802d3b5b7
minor tweaks to go with the new version of the Accountability paper

diff -r 02be3516e90b -r 58d216b32199 src/HOL/Auth/CertifiedEmail.thy
--- a/src/HOL/Auth/CertifiedEmail.thy	Tue Jul 20 14:23:09 2004 +0200
+++ b/src/HOL/Auth/CertifiedEmail.thy	Tue Jul 20 14:24:23 2004 +0200
@@ -48,26 +48,26 @@
           ==> Notes TTP {|Agent Spy, Agent TTP, X|} # evsfssl \<in> certified_mail"
 
 CM1: --{*The sender approaches the recipient.  The message is a number.*}
-"[|evs1 \<in> certified_mail;
-   Key K \<notin> used evs1;
-   K \<in> symKeys;
-   Nonce q \<notin> used evs1;
-   hs = Hash {|Number cleartext, Nonce q, response S R q, Crypt K (Number m)|};
-   S2TTP = Crypt (pubEK TTP) {|Agent S, Number BothAuth, Key K, Agent R, hs|}|]
- ==> Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number BothAuth, 
-                Number cleartext, Nonce q, S2TTP|} # evs1 
-       \<in> certified_mail"
+ "[|evs1 \<in> certified_mail;
+    Key K \<notin> used evs1;
+    K \<in> symKeys;
+    Nonce q \<notin> used evs1;
+    hs = Hash{|Number cleartext, Nonce q, response S R q, Crypt K (Number m)|};
+    S2TTP = Crypt(pubEK TTP) {|Agent S, Number BothAuth, Key K, Agent R, hs|}|]
+  ==> Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number BothAuth, 
+		 Number cleartext, Nonce q, S2TTP|} # evs1 
+	\<in> certified_mail"
 
 CM2: --{*The recipient records @{term S2TTP} while transmitting it and her
      password to @{term TTP} over an SSL channel.*}
-"[|evs2 \<in> certified_mail;
-   Gets R {|Agent S, Agent TTP, em, Number BothAuth, Number cleartext, 
-            Nonce q, S2TTP|} \<in> set evs2;
-   TTP \<noteq> R;  
-   hr = Hash {|Number cleartext, Nonce q, response S R q, em|} |]
- ==> 
-  Notes TTP {|Agent R, Agent TTP, S2TTP, Key(RPwd R), hr|} # evs2
-     \<in> certified_mail"
+ "[|evs2 \<in> certified_mail;
+    Gets R {|Agent S, Agent TTP, em, Number BothAuth, Number cleartext, 
+	     Nonce q, S2TTP|} \<in> set evs2;
+    TTP \<noteq> R;  
+    hr = Hash {|Number cleartext, Nonce q, response S R q, em|} |]
+  ==> 
+   Notes TTP {|Agent R, Agent TTP, S2TTP, Key(RPwd R), hr|} # evs2
+      \<in> certified_mail"
 
 CM3: --{*@{term TTP} simultaneously reveals the key to the recipient and gives
          a receipt to the sender.  The SSL channel does not authenticate 
@@ -79,10 +79,10 @@
     S2TTP = Crypt (pubEK TTP) 
                      {|Agent S, Number BothAuth, Key k, Agent R, hs|};
     TTP \<noteq> R;  hs = hr;  k \<in> symKeys|]
- ==> 
-  Notes R {|Agent TTP, Agent R, Key k, hr|} # 
-  Gets S (Crypt (priSK TTP) S2TTP) # 
-  Says TTP S (Crypt (priSK TTP) S2TTP) # evs3 \<in> certified_mail"
+  ==> 
+   Notes R {|Agent TTP, Agent R, Key k, hr|} # 
+   Gets S (Crypt (priSK TTP) S2TTP) # 
+   Says TTP S (Crypt (priSK TTP) S2TTP) # evs3 \<in> certified_mail"
 
 Reception:
  "[|evsr \<in> certified_mail; Says A B X \<in> set evsr|]
diff -r 02be3516e90b -r 58d216b32199 src/HOL/Auth/ZhouGollmann.thy
--- a/src/HOL/Auth/ZhouGollmann.thy	Tue Jul 20 14:23:09 2004 +0200
+++ b/src/HOL/Auth/ZhouGollmann.thy	Tue Jul 20 14:24:23 2004 +0200
@@ -178,7 +178,7 @@
 sent it, provided @{term A} is not broken.*}
 
 text{*Strong conclusion for a good agent*}
-lemma NRO_authenticity_good:
+lemma NRO_validity_good:
      "[|NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
         NRO \<in> parts (spies evs);
         A \<notin> bad;  evs \<in> zg |]
@@ -197,7 +197,7 @@
 done
 
 text{*Holds also for @{term "A = Spy"}!*}
-theorem NRO_authenticity:
+theorem NRO_validity:
      "[|Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs;
         NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
         A \<notin> broken;  evs \<in> zg |]
@@ -207,8 +207,8 @@
 apply (frule NRO_sender, auto)
 txt{*We are left with the case where the sender is @{term Spy} and not
   equal to @{term A}, because @{term "A \<notin> bad"}. 
-  Thus theorem @{text NRO_authenticity_good} applies.*}
-apply (blast dest: NRO_authenticity_good [OF refl])
+  Thus theorem @{text NRO_validity_good} applies.*}
+apply (blast dest: NRO_validity_good [OF refl])
 done
 
 
@@ -218,7 +218,7 @@
 sent it, provided @{term B} is not broken.*}
 
 text{*Strong conclusion for a good agent*}
-lemma NRR_authenticity_good:
+lemma NRR_validity_good:
      "[|NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
         NRR \<in> parts (spies evs);
         B \<notin> bad;  evs \<in> zg |]
@@ -237,7 +237,7 @@
 done
 
 text{*Holds also for @{term "B = Spy"}!*}
-theorem NRR_authenticity:
+theorem NRR_validity:
      "[|Says B' A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs;
         NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
         B \<notin> broken; evs \<in> zg|]
@@ -245,8 +245,8 @@
 apply clarify 
 apply (frule NRR_sender, auto)
 txt{*We are left with the case where @{term "B' = Spy"} and  @{term "B' \<noteq> B"},
-  i.e. @{term "B \<notin> bad"}, when we can apply @{text NRR_authenticity_good}.*}
- apply (blast dest: NRR_authenticity_good [OF refl])
+  i.e. @{term "B \<notin> bad"}, when we can apply @{text NRR_validity_good}.*}
+ apply (blast dest: NRR_validity_good [OF refl])
 done
 
 
@@ -256,7 +256,7 @@
 sent it, provided @{term A} is not broken.  *}
 
 text{*Strong conclusion for a good agent*}
-lemma sub_K_authenticity_good:
+lemma sub_K_validity_good:
      "[|sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
         sub_K \<in> parts (spies evs);
         A \<notin> bad;  evs \<in> zg |]
@@ -277,7 +277,7 @@
 done
 
 text{*Holds also for @{term "A = Spy"}!*}
-theorem sub_K_authenticity:
+theorem sub_K_validity:
      "[|Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs;
         sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
         A \<notin> broken;  evs \<in> zg |]
@@ -287,8 +287,8 @@
 apply (frule sub_K_sender, auto)
 txt{*We are left with the case where the sender is @{term Spy} and not
   equal to @{term A}, because @{term "A \<notin> bad"}. 
-  Thus theorem @{text sub_K_authenticity_good} applies.*}
-apply (blast dest: sub_K_authenticity_good [OF refl])
+  Thus theorem @{text sub_K_validity_good} applies.*}
+apply (blast dest: sub_K_validity_good [OF refl])
 done
 
 
@@ -299,7 +299,7 @@
 and therefore @{term A} and @{term B}) can get it too.  Moreover, we know
 that @{term A} sent @{term sub_K}*}
 
-lemma con_K_authenticity:
+lemma con_K_validity:
      "[|con_K \<in> used evs;
         con_K = Crypt (priK TTP)
                   {|Number f_con, Agent A, Agent B, Nonce L, Key K|};
@@ -331,19 +331,19 @@
 apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
 txt{*ZG4*}
 apply clarify 
-apply (rule sub_K_authenticity, auto) 
+apply (rule sub_K_validity, auto) 
 done
 
 text{*If @{term con_K} exists, then @{term A} sent @{term sub_K}.  We again
    assume that @{term A} is not broken. *}
-theorem B_sub_K_authenticity:
+theorem B_sub_K_validity:
      "[|con_K \<in> used evs;
         con_K = Crypt (priK TTP) {|Number f_con, Agent A, Agent B,
                                    Nonce L, Key K|};
         sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
         A \<notin> broken; evs \<in> zg|]
      ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
-by (blast dest: con_K_authenticity Notes_TTP_imp_Says_A)
+by (blast dest: con_K_validity Notes_TTP_imp_Says_A)
 
 
 subsection{*Proving fairness*}
@@ -456,7 +456,7 @@
 
 
 text{*If @{term con_K} exists at all, then @{term B} can get it, by @{text
-con_K_authenticity}.  Cannot conclude that also NRO is available to @{term B},
+con_K_validity}.  Cannot conclude that also NRO is available to @{term B},
 because if @{term A} were unfair, @{term A} could build message 3 without
 building message 1, which contains NRO. *}