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