src/HOL/Auth/ZhouGollmann.thy
author wenzelm
Thu Sep 28 23:42:35 2006 +0200 (2006-09-28)
changeset 20768 1d478c2d621f
parent 16417 9bc16273c2d4
child 21404 eb85850d3eb7
permissions -rw-r--r--
replaced syntax/translations by abbreviation;
     1 (*  Title:      HOL/Auth/ZhouGollmann
     2     ID:         $Id$
     3     Author:     Giampaolo Bella and L C Paulson, Cambridge Univ Computer Lab
     4     Copyright   2003  University of Cambridge
     5 
     6 The protocol of
     7   Jianying Zhou and Dieter Gollmann,
     8   A Fair Non-Repudiation Protocol,
     9   Security and Privacy 1996 (Oakland)
    10   55-61
    11 *)
    12 
    13 theory ZhouGollmann imports Public begin
    14 
    15 abbreviation
    16   TTP :: agent
    17   "TTP == Server"
    18 
    19   f_sub :: nat
    20   "f_sub == 5"
    21   f_nro :: nat
    22   "f_nro == 2"
    23   f_nrr :: nat
    24   "f_nrr == 3"
    25   f_con :: nat
    26   "f_con == 4"
    27 
    28 
    29 constdefs
    30   broken :: "agent set"    
    31     --{*the compromised honest agents; TTP is included as it's not allowed to
    32         use the protocol*}
    33    "broken == bad - {Spy}"
    34 
    35 declare broken_def [simp]
    36 
    37 consts  zg  :: "event list set"
    38 
    39 inductive zg
    40   intros
    41 
    42   Nil:  "[] \<in> zg"
    43 
    44   Fake: "[| evsf \<in> zg;  X \<in> synth (analz (spies evsf)) |]
    45 	 ==> Says Spy B X  # evsf \<in> zg"
    46 
    47 Reception:  "[| evsr \<in> zg; Says A B X \<in> set evsr |] ==> Gets B X # evsr \<in> zg"
    48 
    49   (*L is fresh for honest agents.
    50     We don't require K to be fresh because we don't bother to prove secrecy!
    51     We just assume that the protocol's objective is to deliver K fairly,
    52     rather than to keep M secret.*)
    53   ZG1: "[| evs1 \<in> zg;  Nonce L \<notin> used evs1; C = Crypt K (Number m);
    54 	   K \<in> symKeys;
    55 	   NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|}|]
    56        ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} # evs1 \<in> zg"
    57 
    58   (*B must check that NRO is A's signature to learn the sender's name*)
    59   ZG2: "[| evs2 \<in> zg;
    60 	   Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs2;
    61 	   NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
    62 	   NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|}|]
    63        ==> Says B A {|Number f_nrr, Agent A, Nonce L, NRR|} # evs2  \<in>  zg"
    64 
    65   (*A must check that NRR is B's signature to learn the sender's name;
    66     without spy, the matching label would be enough*)
    67   ZG3: "[| evs3 \<in> zg; C = Crypt K M; K \<in> symKeys;
    68 	   Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs3;
    69 	   Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs3;
    70 	   NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
    71 	   sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|}|]
    72        ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|}
    73 	     # evs3 \<in> zg"
    74 
    75  (*TTP checks that sub_K is A's signature to learn who issued K, then
    76    gives credentials to A and B.  The Notes event models the availability of
    77    the credentials, but the act of fetching them is not modelled.  We also
    78    give con_K to the Spy. This makes the threat model more dangerous, while 
    79    also allowing lemma @{text Crypt_used_imp_spies} to omit the condition
    80    @{term "K \<noteq> priK TTP"}. *)
    81   ZG4: "[| evs4 \<in> zg; K \<in> symKeys;
    82 	   Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|}
    83 	     \<in> set evs4;
    84 	   sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
    85 	   con_K = Crypt (priK TTP) {|Number f_con, Agent A, Agent B,
    86 				      Nonce L, Key K|}|]
    87        ==> Says TTP Spy con_K
    88            #
    89 	   Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
    90 	   # evs4 \<in> zg"
    91 
    92 
    93 declare Says_imp_knows_Spy [THEN analz.Inj, dest]
    94 declare Fake_parts_insert_in_Un  [dest]
    95 declare analz_into_parts [dest]
    96 
    97 declare symKey_neq_priEK [simp]
    98 declare symKey_neq_priEK [THEN not_sym, simp]
    99 
   100 
   101 text{*A "possibility property": there are traces that reach the end*}
   102 lemma "[|A \<noteq> B; TTP \<noteq> A; TTP \<noteq> B; K \<in> symKeys|] ==>
   103      \<exists>L. \<exists>evs \<in> zg.
   104            Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K,
   105                Crypt (priK TTP) {|Number f_con, Agent A, Agent B, Nonce L, Key K|} |}
   106                \<in> set evs"
   107 apply (intro exI bexI)
   108 apply (rule_tac [2] zg.Nil
   109                     [THEN zg.ZG1, THEN zg.Reception [of _ A B],
   110                      THEN zg.ZG2, THEN zg.Reception [of _ B A],
   111                      THEN zg.ZG3, THEN zg.Reception [of _ A TTP], 
   112                      THEN zg.ZG4])
   113 apply (possibility, auto)
   114 done
   115 
   116 subsection {*Basic Lemmas*}
   117 
   118 lemma Gets_imp_Says:
   119      "[| Gets B X \<in> set evs; evs \<in> zg |] ==> \<exists>A. Says A B X \<in> set evs"
   120 apply (erule rev_mp)
   121 apply (erule zg.induct, auto)
   122 done
   123 
   124 lemma Gets_imp_knows_Spy:
   125      "[| Gets B X \<in> set evs; evs \<in> zg |]  ==> X \<in> spies evs"
   126 by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
   127 
   128 
   129 text{*Lets us replace proofs about @{term "used evs"} by simpler proofs 
   130 about @{term "parts (spies evs)"}.*}
   131 lemma Crypt_used_imp_spies:
   132      "[| Crypt K X \<in> used evs; evs \<in> zg |]
   133       ==> Crypt K X \<in> parts (spies evs)"
   134 apply (erule rev_mp)
   135 apply (erule zg.induct)
   136 apply (simp_all add: parts_insert_knows_A) 
   137 done
   138 
   139 lemma Notes_TTP_imp_Gets:
   140      "[|Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K |}
   141            \<in> set evs;
   142         sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   143         evs \<in> zg|]
   144     ==> Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
   145 apply (erule rev_mp)
   146 apply (erule zg.induct, auto)
   147 done
   148 
   149 text{*For reasoning about C, which is encrypted in message ZG2*}
   150 lemma ZG2_msg_in_parts_spies:
   151      "[|Gets B {|F, B', L, C, X|} \<in> set evs; evs \<in> zg|]
   152       ==> C \<in> parts (spies evs)"
   153 by (blast dest: Gets_imp_Says)
   154 
   155 (*classical regularity lemma on priK*)
   156 lemma Spy_see_priK [simp]:
   157      "evs \<in> zg ==> (Key (priK A) \<in> parts (spies evs)) = (A \<in> bad)"
   158 apply (erule zg.induct)
   159 apply (frule_tac [5] ZG2_msg_in_parts_spies, auto)
   160 done
   161 
   162 text{*So that blast can use it too*}
   163 declare  Spy_see_priK [THEN [2] rev_iffD1, dest!]
   164 
   165 lemma Spy_analz_priK [simp]:
   166      "evs \<in> zg ==> (Key (priK A) \<in> analz (spies evs)) = (A \<in> bad)"
   167 by auto 
   168 
   169 
   170 subsection{*About NRO: Validity for @{term B}*}
   171 
   172 text{*Below we prove that if @{term NRO} exists then @{term A} definitely
   173 sent it, provided @{term A} is not broken.*}
   174 
   175 text{*Strong conclusion for a good agent*}
   176 lemma NRO_validity_good:
   177      "[|NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
   178         NRO \<in> parts (spies evs);
   179         A \<notin> bad;  evs \<in> zg |]
   180      ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs"
   181 apply clarify
   182 apply (erule rev_mp)
   183 apply (erule zg.induct)
   184 apply (frule_tac [5] ZG2_msg_in_parts_spies, auto)  
   185 done
   186 
   187 lemma NRO_sender:
   188      "[|Says A' B {|n, b, l, C, Crypt (priK A) X|} \<in> set evs; evs \<in> zg|]
   189     ==> A' \<in> {A,Spy}"
   190 apply (erule rev_mp)  
   191 apply (erule zg.induct, simp_all)
   192 done
   193 
   194 text{*Holds also for @{term "A = Spy"}!*}
   195 theorem NRO_validity:
   196      "[|Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs;
   197         NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
   198         A \<notin> broken;  evs \<in> zg |]
   199      ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs"
   200 apply (drule Gets_imp_Says, assumption) 
   201 apply clarify 
   202 apply (frule NRO_sender, auto)
   203 txt{*We are left with the case where the sender is @{term Spy} and not
   204   equal to @{term A}, because @{term "A \<notin> bad"}. 
   205   Thus theorem @{text NRO_validity_good} applies.*}
   206 apply (blast dest: NRO_validity_good [OF refl])
   207 done
   208 
   209 
   210 subsection{*About NRR: Validity for @{term A}*}
   211 
   212 text{*Below we prove that if @{term NRR} exists then @{term B} definitely
   213 sent it, provided @{term B} is not broken.*}
   214 
   215 text{*Strong conclusion for a good agent*}
   216 lemma NRR_validity_good:
   217      "[|NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
   218         NRR \<in> parts (spies evs);
   219         B \<notin> bad;  evs \<in> zg |]
   220      ==> Says B A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
   221 apply clarify
   222 apply (erule rev_mp)
   223 apply (erule zg.induct) 
   224 apply (frule_tac [5] ZG2_msg_in_parts_spies, auto)  
   225 done
   226 
   227 lemma NRR_sender:
   228      "[|Says B' A {|n, a, l, Crypt (priK B) X|} \<in> set evs; evs \<in> zg|]
   229     ==> B' \<in> {B,Spy}"
   230 apply (erule rev_mp)  
   231 apply (erule zg.induct, simp_all)
   232 done
   233 
   234 text{*Holds also for @{term "B = Spy"}!*}
   235 theorem NRR_validity:
   236      "[|Says B' A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs;
   237         NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
   238         B \<notin> broken; evs \<in> zg|]
   239     ==> Says B A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
   240 apply clarify 
   241 apply (frule NRR_sender, auto)
   242 txt{*We are left with the case where @{term "B' = Spy"} and  @{term "B' \<noteq> B"},
   243   i.e. @{term "B \<notin> bad"}, when we can apply @{text NRR_validity_good}.*}
   244  apply (blast dest: NRR_validity_good [OF refl])
   245 done
   246 
   247 
   248 subsection{*Proofs About @{term sub_K}*}
   249 
   250 text{*Below we prove that if @{term sub_K} exists then @{term A} definitely
   251 sent it, provided @{term A} is not broken.  *}
   252 
   253 text{*Strong conclusion for a good agent*}
   254 lemma sub_K_validity_good:
   255      "[|sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   256         sub_K \<in> parts (spies evs);
   257         A \<notin> bad;  evs \<in> zg |]
   258      ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
   259 apply clarify
   260 apply (erule rev_mp)
   261 apply (erule zg.induct)
   262 apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   263 txt{*Fake*} 
   264 apply (blast dest!: Fake_parts_sing_imp_Un)
   265 done
   266 
   267 lemma sub_K_sender:
   268      "[|Says A' TTP {|n, b, l, k, Crypt (priK A) X|} \<in> set evs;  evs \<in> zg|]
   269     ==> A' \<in> {A,Spy}"
   270 apply (erule rev_mp)  
   271 apply (erule zg.induct, simp_all)
   272 done
   273 
   274 text{*Holds also for @{term "A = Spy"}!*}
   275 theorem sub_K_validity:
   276      "[|Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs;
   277         sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   278         A \<notin> broken;  evs \<in> zg |]
   279      ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
   280 apply (drule Gets_imp_Says, assumption) 
   281 apply clarify 
   282 apply (frule sub_K_sender, auto)
   283 txt{*We are left with the case where the sender is @{term Spy} and not
   284   equal to @{term A}, because @{term "A \<notin> bad"}. 
   285   Thus theorem @{text sub_K_validity_good} applies.*}
   286 apply (blast dest: sub_K_validity_good [OF refl])
   287 done
   288 
   289 
   290 
   291 subsection{*Proofs About @{term con_K}*}
   292 
   293 text{*Below we prove that if @{term con_K} exists, then @{term TTP} has it,
   294 and therefore @{term A} and @{term B}) can get it too.  Moreover, we know
   295 that @{term A} sent @{term sub_K}*}
   296 
   297 lemma con_K_validity:
   298      "[|con_K \<in> used evs;
   299         con_K = Crypt (priK TTP)
   300                   {|Number f_con, Agent A, Agent B, Nonce L, Key K|};
   301         evs \<in> zg |]
   302     ==> Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
   303           \<in> set evs"
   304 apply clarify
   305 apply (erule rev_mp)
   306 apply (erule zg.induct)
   307 apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   308 txt{*Fake*}
   309 apply (blast dest!: Fake_parts_sing_imp_Un)
   310 txt{*ZG2*} 
   311 apply (blast dest: parts_cut)
   312 done
   313 
   314 text{*If @{term TTP} holds @{term con_K} then @{term A} sent
   315  @{term sub_K}.  We assume that @{term A} is not broken.  Importantly, nothing
   316   needs to be assumed about the form of @{term con_K}!*}
   317 lemma Notes_TTP_imp_Says_A:
   318      "[|Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
   319            \<in> set evs;
   320         sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   321         A \<notin> broken; evs \<in> zg|]
   322      ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
   323 apply clarify
   324 apply (erule rev_mp)
   325 apply (erule zg.induct)
   326 apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   327 txt{*ZG4*}
   328 apply clarify 
   329 apply (rule sub_K_validity, auto) 
   330 done
   331 
   332 text{*If @{term con_K} exists, then @{term A} sent @{term sub_K}.  We again
   333    assume that @{term A} is not broken. *}
   334 theorem B_sub_K_validity:
   335      "[|con_K \<in> used evs;
   336         con_K = Crypt (priK TTP) {|Number f_con, Agent A, Agent B,
   337                                    Nonce L, Key K|};
   338         sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   339         A \<notin> broken; evs \<in> zg|]
   340      ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
   341 by (blast dest: con_K_validity Notes_TTP_imp_Says_A)
   342 
   343 
   344 subsection{*Proving fairness*}
   345 
   346 text{*Cannot prove that, if @{term B} has NRO, then  @{term A} has her NRR.
   347 It would appear that @{term B} has a small advantage, though it is
   348 useless to win disputes: @{term B} needs to present @{term con_K} as well.*}
   349 
   350 text{*Strange: unicity of the label protects @{term A}?*}
   351 lemma A_unicity: 
   352      "[|NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
   353         NRO \<in> parts (spies evs);
   354         Says A B {|Number f_nro, Agent B, Nonce L, Crypt K M', NRO'|}
   355           \<in> set evs;
   356         A \<notin> bad; evs \<in> zg |]
   357      ==> M'=M"
   358 apply clarify
   359 apply (erule rev_mp)
   360 apply (erule rev_mp)
   361 apply (erule zg.induct)
   362 apply (frule_tac [5] ZG2_msg_in_parts_spies, auto) 
   363 txt{*ZG1: freshness*}
   364 apply (blast dest: parts.Body) 
   365 done
   366 
   367 
   368 text{*Fairness lemma: if @{term sub_K} exists, then @{term A} holds 
   369 NRR.  Relies on unicity of labels.*}
   370 lemma sub_K_implies_NRR:
   371      "[| NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
   372          NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, Crypt K M|};
   373          sub_K \<in> parts (spies evs);
   374          NRO \<in> parts (spies evs);
   375          sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   376          A \<notin> bad;  evs \<in> zg |]
   377      ==> Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
   378 apply clarify
   379 apply (erule rev_mp)
   380 apply (erule rev_mp)
   381 apply (erule zg.induct)
   382 apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   383 txt{*Fake*}
   384 apply blast 
   385 txt{*ZG1: freshness*}
   386 apply (blast dest: parts.Body) 
   387 txt{*ZG3*} 
   388 apply (blast dest: A_unicity [OF refl]) 
   389 done
   390 
   391 
   392 lemma Crypt_used_imp_L_used:
   393      "[| Crypt (priK TTP) {|F, A, B, L, K|} \<in> used evs; evs \<in> zg |]
   394       ==> L \<in> used evs"
   395 apply (erule rev_mp)
   396 apply (erule zg.induct, auto)
   397 txt{*Fake*}
   398 apply (blast dest!: Fake_parts_sing_imp_Un)
   399 txt{*ZG2: freshness*}
   400 apply (blast dest: parts.Body) 
   401 done
   402 
   403 
   404 text{*Fairness for @{term A}: if @{term con_K} and @{term NRO} exist, 
   405 then @{term A} holds NRR.  @{term A} must be uncompromised, but there is no
   406 assumption about @{term B}.*}
   407 theorem A_fairness_NRO:
   408      "[|con_K \<in> used evs;
   409         NRO \<in> parts (spies evs);
   410         con_K = Crypt (priK TTP)
   411                       {|Number f_con, Agent A, Agent B, Nonce L, Key K|};
   412         NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
   413         NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, Crypt K M|};
   414         A \<notin> bad;  evs \<in> zg |]
   415     ==> Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
   416 apply clarify
   417 apply (erule rev_mp)
   418 apply (erule rev_mp)
   419 apply (erule zg.induct)
   420 apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   421    txt{*Fake*}
   422    apply (simp add: parts_insert_knows_A) 
   423    apply (blast dest: Fake_parts_sing_imp_Un) 
   424   txt{*ZG1*}
   425   apply (blast dest: Crypt_used_imp_L_used) 
   426  txt{*ZG2*}
   427  apply (blast dest: parts_cut)
   428 txt{*ZG4*} 
   429 apply (blast intro: sub_K_implies_NRR [OF refl] 
   430              dest: Gets_imp_knows_Spy [THEN parts.Inj])
   431 done
   432 
   433 text{*Fairness for @{term B}: NRR exists at all, then @{term B} holds NRO.
   434 @{term B} must be uncompromised, but there is no assumption about @{term
   435 A}. *}
   436 theorem B_fairness_NRR:
   437      "[|NRR \<in> used evs;
   438         NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
   439         NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
   440         B \<notin> bad; evs \<in> zg |]
   441     ==> Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs"
   442 apply clarify
   443 apply (erule rev_mp)
   444 apply (erule zg.induct)
   445 apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   446 txt{*Fake*}
   447 apply (blast dest!: Fake_parts_sing_imp_Un)
   448 txt{*ZG2*}
   449 apply (blast dest: parts_cut)
   450 done
   451 
   452 
   453 text{*If @{term con_K} exists at all, then @{term B} can get it, by @{text
   454 con_K_validity}.  Cannot conclude that also NRO is available to @{term B},
   455 because if @{term A} were unfair, @{term A} could build message 3 without
   456 building message 1, which contains NRO. *}
   457 
   458 end