minor tweaks to go with the new version of the Accountability paper
authorpaulson
Tue Jul 20 14:24:23 2004 +0200 (2004-07-20)
changeset 1506858d216b32199
parent 15067 02be3516e90b
child 15069 0a0371b55a0f
minor tweaks to go with the new version of the Accountability paper
src/HOL/Auth/CertifiedEmail.thy
src/HOL/Auth/ZhouGollmann.thy
     1.1 --- a/src/HOL/Auth/CertifiedEmail.thy	Tue Jul 20 14:23:09 2004 +0200
     1.2 +++ b/src/HOL/Auth/CertifiedEmail.thy	Tue Jul 20 14:24:23 2004 +0200
     1.3 @@ -48,26 +48,26 @@
     1.4            ==> Notes TTP {|Agent Spy, Agent TTP, X|} # evsfssl \<in> certified_mail"
     1.5  
     1.6  CM1: --{*The sender approaches the recipient.  The message is a number.*}
     1.7 -"[|evs1 \<in> certified_mail;
     1.8 -   Key K \<notin> used evs1;
     1.9 -   K \<in> symKeys;
    1.10 -   Nonce q \<notin> used evs1;
    1.11 -   hs = Hash {|Number cleartext, Nonce q, response S R q, Crypt K (Number m)|};
    1.12 -   S2TTP = Crypt (pubEK TTP) {|Agent S, Number BothAuth, Key K, Agent R, hs|}|]
    1.13 - ==> Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number BothAuth, 
    1.14 -                Number cleartext, Nonce q, S2TTP|} # evs1 
    1.15 -       \<in> certified_mail"
    1.16 + "[|evs1 \<in> certified_mail;
    1.17 +    Key K \<notin> used evs1;
    1.18 +    K \<in> symKeys;
    1.19 +    Nonce q \<notin> used evs1;
    1.20 +    hs = Hash{|Number cleartext, Nonce q, response S R q, Crypt K (Number m)|};
    1.21 +    S2TTP = Crypt(pubEK TTP) {|Agent S, Number BothAuth, Key K, Agent R, hs|}|]
    1.22 +  ==> Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number BothAuth, 
    1.23 +		 Number cleartext, Nonce q, S2TTP|} # evs1 
    1.24 +	\<in> certified_mail"
    1.25  
    1.26  CM2: --{*The recipient records @{term S2TTP} while transmitting it and her
    1.27       password to @{term TTP} over an SSL channel.*}
    1.28 -"[|evs2 \<in> certified_mail;
    1.29 -   Gets R {|Agent S, Agent TTP, em, Number BothAuth, Number cleartext, 
    1.30 -            Nonce q, S2TTP|} \<in> set evs2;
    1.31 -   TTP \<noteq> R;  
    1.32 -   hr = Hash {|Number cleartext, Nonce q, response S R q, em|} |]
    1.33 - ==> 
    1.34 -  Notes TTP {|Agent R, Agent TTP, S2TTP, Key(RPwd R), hr|} # evs2
    1.35 -     \<in> certified_mail"
    1.36 + "[|evs2 \<in> certified_mail;
    1.37 +    Gets R {|Agent S, Agent TTP, em, Number BothAuth, Number cleartext, 
    1.38 +	     Nonce q, S2TTP|} \<in> set evs2;
    1.39 +    TTP \<noteq> R;  
    1.40 +    hr = Hash {|Number cleartext, Nonce q, response S R q, em|} |]
    1.41 +  ==> 
    1.42 +   Notes TTP {|Agent R, Agent TTP, S2TTP, Key(RPwd R), hr|} # evs2
    1.43 +      \<in> certified_mail"
    1.44  
    1.45  CM3: --{*@{term TTP} simultaneously reveals the key to the recipient and gives
    1.46           a receipt to the sender.  The SSL channel does not authenticate 
    1.47 @@ -79,10 +79,10 @@
    1.48      S2TTP = Crypt (pubEK TTP) 
    1.49                       {|Agent S, Number BothAuth, Key k, Agent R, hs|};
    1.50      TTP \<noteq> R;  hs = hr;  k \<in> symKeys|]
    1.51 - ==> 
    1.52 -  Notes R {|Agent TTP, Agent R, Key k, hr|} # 
    1.53 -  Gets S (Crypt (priSK TTP) S2TTP) # 
    1.54 -  Says TTP S (Crypt (priSK TTP) S2TTP) # evs3 \<in> certified_mail"
    1.55 +  ==> 
    1.56 +   Notes R {|Agent TTP, Agent R, Key k, hr|} # 
    1.57 +   Gets S (Crypt (priSK TTP) S2TTP) # 
    1.58 +   Says TTP S (Crypt (priSK TTP) S2TTP) # evs3 \<in> certified_mail"
    1.59  
    1.60  Reception:
    1.61   "[|evsr \<in> certified_mail; Says A B X \<in> set evsr|]
     2.1 --- a/src/HOL/Auth/ZhouGollmann.thy	Tue Jul 20 14:23:09 2004 +0200
     2.2 +++ b/src/HOL/Auth/ZhouGollmann.thy	Tue Jul 20 14:24:23 2004 +0200
     2.3 @@ -178,7 +178,7 @@
     2.4  sent it, provided @{term A} is not broken.*}
     2.5  
     2.6  text{*Strong conclusion for a good agent*}
     2.7 -lemma NRO_authenticity_good:
     2.8 +lemma NRO_validity_good:
     2.9       "[|NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
    2.10          NRO \<in> parts (spies evs);
    2.11          A \<notin> bad;  evs \<in> zg |]
    2.12 @@ -197,7 +197,7 @@
    2.13  done
    2.14  
    2.15  text{*Holds also for @{term "A = Spy"}!*}
    2.16 -theorem NRO_authenticity:
    2.17 +theorem NRO_validity:
    2.18       "[|Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs;
    2.19          NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
    2.20          A \<notin> broken;  evs \<in> zg |]
    2.21 @@ -207,8 +207,8 @@
    2.22  apply (frule NRO_sender, auto)
    2.23  txt{*We are left with the case where the sender is @{term Spy} and not
    2.24    equal to @{term A}, because @{term "A \<notin> bad"}. 
    2.25 -  Thus theorem @{text NRO_authenticity_good} applies.*}
    2.26 -apply (blast dest: NRO_authenticity_good [OF refl])
    2.27 +  Thus theorem @{text NRO_validity_good} applies.*}
    2.28 +apply (blast dest: NRO_validity_good [OF refl])
    2.29  done
    2.30  
    2.31  
    2.32 @@ -218,7 +218,7 @@
    2.33  sent it, provided @{term B} is not broken.*}
    2.34  
    2.35  text{*Strong conclusion for a good agent*}
    2.36 -lemma NRR_authenticity_good:
    2.37 +lemma NRR_validity_good:
    2.38       "[|NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
    2.39          NRR \<in> parts (spies evs);
    2.40          B \<notin> bad;  evs \<in> zg |]
    2.41 @@ -237,7 +237,7 @@
    2.42  done
    2.43  
    2.44  text{*Holds also for @{term "B = Spy"}!*}
    2.45 -theorem NRR_authenticity:
    2.46 +theorem NRR_validity:
    2.47       "[|Says B' A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs;
    2.48          NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
    2.49          B \<notin> broken; evs \<in> zg|]
    2.50 @@ -245,8 +245,8 @@
    2.51  apply clarify 
    2.52  apply (frule NRR_sender, auto)
    2.53  txt{*We are left with the case where @{term "B' = Spy"} and  @{term "B' \<noteq> B"},
    2.54 -  i.e. @{term "B \<notin> bad"}, when we can apply @{text NRR_authenticity_good}.*}
    2.55 - apply (blast dest: NRR_authenticity_good [OF refl])
    2.56 +  i.e. @{term "B \<notin> bad"}, when we can apply @{text NRR_validity_good}.*}
    2.57 + apply (blast dest: NRR_validity_good [OF refl])
    2.58  done
    2.59  
    2.60  
    2.61 @@ -256,7 +256,7 @@
    2.62  sent it, provided @{term A} is not broken.  *}
    2.63  
    2.64  text{*Strong conclusion for a good agent*}
    2.65 -lemma sub_K_authenticity_good:
    2.66 +lemma sub_K_validity_good:
    2.67       "[|sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
    2.68          sub_K \<in> parts (spies evs);
    2.69          A \<notin> bad;  evs \<in> zg |]
    2.70 @@ -277,7 +277,7 @@
    2.71  done
    2.72  
    2.73  text{*Holds also for @{term "A = Spy"}!*}
    2.74 -theorem sub_K_authenticity:
    2.75 +theorem sub_K_validity:
    2.76       "[|Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs;
    2.77          sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
    2.78          A \<notin> broken;  evs \<in> zg |]
    2.79 @@ -287,8 +287,8 @@
    2.80  apply (frule sub_K_sender, auto)
    2.81  txt{*We are left with the case where the sender is @{term Spy} and not
    2.82    equal to @{term A}, because @{term "A \<notin> bad"}. 
    2.83 -  Thus theorem @{text sub_K_authenticity_good} applies.*}
    2.84 -apply (blast dest: sub_K_authenticity_good [OF refl])
    2.85 +  Thus theorem @{text sub_K_validity_good} applies.*}
    2.86 +apply (blast dest: sub_K_validity_good [OF refl])
    2.87  done
    2.88  
    2.89  
    2.90 @@ -299,7 +299,7 @@
    2.91  and therefore @{term A} and @{term B}) can get it too.  Moreover, we know
    2.92  that @{term A} sent @{term sub_K}*}
    2.93  
    2.94 -lemma con_K_authenticity:
    2.95 +lemma con_K_validity:
    2.96       "[|con_K \<in> used evs;
    2.97          con_K = Crypt (priK TTP)
    2.98                    {|Number f_con, Agent A, Agent B, Nonce L, Key K|};
    2.99 @@ -331,19 +331,19 @@
   2.100  apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   2.101  txt{*ZG4*}
   2.102  apply clarify 
   2.103 -apply (rule sub_K_authenticity, auto) 
   2.104 +apply (rule sub_K_validity, auto) 
   2.105  done
   2.106  
   2.107  text{*If @{term con_K} exists, then @{term A} sent @{term sub_K}.  We again
   2.108     assume that @{term A} is not broken. *}
   2.109 -theorem B_sub_K_authenticity:
   2.110 +theorem B_sub_K_validity:
   2.111       "[|con_K \<in> used evs;
   2.112          con_K = Crypt (priK TTP) {|Number f_con, Agent A, Agent B,
   2.113                                     Nonce L, Key K|};
   2.114          sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   2.115          A \<notin> broken; evs \<in> zg|]
   2.116       ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
   2.117 -by (blast dest: con_K_authenticity Notes_TTP_imp_Says_A)
   2.118 +by (blast dest: con_K_validity Notes_TTP_imp_Says_A)
   2.119  
   2.120  
   2.121  subsection{*Proving fairness*}
   2.122 @@ -456,7 +456,7 @@
   2.123  
   2.124  
   2.125  text{*If @{term con_K} exists at all, then @{term B} can get it, by @{text
   2.126 -con_K_authenticity}.  Cannot conclude that also NRO is available to @{term B},
   2.127 +con_K_validity}.  Cannot conclude that also NRO is available to @{term B},
   2.128  because if @{term A} were unfair, @{term A} could build message 3 without
   2.129  building message 1, which contains NRO. *}
   2.130