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