src/HOL/Auth/ZhouGollmann.thy
changeset 61830 4f5ab843cf5b
parent 57492 74bf65a1910a
child 61956 38b73f7940af
     1.1 --- a/src/HOL/Auth/ZhouGollmann.thy	Thu Dec 10 21:31:24 2015 +0100
     1.2 +++ b/src/HOL/Auth/ZhouGollmann.thy	Thu Dec 10 21:39:33 2015 +0100
     1.3 @@ -21,8 +21,8 @@
     1.4  
     1.5  
     1.6  definition broken :: "agent set" where    
     1.7 -    --{*the compromised honest agents; TTP is included as it's not allowed to
     1.8 -        use the protocol*}
     1.9 +    \<comment>\<open>the compromised honest agents; TTP is included as it's not allowed to
    1.10 +        use the protocol\<close>
    1.11     "broken == bad - {Spy}"
    1.12  
    1.13  declare broken_def [simp]
    1.14 @@ -89,7 +89,7 @@
    1.15  declare symKey_neq_priEK [THEN not_sym, simp]
    1.16  
    1.17  
    1.18 -text{*A "possibility property": there are traces that reach the end*}
    1.19 +text\<open>A "possibility property": there are traces that reach the end\<close>
    1.20  lemma "[|A \<noteq> B; TTP \<noteq> A; TTP \<noteq> B; K \<in> symKeys|] ==>
    1.21       \<exists>L. \<exists>evs \<in> zg.
    1.22             Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K,
    1.23 @@ -104,7 +104,7 @@
    1.24  apply (basic_possibility, auto)
    1.25  done
    1.26  
    1.27 -subsection {*Basic Lemmas*}
    1.28 +subsection \<open>Basic Lemmas\<close>
    1.29  
    1.30  lemma Gets_imp_Says:
    1.31       "[| Gets B X \<in> set evs; evs \<in> zg |] ==> \<exists>A. Says A B X \<in> set evs"
    1.32 @@ -117,8 +117,8 @@
    1.33  by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
    1.34  
    1.35  
    1.36 -text{*Lets us replace proofs about @{term "used evs"} by simpler proofs 
    1.37 -about @{term "parts (spies evs)"}.*}
    1.38 +text\<open>Lets us replace proofs about @{term "used evs"} by simpler proofs 
    1.39 +about @{term "parts (spies evs)"}.\<close>
    1.40  lemma Crypt_used_imp_spies:
    1.41       "[| Crypt K X \<in> used evs; evs \<in> zg |]
    1.42        ==> Crypt K X \<in> parts (spies evs)"
    1.43 @@ -137,7 +137,7 @@
    1.44  apply (erule zg.induct, auto)
    1.45  done
    1.46  
    1.47 -text{*For reasoning about C, which is encrypted in message ZG2*}
    1.48 +text\<open>For reasoning about C, which is encrypted in message ZG2\<close>
    1.49  lemma ZG2_msg_in_parts_spies:
    1.50       "[|Gets B {|F, B', L, C, X|} \<in> set evs; evs \<in> zg|]
    1.51        ==> C \<in> parts (spies evs)"
    1.52 @@ -150,7 +150,7 @@
    1.53  apply (frule_tac [5] ZG2_msg_in_parts_spies, auto)
    1.54  done
    1.55  
    1.56 -text{*So that blast can use it too*}
    1.57 +text\<open>So that blast can use it too\<close>
    1.58  declare  Spy_see_priK [THEN [2] rev_iffD1, dest!]
    1.59  
    1.60  lemma Spy_analz_priK [simp]:
    1.61 @@ -158,12 +158,12 @@
    1.62  by auto 
    1.63  
    1.64  
    1.65 -subsection{*About NRO: Validity for @{term B}*}
    1.66 +subsection\<open>About NRO: Validity for @{term B}\<close>
    1.67  
    1.68 -text{*Below we prove that if @{term NRO} exists then @{term A} definitely
    1.69 -sent it, provided @{term A} is not broken.*}
    1.70 +text\<open>Below we prove that if @{term NRO} exists then @{term A} definitely
    1.71 +sent it, provided @{term A} is not broken.\<close>
    1.72  
    1.73 -text{*Strong conclusion for a good agent*}
    1.74 +text\<open>Strong conclusion for a good agent\<close>
    1.75  lemma NRO_validity_good:
    1.76       "[|NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
    1.77          NRO \<in> parts (spies evs);
    1.78 @@ -182,7 +182,7 @@
    1.79  apply (erule zg.induct, simp_all)
    1.80  done
    1.81  
    1.82 -text{*Holds also for @{term "A = Spy"}!*}
    1.83 +text\<open>Holds also for @{term "A = Spy"}!\<close>
    1.84  theorem NRO_validity:
    1.85       "[|Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs;
    1.86          NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
    1.87 @@ -191,19 +191,19 @@
    1.88  apply (drule Gets_imp_Says, assumption) 
    1.89  apply clarify 
    1.90  apply (frule NRO_sender, auto)
    1.91 -txt{*We are left with the case where the sender is @{term Spy} and not
    1.92 +txt\<open>We are left with the case where the sender is @{term Spy} and not
    1.93    equal to @{term A}, because @{term "A \<notin> bad"}. 
    1.94 -  Thus theorem @{text NRO_validity_good} applies.*}
    1.95 +  Thus theorem \<open>NRO_validity_good\<close> applies.\<close>
    1.96  apply (blast dest: NRO_validity_good [OF refl])
    1.97  done
    1.98  
    1.99  
   1.100 -subsection{*About NRR: Validity for @{term A}*}
   1.101 +subsection\<open>About NRR: Validity for @{term A}\<close>
   1.102  
   1.103 -text{*Below we prove that if @{term NRR} exists then @{term B} definitely
   1.104 -sent it, provided @{term B} is not broken.*}
   1.105 +text\<open>Below we prove that if @{term NRR} exists then @{term B} definitely
   1.106 +sent it, provided @{term B} is not broken.\<close>
   1.107  
   1.108 -text{*Strong conclusion for a good agent*}
   1.109 +text\<open>Strong conclusion for a good agent\<close>
   1.110  lemma NRR_validity_good:
   1.111       "[|NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
   1.112          NRR \<in> parts (spies evs);
   1.113 @@ -222,7 +222,7 @@
   1.114  apply (erule zg.induct, simp_all)
   1.115  done
   1.116  
   1.117 -text{*Holds also for @{term "B = Spy"}!*}
   1.118 +text\<open>Holds also for @{term "B = Spy"}!\<close>
   1.119  theorem NRR_validity:
   1.120       "[|Says B' A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs;
   1.121          NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
   1.122 @@ -230,18 +230,18 @@
   1.123      ==> Says B A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
   1.124  apply clarify 
   1.125  apply (frule NRR_sender, auto)
   1.126 -txt{*We are left with the case where @{term "B' = Spy"} and  @{term "B' \<noteq> B"},
   1.127 -  i.e. @{term "B \<notin> bad"}, when we can apply @{text NRR_validity_good}.*}
   1.128 +txt\<open>We are left with the case where @{term "B' = Spy"} and  @{term "B' \<noteq> B"},
   1.129 +  i.e. @{term "B \<notin> bad"}, when we can apply \<open>NRR_validity_good\<close>.\<close>
   1.130   apply (blast dest: NRR_validity_good [OF refl])
   1.131  done
   1.132  
   1.133  
   1.134 -subsection{*Proofs About @{term sub_K}*}
   1.135 +subsection\<open>Proofs About @{term sub_K}\<close>
   1.136  
   1.137 -text{*Below we prove that if @{term sub_K} exists then @{term A} definitely
   1.138 -sent it, provided @{term A} is not broken.  *}
   1.139 +text\<open>Below we prove that if @{term sub_K} exists then @{term A} definitely
   1.140 +sent it, provided @{term A} is not broken.\<close>
   1.141  
   1.142 -text{*Strong conclusion for a good agent*}
   1.143 +text\<open>Strong conclusion for a good agent\<close>
   1.144  lemma sub_K_validity_good:
   1.145       "[|sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   1.146          sub_K \<in> parts (spies evs);
   1.147 @@ -251,7 +251,7 @@
   1.148  apply (erule rev_mp)
   1.149  apply (erule zg.induct)
   1.150  apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   1.151 -txt{*Fake*} 
   1.152 +txt\<open>Fake\<close> 
   1.153  apply (blast dest!: Fake_parts_sing_imp_Un)
   1.154  done
   1.155  
   1.156 @@ -262,7 +262,7 @@
   1.157  apply (erule zg.induct, simp_all)
   1.158  done
   1.159  
   1.160 -text{*Holds also for @{term "A = Spy"}!*}
   1.161 +text\<open>Holds also for @{term "A = Spy"}!\<close>
   1.162  theorem sub_K_validity:
   1.163       "[|Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs;
   1.164          sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   1.165 @@ -271,19 +271,19 @@
   1.166  apply (drule Gets_imp_Says, assumption) 
   1.167  apply clarify 
   1.168  apply (frule sub_K_sender, auto)
   1.169 -txt{*We are left with the case where the sender is @{term Spy} and not
   1.170 +txt\<open>We are left with the case where the sender is @{term Spy} and not
   1.171    equal to @{term A}, because @{term "A \<notin> bad"}. 
   1.172 -  Thus theorem @{text sub_K_validity_good} applies.*}
   1.173 +  Thus theorem \<open>sub_K_validity_good\<close> applies.\<close>
   1.174  apply (blast dest: sub_K_validity_good [OF refl])
   1.175  done
   1.176  
   1.177  
   1.178  
   1.179 -subsection{*Proofs About @{term con_K}*}
   1.180 +subsection\<open>Proofs About @{term con_K}\<close>
   1.181  
   1.182 -text{*Below we prove that if @{term con_K} exists, then @{term TTP} has it,
   1.183 +text\<open>Below we prove that if @{term con_K} exists, then @{term TTP} has it,
   1.184  and therefore @{term A} and @{term B}) can get it too.  Moreover, we know
   1.185 -that @{term A} sent @{term sub_K}*}
   1.186 +that @{term A} sent @{term sub_K}\<close>
   1.187  
   1.188  lemma con_K_validity:
   1.189       "[|con_K \<in> used evs;
   1.190 @@ -296,15 +296,15 @@
   1.191  apply (erule rev_mp)
   1.192  apply (erule zg.induct)
   1.193  apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   1.194 -txt{*Fake*}
   1.195 +txt\<open>Fake\<close>
   1.196  apply (blast dest!: Fake_parts_sing_imp_Un)
   1.197 -txt{*ZG2*} 
   1.198 +txt\<open>ZG2\<close> 
   1.199  apply (blast dest: parts_cut)
   1.200  done
   1.201  
   1.202 -text{*If @{term TTP} holds @{term con_K} then @{term A} sent
   1.203 +text\<open>If @{term TTP} holds @{term con_K} then @{term A} sent
   1.204   @{term sub_K}.  We assume that @{term A} is not broken.  Importantly, nothing
   1.205 -  needs to be assumed about the form of @{term con_K}!*}
   1.206 +  needs to be assumed about the form of @{term con_K}!\<close>
   1.207  lemma Notes_TTP_imp_Says_A:
   1.208       "[|Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
   1.209             \<in> set evs;
   1.210 @@ -315,13 +315,13 @@
   1.211  apply (erule rev_mp)
   1.212  apply (erule zg.induct)
   1.213  apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   1.214 -txt{*ZG4*}
   1.215 +txt\<open>ZG4\<close>
   1.216  apply clarify 
   1.217  apply (rule sub_K_validity, auto) 
   1.218  done
   1.219  
   1.220 -text{*If @{term con_K} exists, then @{term A} sent @{term sub_K}.  We again
   1.221 -   assume that @{term A} is not broken. *}
   1.222 +text\<open>If @{term con_K} exists, then @{term A} sent @{term sub_K}.  We again
   1.223 +   assume that @{term A} is not broken.\<close>
   1.224  theorem B_sub_K_validity:
   1.225       "[|con_K \<in> used evs;
   1.226          con_K = Crypt (priK TTP) {|Number f_con, Agent A, Agent B,
   1.227 @@ -332,13 +332,13 @@
   1.228  by (blast dest: con_K_validity Notes_TTP_imp_Says_A)
   1.229  
   1.230  
   1.231 -subsection{*Proving fairness*}
   1.232 +subsection\<open>Proving fairness\<close>
   1.233  
   1.234 -text{*Cannot prove that, if @{term B} has NRO, then  @{term A} has her NRR.
   1.235 +text\<open>Cannot prove that, if @{term B} has NRO, then  @{term A} has her NRR.
   1.236  It would appear that @{term B} has a small advantage, though it is
   1.237 -useless to win disputes: @{term B} needs to present @{term con_K} as well.*}
   1.238 +useless to win disputes: @{term B} needs to present @{term con_K} as well.\<close>
   1.239  
   1.240 -text{*Strange: unicity of the label protects @{term A}?*}
   1.241 +text\<open>Strange: unicity of the label protects @{term A}?\<close>
   1.242  lemma A_unicity: 
   1.243       "[|NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
   1.244          NRO \<in> parts (spies evs);
   1.245 @@ -351,13 +351,13 @@
   1.246  apply (erule rev_mp)
   1.247  apply (erule zg.induct)
   1.248  apply (frule_tac [5] ZG2_msg_in_parts_spies, auto) 
   1.249 -txt{*ZG1: freshness*}
   1.250 +txt\<open>ZG1: freshness\<close>
   1.251  apply (blast dest: parts.Body) 
   1.252  done
   1.253  
   1.254  
   1.255 -text{*Fairness lemma: if @{term sub_K} exists, then @{term A} holds 
   1.256 -NRR.  Relies on unicity of labels.*}
   1.257 +text\<open>Fairness lemma: if @{term sub_K} exists, then @{term A} holds 
   1.258 +NRR.  Relies on unicity of labels.\<close>
   1.259  lemma sub_K_implies_NRR:
   1.260       "[| NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
   1.261           NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, Crypt K M|};
   1.262 @@ -372,11 +372,11 @@
   1.263  apply (erule rev_mp)
   1.264  apply (erule zg.induct)
   1.265  apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   1.266 -txt{*Fake*}
   1.267 +txt\<open>Fake\<close>
   1.268  apply blast 
   1.269 -txt{*ZG1: freshness*}
   1.270 +txt\<open>ZG1: freshness\<close>
   1.271  apply (blast dest: parts.Body) 
   1.272 -txt{*ZG3*} 
   1.273 +txt\<open>ZG3\<close> 
   1.274  apply (blast dest: A_unicity [OF refl]) 
   1.275  done
   1.276  
   1.277 @@ -386,16 +386,16 @@
   1.278        ==> L \<in> used evs"
   1.279  apply (erule rev_mp)
   1.280  apply (erule zg.induct, auto)
   1.281 -txt{*Fake*}
   1.282 +txt\<open>Fake\<close>
   1.283  apply (blast dest!: Fake_parts_sing_imp_Un)
   1.284 -txt{*ZG2: freshness*}
   1.285 +txt\<open>ZG2: freshness\<close>
   1.286  apply (blast dest: parts.Body) 
   1.287  done
   1.288  
   1.289  
   1.290 -text{*Fairness for @{term A}: if @{term con_K} and @{term NRO} exist, 
   1.291 +text\<open>Fairness for @{term A}: if @{term con_K} and @{term NRO} exist, 
   1.292  then @{term A} holds NRR.  @{term A} must be uncompromised, but there is no
   1.293 -assumption about @{term B}.*}
   1.294 +assumption about @{term B}.\<close>
   1.295  theorem A_fairness_NRO:
   1.296       "[|con_K \<in> used evs;
   1.297          NRO \<in> parts (spies evs);
   1.298 @@ -410,21 +410,21 @@
   1.299  apply (erule rev_mp)
   1.300  apply (erule zg.induct)
   1.301  apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   1.302 -   txt{*Fake*}
   1.303 +   txt\<open>Fake\<close>
   1.304     apply (simp add: parts_insert_knows_A) 
   1.305     apply (blast dest: Fake_parts_sing_imp_Un) 
   1.306 -  txt{*ZG1*}
   1.307 +  txt\<open>ZG1\<close>
   1.308    apply (blast dest: Crypt_used_imp_L_used) 
   1.309 - txt{*ZG2*}
   1.310 + txt\<open>ZG2\<close>
   1.311   apply (blast dest: parts_cut)
   1.312 -txt{*ZG4*} 
   1.313 +txt\<open>ZG4\<close> 
   1.314  apply (blast intro: sub_K_implies_NRR [OF refl] 
   1.315               dest: Gets_imp_knows_Spy [THEN parts.Inj])
   1.316  done
   1.317  
   1.318 -text{*Fairness for @{term B}: NRR exists at all, then @{term B} holds NRO.
   1.319 +text\<open>Fairness for @{term B}: NRR exists at all, then @{term B} holds NRO.
   1.320  @{term B} must be uncompromised, but there is no assumption about @{term
   1.321 -A}. *}
   1.322 +A}.\<close>
   1.323  theorem B_fairness_NRR:
   1.324       "[|NRR \<in> used evs;
   1.325          NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
   1.326 @@ -435,16 +435,15 @@
   1.327  apply (erule rev_mp)
   1.328  apply (erule zg.induct)
   1.329  apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   1.330 -txt{*Fake*}
   1.331 +txt\<open>Fake\<close>
   1.332  apply (blast dest!: Fake_parts_sing_imp_Un)
   1.333 -txt{*ZG2*}
   1.334 +txt\<open>ZG2\<close>
   1.335  apply (blast dest: parts_cut)
   1.336  done
   1.337  
   1.338  
   1.339 -text{*If @{term con_K} exists at all, then @{term B} can get it, by @{text
   1.340 -con_K_validity}.  Cannot conclude that also NRO is available to @{term B},
   1.341 +text\<open>If @{term con_K} exists at all, then @{term B} can get it, by \<open>con_K_validity\<close>.  Cannot conclude that also NRO is available to @{term B},
   1.342  because if @{term A} were unfair, @{term A} could build message 3 without
   1.343 -building message 1, which contains NRO. *}
   1.344 +building message 1, which contains NRO.\<close>
   1.345  
   1.346  end