src/HOL/Auth/ZhouGollmann.thy
author paulson
Tue Aug 12 13:35:03 2003 +0200 (2003-08-12)
changeset 14145 2e31b8cc8788
child 14146 0edd2d57eaf8
permissions -rw-r--r--
ZhouGollmann: new example (fair non-repudiation protocol)
     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 == insert TTP (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; A \<noteq> B; Says A B X \<in> set evsr |]
    53 	     ==> Gets B X # evsr \<in> zg"
    54 
    55   (*L is fresh for honest agents.
    56     We don't require K to be fresh because we don't bother to prove secrecy!
    57     We just assume that the protocol's objective is to deliver K fairly,
    58     rather than to keep M secret.*)
    59   ZG1: "[| evs1 \<in> zg;  Nonce L \<notin> used evs1; C = Crypt K (Number m);
    60 	   K \<in> symKeys;
    61 	   NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|}|]
    62        ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} # evs1 \<in> zg"
    63 
    64   (*B must check that NRO is A's signature to learn the sender's name*)
    65   ZG2: "[| evs2 \<in> zg;
    66 	   Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs2;
    67 	   NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
    68 	   NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|}|]
    69        ==> Says B A {|Number f_nrr, Agent A, Nonce L, NRR|} # evs2  \<in>  zg"
    70 
    71   (*K is symmetric must be repeated IF there's spy*)
    72   (*A must check that NRR is B's signature to learn the sender's name*)
    73   (*without spy, the matching label would be enough*)
    74   ZG3: "[| evs3 \<in> zg; C = Crypt K M; K \<in> symKeys;
    75 	   Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs3;
    76 	   Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs3;
    77 	   NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
    78 	   sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|}|]
    79        ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|}
    80 	     # evs3 \<in> zg"
    81 
    82  (*TTP checks that sub_K is A's signature to learn who issued K, then
    83    gives credentials to A and B.  The Notes event models the availability of
    84    the credentials, but the act of fetching them is not modelled.*)
    85  (*Also said TTP_prepare_ftp*)
    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        ==> Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
    93 	     # evs4 \<in> zg"
    94 
    95 
    96 declare Says_imp_knows_Spy [THEN analz.Inj, dest]
    97 declare Fake_parts_insert_in_Un  [dest]
    98 declare analz_into_parts [dest]
    99 
   100 declare symKey_neq_priEK [simp]
   101 declare symKey_neq_priEK [THEN not_sym, simp]
   102 
   103 
   104 subsection {*Basic Lemmas*}
   105 
   106 lemma Gets_imp_Says:
   107      "[| Gets B X \<in> set evs; evs \<in> zg |] ==> \<exists>A. Says A B X \<in> set evs"
   108 apply (erule rev_mp)
   109 apply (erule zg.induct, auto)
   110 done
   111 
   112 lemma Gets_imp_knows_Spy:
   113      "[| Gets B X \<in> set evs; evs \<in> zg |]  ==> X \<in> spies evs"
   114 by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
   115 
   116 
   117 text{*Lets us replace proofs about @{term "used evs"} by simpler proofs 
   118 about @{term "parts (spies evs)"}.*}
   119 lemma Crypt_used_imp_spies:
   120      "[| Crypt K X \<in> used evs;  K \<noteq> priK TTP; evs \<in> zg |]
   121       ==> Crypt K X \<in> parts (spies evs)"
   122 apply (erule rev_mp)
   123 apply (erule zg.induct)
   124 apply (simp_all add: parts_insert_knows_A) 
   125 done
   126 
   127 lemma Notes_TTP_imp_Gets:
   128      "[|Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K |}
   129            \<in> set evs;
   130         sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   131         evs \<in> zg|]
   132     ==> Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
   133 apply (erule rev_mp)
   134 apply (erule zg.induct, auto)
   135 done
   136 
   137 text{*For reasoning about C, which is encrypted in message ZG2*}
   138 lemma ZG2_msg_in_parts_spies:
   139      "[|Gets B {|F, B', L, C, X|} \<in> set evs; evs \<in> zg|]
   140       ==> C \<in> parts (spies evs)"
   141 by (blast dest: Gets_imp_Says)
   142 
   143 (*classical regularity lemma on priK*)
   144 lemma Spy_see_priK [simp]:
   145      "evs \<in> zg ==> (Key (priK A) \<in> parts (spies evs)) = (A \<in> bad)"
   146 apply (erule zg.induct)
   147 apply (frule_tac [5] ZG2_msg_in_parts_spies, auto)
   148 done
   149 
   150 text{*So that blast can use it too*}
   151 declare  Spy_see_priK [THEN [2] rev_iffD1, dest!]
   152 
   153 lemma Spy_analz_priK [simp]:
   154      "evs \<in> zg ==> (Key (priK A) \<in> analz (spies evs)) = (A \<in> bad)"
   155 by auto 
   156 
   157 
   158 subsection{*About NRO*}
   159 
   160 text{*Below we prove that if @{term NRO} exists then @{term A} definitely
   161 sent it, provided @{term A} is not broken.  *}
   162 
   163 text{*Strong conclusion for a good agent*}
   164 lemma NRO_authenticity_good:
   165      "[| NRO \<in> parts (spies evs);
   166          NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
   167          A \<notin> bad;  evs \<in> zg |]
   168      ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs"
   169 apply clarify
   170 apply (erule rev_mp)
   171 apply (erule zg.induct)
   172 apply (frule_tac [5] ZG2_msg_in_parts_spies, auto)  
   173 done
   174 
   175 text{*A compromised agent: we can't be sure whether A or the Spy sends the
   176 message or of the precise form of the message*}
   177 lemma NRO_authenticity_bad:
   178      "[| NRO \<in> parts (spies evs);
   179          NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
   180          A \<in> bad;  evs \<in> zg |]
   181      ==> \<exists>A' \<in> {A,Spy}. \<exists>C Y. Says A' C Y \<in> set evs & NRO \<in> parts {Y}"
   182 apply clarify
   183 apply (erule rev_mp)
   184 apply (erule zg.induct)
   185 apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   186 txt{*ZG3*}
   187    prefer 4 apply blast
   188 txt{*ZG2*}
   189    prefer 3 apply blast
   190 txt{*Fake*}
   191 apply (simp add: parts_insert_knows_A, blast) 
   192 txt{*ZG1*}
   193 apply (auto intro!: exI)
   194 done
   195 
   196 theorem NRO_authenticity:
   197      "[| NRO \<in> used evs;
   198          NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
   199          A \<notin> broken;  evs \<in> zg |]
   200      ==> \<exists>C Y. Says A C Y \<in> set evs & NRO \<in> parts {Y}"
   201 apply auto
   202  apply (force dest!: Crypt_used_imp_spies NRO_authenticity_good)
   203 apply (force dest!: Crypt_used_imp_spies NRO_authenticity_bad)
   204 done
   205 
   206 
   207 subsection{*About NRR*}
   208 
   209 text{*Below we prove that if @{term NRR} exists then @{term B} definitely
   210 sent it, provided @{term B} is not broken.*}
   211 
   212 text{*Strong conclusion for a good agent*}
   213 lemma NRR_authenticity_good:
   214      "[| NRR \<in> parts (spies evs);
   215          NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
   216          B \<notin> bad;  evs \<in> zg |]
   217      ==> Says B A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
   218 apply clarify
   219 apply (erule rev_mp)
   220 apply (erule zg.induct)
   221 apply (frule_tac [5] ZG2_msg_in_parts_spies, auto)  
   222 done
   223 
   224 lemma NRR_authenticity_bad:
   225      "[| NRR \<in> parts (spies evs);
   226          NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
   227          B \<in> bad;  evs \<in> zg |]
   228      ==> \<exists>B' \<in> {B,Spy}. \<exists>C Y. Says B' C Y \<in> set evs & NRR \<in> parts {Y}"
   229 apply clarify
   230 apply (erule rev_mp)
   231 apply (erule zg.induct)
   232 apply (frule_tac [5] ZG2_msg_in_parts_spies)
   233 apply (simp_all del: bex_simps)
   234 txt{*ZG3*}
   235    prefer 4 apply blast
   236 txt{*Fake*}
   237 apply (simp add: parts_insert_knows_A, blast)
   238 txt{*ZG1*}
   239 apply (auto simp del: bex_simps)
   240 txt{*ZG2*}
   241 apply (force intro!: exI)
   242 done
   243 
   244 theorem NRR_authenticity:
   245      "[| NRR \<in> used evs;
   246          NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
   247          B \<notin> broken;  evs \<in> zg |]
   248      ==> \<exists>C Y. Says B C Y \<in> set evs & NRR \<in> parts {Y}"
   249 apply auto
   250  apply (force dest!: Crypt_used_imp_spies NRR_authenticity_good)
   251 apply (force dest!: Crypt_used_imp_spies NRR_authenticity_bad)
   252 done
   253 
   254 
   255 subsection{*Proofs About @{term sub_K}*}
   256 
   257 text{*Below we prove that if @{term sub_K} exists then @{term A} definitely
   258 sent it, provided @{term A} is not broken.  *}
   259 
   260 text{*Strong conclusion for a good agent*}
   261 lemma sub_K_authenticity_good:
   262      "[| sub_K \<in> parts (spies evs);
   263          sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   264          A \<notin> bad;  evs \<in> zg |]
   265      ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
   266 apply (erule rev_mp)
   267 apply (erule zg.induct)
   268 apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   269 txt{*Fake*} 
   270 apply (blast dest!: Fake_parts_sing_imp_Un)
   271 done
   272 
   273 text{*A compromised agent: we can't be sure whether A or the Spy sends the
   274 message or of the precise form of the message*}
   275 lemma sub_K_authenticity_bad:
   276      "[| sub_K \<in> parts (spies evs);
   277          sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   278          A \<in> bad;  evs \<in> zg |]
   279      ==> \<exists>A' \<in> {A,Spy}. \<exists>C Y. Says A' C Y \<in> set evs & sub_K \<in> parts {Y}"
   280 apply clarify
   281 apply (erule rev_mp)
   282 apply (erule zg.induct)
   283 apply (frule_tac [5] ZG2_msg_in_parts_spies)
   284 apply (simp_all del: bex_simps)
   285 txt{*Fake*}
   286 apply (simp add: parts_insert_knows_A, blast)
   287 txt{*ZG1*}
   288 apply (auto simp del: bex_simps)
   289 txt{*ZG3*}
   290 apply (force intro!: exI)
   291 done
   292 
   293 theorem sub_K_authenticity:
   294      "[| sub_K \<in> used evs;
   295          sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   296          A \<notin> broken;  evs \<in> zg |]
   297      ==> \<exists>C Y. Says A C Y \<in> set evs & sub_K \<in> parts {Y}"
   298 apply auto
   299  apply (force dest!: Crypt_used_imp_spies sub_K_authenticity_good)
   300 apply (force dest!: Crypt_used_imp_spies sub_K_authenticity_bad)
   301 done
   302 
   303 
   304 subsection{*Proofs About @{term con_K}*}
   305 
   306 text{*Below we prove that if @{term con_K} exists, then @{term TTP} has it,
   307 and therefore @{term A} and @{term B}) can get it too.  Moreover, we know
   308 that @{term A} sent @{term sub_K}*}
   309 
   310 lemma con_K_authenticity:
   311      "[|con_K \<in> used evs;
   312         con_K = Crypt (priK TTP)
   313                   {|Number f_con, Agent A, Agent B, Nonce L, Key K|};
   314         evs \<in> zg |]
   315     ==> Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
   316           \<in> set evs"
   317 apply clarify
   318 apply (erule rev_mp)
   319 apply (erule zg.induct)
   320 apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   321 txt{*Fake*}
   322 apply (blast dest!: Fake_parts_sing_imp_Un)
   323 txt{*ZG2*}
   324 apply (blast dest: parts_cut)
   325 done
   326 
   327 text{*If @{term TTP} holds @{term con_K} then @{term A} sent
   328  @{term sub_K}.  We assume that @{term A} is not broken.  Nothing needs to
   329  be assumed about the form of @{term con_K}!*}
   330 lemma Notes_TTP_imp_Says_A:
   331      "[|Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
   332            \<in> set evs;
   333         sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   334         A \<notin> broken; evs \<in> zg|]
   335     ==> \<exists>C Y. Says A C Y \<in> set evs & sub_K \<in> parts {Y}"
   336 by (blast dest!: Notes_TTP_imp_Gets [THEN Gets_imp_knows_Spy, THEN parts.Inj] intro: sub_K_authenticity)
   337 
   338 text{*If @{term con_K} exists, then @{term A} sent @{term sub_K}.*}
   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; B \<noteq> TTP; evs \<in> zg|]
   345     ==> \<exists>C Y. Says A C Y \<in> set evs & sub_K \<in> parts {Y}"
   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      "[| sub_K \<in> parts (spies evs);
   377          NRO \<in> parts (spies evs);
   378          sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   379          NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
   380          NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, Crypt K M|};
   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