src/HOL/Auth/ZhouGollmann.thy
author paulson
Tue May 11 10:49:58 2004 +0200 (2004-05-11)
changeset 14736 7104394df99a
parent 14207 f20fbb141673
child 14741 36582c356db7
permissions -rw-r--r--
broken no longer includes TTP, and other minor changes
     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*}
   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 \<in> parts (spies evs);
   183          NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
   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 text{*A compromised agent: we can't be sure whether A or the Spy sends the
   193 message or of the precise form of the message*}
   194 lemma NRO_authenticity_bad:
   195      "[| NRO \<in> parts (spies evs);
   196          NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
   197          A \<in> bad;  evs \<in> zg |]
   198      ==> \<exists>A' \<in> {A,Spy}. \<exists>C Y. Says A' C Y \<in> set evs & NRO \<in> parts {Y}"
   199 apply clarify
   200 apply (erule rev_mp)
   201 apply (erule zg.induct)
   202 apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   203 txt{*ZG3*}
   204    prefer 4 apply blast
   205 txt{*ZG2*}
   206    prefer 3 apply blast
   207 txt{*Fake*}
   208 apply (simp add: parts_insert_knows_A, blast) 
   209 txt{*ZG1*}
   210 apply (force intro!: exI)
   211 txt{*ZG4*}
   212 apply (auto ); 
   213 done
   214 
   215 theorem NRO_authenticity:
   216      "[| NRO \<in> used evs;
   217          NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
   218          A \<notin> broken; evs \<in> zg |]
   219      ==> \<exists>C Y. Says A C Y \<in> set evs & NRO \<in> parts {Y}"
   220 apply auto
   221  apply (force dest!: Crypt_used_imp_spies NRO_authenticity_good)
   222 apply (force dest!: Crypt_used_imp_spies NRO_authenticity_bad)
   223 done
   224 
   225 
   226 subsection{*About NRR*}
   227 
   228 text{*Below we prove that if @{term NRR} exists then @{term B} definitely
   229 sent it, provided @{term B} is not broken.*}
   230 
   231 text{*Strong conclusion for a good agent*}
   232 lemma NRR_authenticity_good:
   233      "[| NRR \<in> parts (spies evs);
   234          NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
   235          B \<notin> bad;  evs \<in> zg |]
   236      ==> Says B A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
   237 apply clarify
   238 apply (erule rev_mp)
   239 apply (erule zg.induct)
   240 apply (frule_tac [5] ZG2_msg_in_parts_spies, auto)  
   241 done
   242 
   243 lemma NRR_authenticity_bad:
   244      "[| NRR \<in> parts (spies evs);
   245          NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
   246          B \<in> bad;  evs \<in> zg |]
   247      ==> \<exists>B' \<in> {B,Spy}. \<exists>C Y. Says B' C Y \<in> set evs & NRR \<in> parts {Y}"
   248 apply clarify
   249 apply (erule rev_mp)
   250 apply (erule zg.induct)
   251 apply (frule_tac [5] ZG2_msg_in_parts_spies)
   252 apply (simp_all del: bex_simps)
   253 txt{*ZG3*}
   254    prefer 4 apply blast
   255 txt{*Fake*}
   256 apply (simp add: parts_insert_knows_A, blast)
   257 txt{*ZG1*}
   258 apply (auto simp del: bex_simps)
   259 txt{*ZG2*}
   260 apply (force intro!: exI)
   261 done
   262 
   263 theorem NRR_authenticity:
   264      "[| NRR \<in> used evs;
   265          NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
   266          B \<notin> broken;  evs \<in> zg |]
   267      ==> \<exists>C Y. Says B C Y \<in> set evs & NRR \<in> parts {Y}"
   268 apply auto
   269  apply (force dest!: Crypt_used_imp_spies NRR_authenticity_good)
   270 apply (force dest!: Crypt_used_imp_spies NRR_authenticity_bad)
   271 done
   272 
   273 
   274 subsection{*Proofs About @{term sub_K}*}
   275 
   276 text{*Below we prove that if @{term sub_K} exists then @{term A} definitely
   277 sent it, provided @{term A} is not broken.  *}
   278 
   279 text{*Strong conclusion for a good agent*}
   280 lemma sub_K_authenticity_good:
   281      "[| sub_K \<in> parts (spies evs);
   282          sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   283          A \<notin> bad;  evs \<in> zg |]
   284      ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
   285 apply (erule rev_mp)
   286 apply (erule zg.induct)
   287 apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   288 txt{*Fake*} 
   289 apply (blast dest!: Fake_parts_sing_imp_Un)
   290 done
   291 
   292 text{*A compromised agent: we can't be sure whether A or the Spy sends the
   293 message or of the precise form of the message*}
   294 lemma sub_K_authenticity_bad:
   295      "[| sub_K \<in> parts (spies evs);
   296          sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   297          A \<in> bad;  evs \<in> zg |]
   298      ==> \<exists>A' \<in> {A,Spy}. \<exists>C Y. Says A' C Y \<in> set evs & sub_K \<in> parts {Y}"
   299 apply clarify
   300 apply (erule rev_mp)
   301 apply (erule zg.induct)
   302 apply (frule_tac [5] ZG2_msg_in_parts_spies)
   303 apply (simp_all del: bex_simps)
   304 txt{*Fake*}
   305 apply (simp add: parts_insert_knows_A, blast)
   306 txt{*ZG1*}
   307 apply (auto simp del: bex_simps)
   308 txt{*ZG3*}
   309 apply (force intro!: exI)
   310 done
   311 
   312 theorem sub_K_authenticity:
   313      "[| sub_K \<in> used evs;
   314          sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   315          A \<notin> broken;  evs \<in> zg |]
   316      ==> \<exists>C Y. Says A C Y \<in> set evs & sub_K \<in> parts {Y}"
   317 apply auto
   318  apply (force dest!: Crypt_used_imp_spies sub_K_authenticity_good)
   319 apply (force dest!: Crypt_used_imp_spies sub_K_authenticity_bad)
   320 done
   321 
   322 
   323 subsection{*Proofs About @{term con_K}*}
   324 
   325 text{*Below we prove that if @{term con_K} exists, then @{term TTP} has it,
   326 and therefore @{term A} and @{term B}) can get it too.  Moreover, we know
   327 that @{term A} sent @{term sub_K}*}
   328 
   329 lemma con_K_authenticity:
   330      "[|con_K \<in> used evs;
   331         con_K = Crypt (priK TTP)
   332                   {|Number f_con, Agent A, Agent B, Nonce L, Key K|};
   333         evs \<in> zg |]
   334     ==> Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
   335           \<in> set evs"
   336 apply clarify
   337 apply (erule rev_mp)
   338 apply (erule zg.induct)
   339 apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   340 txt{*Fake*}
   341 apply (blast dest!: Fake_parts_sing_imp_Un)
   342 txt{*ZG2*}
   343 apply (blast dest: parts_cut)
   344 done
   345 
   346 text{*If @{term TTP} holds @{term con_K} then @{term A} sent
   347  @{term sub_K}.  We assume that @{term A} is not broken.  Importantly, nothing
   348   needs to be assumed about the form of @{term con_K}!*}
   349 lemma Notes_TTP_imp_Says_A:
   350      "[|Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
   351            \<in> set evs;
   352         sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   353         A \<notin> broken; evs \<in> zg|]
   354     ==> \<exists>C Y. Says A C Y \<in> set evs & sub_K \<in> parts {Y}"
   355 by (blast dest!: Notes_TTP_imp_Gets [THEN Gets_imp_knows_Spy, THEN parts.Inj] intro: sub_K_authenticity)
   356 
   357 text{*If @{term con_K} exists, then @{term A} sent @{term sub_K}.  We again
   358    assume that @{term A} is not broken. *}
   359 theorem B_sub_K_authenticity:
   360      "[|con_K \<in> used evs;
   361         con_K = Crypt (priK TTP) {|Number f_con, Agent A, Agent B,
   362                                    Nonce L, Key K|};
   363         sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   364         A \<notin> broken; B \<noteq> TTP; evs \<in> zg|]
   365     ==> \<exists>C Y. Says A C Y \<in> set evs & sub_K \<in> parts {Y}"
   366 by (blast dest: con_K_authenticity Notes_TTP_imp_Says_A)
   367 
   368 
   369 subsection{*Proving fairness*}
   370 
   371 text{*Cannot prove that, if @{term B} has NRO, then  @{term A} has her NRR.
   372 It would appear that @{term B} has a small advantage, though it is
   373 useless to win disputes: @{term B} needs to present @{term con_K} as well.*}
   374 
   375 text{*Strange: unicity of the label protects @{term A}?*}
   376 lemma A_unicity: 
   377      "[|NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
   378         NRO \<in> parts (spies evs);
   379         Says A B {|Number f_nro, Agent B, Nonce L, Crypt K M', NRO'|}
   380           \<in> set evs;
   381         A \<notin> bad; evs \<in> zg |]
   382      ==> M'=M"
   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, auto) 
   388 txt{*ZG1: freshness*}
   389 apply (blast dest: parts.Body) 
   390 done
   391 
   392 
   393 text{*Fairness lemma: if @{term sub_K} exists, then @{term A} holds 
   394 NRR.  Relies on unicity of labels.*}
   395 lemma sub_K_implies_NRR:
   396      "[| sub_K \<in> parts (spies evs);
   397          NRO \<in> parts (spies evs);
   398          sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   399          NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
   400          NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, Crypt K M|};
   401          A \<notin> bad;  evs \<in> zg |]
   402      ==> Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
   403 apply clarify
   404 apply (erule rev_mp)
   405 apply (erule rev_mp)
   406 apply (erule zg.induct)
   407 apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   408 txt{*Fake*}
   409 apply blast 
   410 txt{*ZG1: freshness*}
   411 apply (blast dest: parts.Body) 
   412 txt{*ZG3*}
   413 apply (blast dest: A_unicity [OF refl]) 
   414 done
   415 
   416 
   417 lemma Crypt_used_imp_L_used:
   418      "[| Crypt (priK TTP) {|F, A, B, L, K|} \<in> used evs; evs \<in> zg |]
   419       ==> L \<in> used evs"
   420 apply (erule rev_mp)
   421 apply (erule zg.induct, auto)
   422 txt{*Fake*}
   423 apply (blast dest!: Fake_parts_sing_imp_Un)
   424 txt{*ZG2: freshness*}
   425 apply (blast dest: parts.Body) 
   426 done
   427 
   428 
   429 text{*Fairness for @{term A}: if @{term con_K} and @{term NRO} exist, 
   430 then @{term A} holds NRR.  @{term A} must be uncompromised, but there is no
   431 assumption about @{term B}.*}
   432 theorem A_fairness_NRO:
   433      "[|con_K \<in> used evs;
   434         NRO \<in> parts (spies evs);
   435         con_K = Crypt (priK TTP)
   436                       {|Number f_con, Agent A, Agent B, Nonce L, Key K|};
   437         NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
   438         NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, Crypt K M|};
   439         A \<notin> bad;  evs \<in> zg |]
   440     ==> Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
   441 apply clarify
   442 apply (erule rev_mp)
   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 (simp add: parts_insert_knows_A) 
   448    apply (blast dest: Fake_parts_sing_imp_Un) 
   449   txt{*ZG1*}
   450   apply (blast dest: Crypt_used_imp_L_used) 
   451  txt{*ZG2*}
   452  apply (blast dest: parts_cut)
   453 txt{*ZG4*}
   454 apply (blast intro: sub_K_implies_NRR [OF _ _ refl] 
   455              dest: Gets_imp_knows_Spy [THEN parts.Inj])
   456 done
   457 
   458 text{*Fairness for @{term B}: NRR exists at all, then @{term B} holds NRO.
   459 @{term B} must be uncompromised, but there is no assumption about @{term
   460 A}. *}
   461 theorem B_fairness_NRR:
   462      "[|NRR \<in> used evs;
   463         NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
   464         NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
   465         B \<notin> bad; evs \<in> zg |]
   466     ==> Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs"
   467 apply clarify
   468 apply (erule rev_mp)
   469 apply (erule zg.induct)
   470 apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   471 txt{*Fake*}
   472 apply (blast dest!: Fake_parts_sing_imp_Un)
   473 txt{*ZG2*}
   474 apply (blast dest: parts_cut)
   475 done
   476 
   477 
   478 text{*If @{term con_K} exists at all, then @{term B} can get it, by @{text
   479 con_K_authenticity}.  Cannot conclude that also NRO is available to @{term B},
   480 because if @{term A} were unfair, @{term A} could build message 3 without
   481 building message 1, which contains NRO. *}
   482 
   483 end