simpilified and strengthened proofs
authorpaulson
Wed May 12 10:40:41 2004 +0200 (2004-05-12)
changeset 1474136582c356db7
parent 14740 c8e1937110c2
child 14742 dde816115d6a
simpilified and strengthened proofs
src/HOL/Auth/ZhouGollmann.thy
     1.1 --- a/src/HOL/Auth/ZhouGollmann.thy	Wed May 12 10:00:56 2004 +0200
     1.2 +++ b/src/HOL/Auth/ZhouGollmann.thy	Wed May 12 10:40:41 2004 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4    TTP :: agent
     1.5  
     1.6  translations
     1.7 -  "TTP" == "Server "
     1.8 +  "TTP" == " Server "
     1.9  
    1.10  syntax
    1.11    f_sub :: nat
    1.12 @@ -25,10 +25,10 @@
    1.13    f_con :: nat
    1.14  
    1.15  translations
    1.16 -  "f_sub" == "5"
    1.17 -  "f_nro" == "2"
    1.18 -  "f_nrr" == "3"
    1.19 -  "f_con" == "4"
    1.20 +  "f_sub" == " 5 "
    1.21 +  "f_nro" == " 2 "
    1.22 +  "f_nrr" == " 3 "
    1.23 +  "f_con" == " 4 "
    1.24  
    1.25  
    1.26  constdefs
    1.27 @@ -172,16 +172,16 @@
    1.28  by auto 
    1.29  
    1.30  
    1.31 -subsection{*About NRO*}
    1.32 +subsection{*About NRO: Validity for @{term B}*}
    1.33  
    1.34  text{*Below we prove that if @{term NRO} exists then @{term A} definitely
    1.35 -sent it, provided @{term A} is not broken.  *}
    1.36 +sent it, provided @{term A} is not broken.*}
    1.37  
    1.38  text{*Strong conclusion for a good agent*}
    1.39  lemma NRO_authenticity_good:
    1.40 -     "[| NRO \<in> parts (spies evs);
    1.41 -         NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
    1.42 -         A \<notin> bad;  evs \<in> zg |]
    1.43 +     "[|NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
    1.44 +        NRO \<in> parts (spies evs);
    1.45 +        A \<notin> bad;  evs \<in> zg |]
    1.46       ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs"
    1.47  apply clarify
    1.48  apply (erule rev_mp)
    1.49 @@ -189,85 +189,62 @@
    1.50  apply (frule_tac [5] ZG2_msg_in_parts_spies, auto)  
    1.51  done
    1.52  
    1.53 -text{*A compromised agent: we can't be sure whether A or the Spy sends the
    1.54 -message or of the precise form of the message*}
    1.55 -lemma NRO_authenticity_bad:
    1.56 -     "[| NRO \<in> parts (spies evs);
    1.57 -         NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
    1.58 -         A \<in> bad;  evs \<in> zg |]
    1.59 -     ==> \<exists>A' \<in> {A,Spy}. \<exists>C Y. Says A' C Y \<in> set evs & NRO \<in> parts {Y}"
    1.60 -apply clarify
    1.61 -apply (erule rev_mp)
    1.62 -apply (erule zg.induct)
    1.63 -apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
    1.64 -txt{*ZG3*}
    1.65 -   prefer 4 apply blast
    1.66 -txt{*ZG2*}
    1.67 -   prefer 3 apply blast
    1.68 -txt{*Fake*}
    1.69 -apply (simp add: parts_insert_knows_A, blast) 
    1.70 -txt{*ZG1*}
    1.71 -apply (force intro!: exI)
    1.72 -txt{*ZG4*}
    1.73 -apply (auto ); 
    1.74 +lemma NRO_sender:
    1.75 +     "[|Says A' B {|n, b, l, C, Crypt (priK A) X|} \<in> set evs; evs \<in> zg|]
    1.76 +    ==> A' \<in> {A,Spy}"
    1.77 +apply (erule rev_mp)  
    1.78 +apply (erule zg.induct, simp_all)
    1.79  done
    1.80  
    1.81 +text{*Holds also for @{term "A = Spy"}!*}
    1.82  theorem NRO_authenticity:
    1.83 -     "[| NRO \<in> used evs;
    1.84 -         NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
    1.85 -         A \<notin> broken; evs \<in> zg |]
    1.86 -     ==> \<exists>C Y. Says A C Y \<in> set evs & NRO \<in> parts {Y}"
    1.87 -apply auto
    1.88 - apply (force dest!: Crypt_used_imp_spies NRO_authenticity_good)
    1.89 -apply (force dest!: Crypt_used_imp_spies NRO_authenticity_bad)
    1.90 +     "[|Says A' B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs;
    1.91 +        NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
    1.92 +        A \<notin> broken;  evs \<in> zg |]
    1.93 +     ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs"
    1.94 +apply clarify 
    1.95 +apply (frule NRO_sender, auto)
    1.96 +txt{*We are left with the case where @{term "A' = Spy"} and  @{term "A' \<noteq> A"},
    1.97 +  i.e. @{term "A \<notin> bad"}, when we can apply @{text NRO_authenticity_good}.*}
    1.98 + apply (blast dest: NRO_authenticity_good [OF refl])
    1.99  done
   1.100  
   1.101  
   1.102 -subsection{*About NRR*}
   1.103 +subsection{*About NRR: Validity for @{term A}*}
   1.104  
   1.105  text{*Below we prove that if @{term NRR} exists then @{term B} definitely
   1.106  sent it, provided @{term B} is not broken.*}
   1.107  
   1.108  text{*Strong conclusion for a good agent*}
   1.109  lemma NRR_authenticity_good:
   1.110 -     "[| NRR \<in> parts (spies evs);
   1.111 -         NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
   1.112 -         B \<notin> bad;  evs \<in> zg |]
   1.113 +     "[|NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
   1.114 +        NRR \<in> parts (spies evs);
   1.115 +        B \<notin> bad;  evs \<in> zg |]
   1.116       ==> Says B A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
   1.117  apply clarify
   1.118  apply (erule rev_mp)
   1.119 -apply (erule zg.induct)
   1.120 +apply (erule zg.induct) 
   1.121  apply (frule_tac [5] ZG2_msg_in_parts_spies, auto)  
   1.122  done
   1.123  
   1.124 -lemma NRR_authenticity_bad:
   1.125 -     "[| NRR \<in> parts (spies evs);
   1.126 -         NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
   1.127 -         B \<in> bad;  evs \<in> zg |]
   1.128 -     ==> \<exists>B' \<in> {B,Spy}. \<exists>C Y. Says B' C Y \<in> set evs & NRR \<in> parts {Y}"
   1.129 -apply clarify
   1.130 -apply (erule rev_mp)
   1.131 -apply (erule zg.induct)
   1.132 -apply (frule_tac [5] ZG2_msg_in_parts_spies)
   1.133 -apply (simp_all del: bex_simps)
   1.134 -txt{*ZG3*}
   1.135 -   prefer 4 apply blast
   1.136 -txt{*Fake*}
   1.137 -apply (simp add: parts_insert_knows_A, blast)
   1.138 -txt{*ZG1*}
   1.139 -apply (auto simp del: bex_simps)
   1.140 -txt{*ZG2*}
   1.141 -apply (force intro!: exI)
   1.142 +lemma NRR_sender:
   1.143 +     "[|Says B' A {|n, a, l, Crypt (priK B) X|} \<in> set evs; evs \<in> zg|]
   1.144 +    ==> B' \<in> {B,Spy}"
   1.145 +apply (erule rev_mp)  
   1.146 +apply (erule zg.induct, simp_all)
   1.147  done
   1.148  
   1.149 +text{*Holds also for @{term "B = Spy"}!*}
   1.150  theorem NRR_authenticity:
   1.151 -     "[| NRR \<in> used evs;
   1.152 -         NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
   1.153 -         B \<notin> broken;  evs \<in> zg |]
   1.154 -     ==> \<exists>C Y. Says B C Y \<in> set evs & NRR \<in> parts {Y}"
   1.155 -apply auto
   1.156 - apply (force dest!: Crypt_used_imp_spies NRR_authenticity_good)
   1.157 -apply (force dest!: Crypt_used_imp_spies NRR_authenticity_bad)
   1.158 +     "[|Says B' A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs;
   1.159 +        NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
   1.160 +        B \<notin> broken; evs \<in> zg|]
   1.161 +    ==> Says B A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
   1.162 +apply clarify 
   1.163 +apply (frule NRR_sender, auto)
   1.164 +txt{*We are left with the case where @{term "B' = Spy"} and  @{term "B' \<noteq> B"},
   1.165 +  i.e. @{term "B \<notin> bad"}, when we can apply @{text NRR_authenticity_good}.*}
   1.166 + apply (blast dest: NRR_authenticity_good [OF refl])
   1.167  done
   1.168  
   1.169  
   1.170 @@ -278,10 +255,11 @@
   1.171  
   1.172  text{*Strong conclusion for a good agent*}
   1.173  lemma sub_K_authenticity_good:
   1.174 -     "[| sub_K \<in> parts (spies evs);
   1.175 -         sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   1.176 -         A \<notin> bad;  evs \<in> zg |]
   1.177 +     "[|sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   1.178 +        sub_K \<in> parts (spies evs);
   1.179 +        A \<notin> bad;  evs \<in> zg |]
   1.180       ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
   1.181 +apply clarify
   1.182  apply (erule rev_mp)
   1.183  apply (erule zg.induct)
   1.184  apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   1.185 @@ -289,37 +267,28 @@
   1.186  apply (blast dest!: Fake_parts_sing_imp_Un)
   1.187  done
   1.188  
   1.189 -text{*A compromised agent: we can't be sure whether A or the Spy sends the
   1.190 -message or of the precise form of the message*}
   1.191 -lemma sub_K_authenticity_bad:
   1.192 -     "[| sub_K \<in> parts (spies evs);
   1.193 -         sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   1.194 -         A \<in> bad;  evs \<in> zg |]
   1.195 -     ==> \<exists>A' \<in> {A,Spy}. \<exists>C Y. Says A' C Y \<in> set evs & sub_K \<in> parts {Y}"
   1.196 -apply clarify
   1.197 -apply (erule rev_mp)
   1.198 -apply (erule zg.induct)
   1.199 -apply (frule_tac [5] ZG2_msg_in_parts_spies)
   1.200 -apply (simp_all del: bex_simps)
   1.201 -txt{*Fake*}
   1.202 -apply (simp add: parts_insert_knows_A, blast)
   1.203 -txt{*ZG1*}
   1.204 -apply (auto simp del: bex_simps)
   1.205 -txt{*ZG3*}
   1.206 -apply (force intro!: exI)
   1.207 +lemma sub_K_sender:
   1.208 +     "[|Says A' TTP {|n, b, l, k, Crypt (priK A) X|} \<in> set evs;  evs \<in> zg|]
   1.209 +    ==> A' \<in> {A,Spy}"
   1.210 +apply (erule rev_mp)  
   1.211 +apply (erule zg.induct, simp_all)
   1.212  done
   1.213  
   1.214 +text{*Holds also for @{term "A = Spy"}!*}
   1.215  theorem sub_K_authenticity:
   1.216 -     "[| sub_K \<in> used evs;
   1.217 -         sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   1.218 -         A \<notin> broken;  evs \<in> zg |]
   1.219 -     ==> \<exists>C Y. Says A C Y \<in> set evs & sub_K \<in> parts {Y}"
   1.220 -apply auto
   1.221 - apply (force dest!: Crypt_used_imp_spies sub_K_authenticity_good)
   1.222 -apply (force dest!: Crypt_used_imp_spies sub_K_authenticity_bad)
   1.223 +     "[|Says A' TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs;
   1.224 +        sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   1.225 +        A \<notin> broken;  evs \<in> zg |]
   1.226 +     ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
   1.227 +apply clarify 
   1.228 +apply (frule sub_K_sender, auto)
   1.229 +txt{*We are left with the case where @{term "A' = Spy"} and  @{term "A' \<noteq> A"},
   1.230 +  i.e. @{term "A \<notin> bad"}, when we can apply @{text sub_K_authenticity_good}.*}
   1.231 + apply (blast dest: sub_K_authenticity_good [OF refl])
   1.232  done
   1.233  
   1.234  
   1.235 +
   1.236  subsection{*Proofs About @{term con_K}*}
   1.237  
   1.238  text{*Below we prove that if @{term con_K} exists, then @{term TTP} has it,
   1.239 @@ -339,7 +308,7 @@
   1.240  apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   1.241  txt{*Fake*}
   1.242  apply (blast dest!: Fake_parts_sing_imp_Un)
   1.243 -txt{*ZG2*}
   1.244 +txt{*ZG2*} 
   1.245  apply (blast dest: parts_cut)
   1.246  done
   1.247  
   1.248 @@ -351,8 +320,15 @@
   1.249             \<in> set evs;
   1.250          sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   1.251          A \<notin> broken; evs \<in> zg|]
   1.252 -    ==> \<exists>C Y. Says A C Y \<in> set evs & sub_K \<in> parts {Y}"
   1.253 -by (blast dest!: Notes_TTP_imp_Gets [THEN Gets_imp_knows_Spy, THEN parts.Inj] intro: sub_K_authenticity)
   1.254 +     ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
   1.255 +apply clarify
   1.256 +apply (erule rev_mp)
   1.257 +apply (erule zg.induct)
   1.258 +apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   1.259 +txt{*ZG4*}
   1.260 +apply (clarify dest!: Gets_imp_Says) 
   1.261 +apply (rule sub_K_authenticity, auto) 
   1.262 +done
   1.263  
   1.264  text{*If @{term con_K} exists, then @{term A} sent @{term sub_K}.  We again
   1.265     assume that @{term A} is not broken. *}
   1.266 @@ -361,8 +337,8 @@
   1.267          con_K = Crypt (priK TTP) {|Number f_con, Agent A, Agent B,
   1.268                                     Nonce L, Key K|};
   1.269          sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   1.270 -        A \<notin> broken; B \<noteq> TTP; evs \<in> zg|]
   1.271 -    ==> \<exists>C Y. Says A C Y \<in> set evs & sub_K \<in> parts {Y}"
   1.272 +        A \<notin> broken; evs \<in> zg|]
   1.273 +     ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
   1.274  by (blast dest: con_K_authenticity Notes_TTP_imp_Says_A)
   1.275  
   1.276  
   1.277 @@ -393,11 +369,11 @@
   1.278  text{*Fairness lemma: if @{term sub_K} exists, then @{term A} holds 
   1.279  NRR.  Relies on unicity of labels.*}
   1.280  lemma sub_K_implies_NRR:
   1.281 -     "[| sub_K \<in> parts (spies evs);
   1.282 +     "[| NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
   1.283 +         NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, Crypt K M|};
   1.284 +         sub_K \<in> parts (spies evs);
   1.285           NRO \<in> parts (spies evs);
   1.286           sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   1.287 -         NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
   1.288 -         NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, Crypt K M|};
   1.289           A \<notin> bad;  evs \<in> zg |]
   1.290       ==> Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
   1.291  apply clarify
   1.292 @@ -409,7 +385,7 @@
   1.293  apply blast 
   1.294  txt{*ZG1: freshness*}
   1.295  apply (blast dest: parts.Body) 
   1.296 -txt{*ZG3*}
   1.297 +txt{*ZG3*} 
   1.298  apply (blast dest: A_unicity [OF refl]) 
   1.299  done
   1.300  
   1.301 @@ -450,8 +426,8 @@
   1.302    apply (blast dest: Crypt_used_imp_L_used) 
   1.303   txt{*ZG2*}
   1.304   apply (blast dest: parts_cut)
   1.305 -txt{*ZG4*}
   1.306 -apply (blast intro: sub_K_implies_NRR [OF _ _ refl] 
   1.307 +txt{*ZG4*} 
   1.308 +apply (blast intro: sub_K_implies_NRR [OF refl] 
   1.309               dest: Gets_imp_knows_Spy [THEN parts.Inj])
   1.310  done
   1.311