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