src/HOL/Auth/ZhouGollmann.thy
author paulson
Fri Sep 26 10:34:28 2003 +0200 (2003-09-26)
changeset 14207 f20fbb141673
parent 14146 0edd2d57eaf8
child 14736 7104394df99a
permissions -rw-r--r--
Conversion of all main protocols from "Shared" to "Public".
Removal of Key_supply_ax: modifications to possibility theorems.
Improved presentation.
     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 text{*A "possibility property": there are traces that reach the end*}
   105 lemma "[|A \<noteq> B; TTP \<noteq> A; TTP \<noteq> B; K \<in> symKeys|] ==>
   106      \<exists>L. \<exists>evs \<in> zg.
   107            Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K,
   108                Crypt (priK TTP) {|Number f_con, Agent A, Agent B, Nonce L, Key K|} |}
   109                \<in> set evs"
   110 apply (intro exI bexI)
   111 apply (rule_tac [2] zg.Nil
   112                     [THEN zg.ZG1, THEN zg.Reception [of _ A B],
   113                      THEN zg.ZG2, THEN zg.Reception [of _ B A],
   114                      THEN zg.ZG3, THEN zg.Reception [of _ A TTP], 
   115                      THEN zg.ZG4])
   116 apply (possibility, auto)
   117 done
   118 
   119 subsection {*Basic Lemmas*}
   120 
   121 lemma Gets_imp_Says:
   122      "[| Gets B X \<in> set evs; evs \<in> zg |] ==> \<exists>A. Says A B X \<in> set evs"
   123 apply (erule rev_mp)
   124 apply (erule zg.induct, auto)
   125 done
   126 
   127 lemma Gets_imp_knows_Spy:
   128      "[| Gets B X \<in> set evs; evs \<in> zg |]  ==> X \<in> spies evs"
   129 by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
   130 
   131 
   132 text{*Lets us replace proofs about @{term "used evs"} by simpler proofs 
   133 about @{term "parts (spies evs)"}.*}
   134 lemma Crypt_used_imp_spies:
   135      "[| Crypt K X \<in> used evs;  K \<noteq> priK TTP; evs \<in> zg |]
   136       ==> Crypt K X \<in> parts (spies evs)"
   137 apply (erule rev_mp)
   138 apply (erule zg.induct)
   139 apply (simp_all add: parts_insert_knows_A) 
   140 done
   141 
   142 lemma Notes_TTP_imp_Gets:
   143      "[|Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K |}
   144            \<in> set evs;
   145         sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   146         evs \<in> zg|]
   147     ==> Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
   148 apply (erule rev_mp)
   149 apply (erule zg.induct, auto)
   150 done
   151 
   152 text{*For reasoning about C, which is encrypted in message ZG2*}
   153 lemma ZG2_msg_in_parts_spies:
   154      "[|Gets B {|F, B', L, C, X|} \<in> set evs; evs \<in> zg|]
   155       ==> C \<in> parts (spies evs)"
   156 by (blast dest: Gets_imp_Says)
   157 
   158 (*classical regularity lemma on priK*)
   159 lemma Spy_see_priK [simp]:
   160      "evs \<in> zg ==> (Key (priK A) \<in> parts (spies evs)) = (A \<in> bad)"
   161 apply (erule zg.induct)
   162 apply (frule_tac [5] ZG2_msg_in_parts_spies, auto)
   163 done
   164 
   165 text{*So that blast can use it too*}
   166 declare  Spy_see_priK [THEN [2] rev_iffD1, dest!]
   167 
   168 lemma Spy_analz_priK [simp]:
   169      "evs \<in> zg ==> (Key (priK A) \<in> analz (spies evs)) = (A \<in> bad)"
   170 by auto 
   171 
   172 
   173 subsection{*About NRO*}
   174 
   175 text{*Below we prove that if @{term NRO} exists then @{term A} definitely
   176 sent it, provided @{term A} is not broken.  *}
   177 
   178 text{*Strong conclusion for a good agent*}
   179 lemma NRO_authenticity_good:
   180      "[| NRO \<in> parts (spies evs);
   181          NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
   182          A \<notin> bad;  evs \<in> zg |]
   183      ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs"
   184 apply clarify
   185 apply (erule rev_mp)
   186 apply (erule zg.induct)
   187 apply (frule_tac [5] ZG2_msg_in_parts_spies, auto)  
   188 done
   189 
   190 text{*A compromised agent: we can't be sure whether A or the Spy sends the
   191 message or of the precise form of the message*}
   192 lemma NRO_authenticity_bad:
   193      "[| NRO \<in> parts (spies evs);
   194          NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
   195          A \<in> bad;  evs \<in> zg |]
   196      ==> \<exists>A' \<in> {A,Spy}. \<exists>C Y. Says A' C Y \<in> set evs & NRO \<in> parts {Y}"
   197 apply clarify
   198 apply (erule rev_mp)
   199 apply (erule zg.induct)
   200 apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   201 txt{*ZG3*}
   202    prefer 4 apply blast
   203 txt{*ZG2*}
   204    prefer 3 apply blast
   205 txt{*Fake*}
   206 apply (simp add: parts_insert_knows_A, blast) 
   207 txt{*ZG1*}
   208 apply (auto intro!: exI)
   209 done
   210 
   211 theorem NRO_authenticity:
   212      "[| NRO \<in> used evs;
   213          NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
   214          A \<notin> broken;  evs \<in> zg |]
   215      ==> \<exists>C Y. Says A C Y \<in> set evs & NRO \<in> parts {Y}"
   216 apply auto
   217  apply (force dest!: Crypt_used_imp_spies NRO_authenticity_good)
   218 apply (force dest!: Crypt_used_imp_spies NRO_authenticity_bad)
   219 done
   220 
   221 
   222 subsection{*About NRR*}
   223 
   224 text{*Below we prove that if @{term NRR} exists then @{term B} definitely
   225 sent it, provided @{term B} is not broken.*}
   226 
   227 text{*Strong conclusion for a good agent*}
   228 lemma NRR_authenticity_good:
   229      "[| NRR \<in> parts (spies evs);
   230          NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
   231          B \<notin> bad;  evs \<in> zg |]
   232      ==> Says B A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
   233 apply clarify
   234 apply (erule rev_mp)
   235 apply (erule zg.induct)
   236 apply (frule_tac [5] ZG2_msg_in_parts_spies, auto)  
   237 done
   238 
   239 lemma NRR_authenticity_bad:
   240      "[| NRR \<in> parts (spies evs);
   241          NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
   242          B \<in> bad;  evs \<in> zg |]
   243      ==> \<exists>B' \<in> {B,Spy}. \<exists>C Y. Says B' C Y \<in> set evs & NRR \<in> parts {Y}"
   244 apply clarify
   245 apply (erule rev_mp)
   246 apply (erule zg.induct)
   247 apply (frule_tac [5] ZG2_msg_in_parts_spies)
   248 apply (simp_all del: bex_simps)
   249 txt{*ZG3*}
   250    prefer 4 apply blast
   251 txt{*Fake*}
   252 apply (simp add: parts_insert_knows_A, blast)
   253 txt{*ZG1*}
   254 apply (auto simp del: bex_simps)
   255 txt{*ZG2*}
   256 apply (force intro!: exI)
   257 done
   258 
   259 theorem NRR_authenticity:
   260      "[| NRR \<in> used evs;
   261          NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
   262          B \<notin> broken;  evs \<in> zg |]
   263      ==> \<exists>C Y. Says B C Y \<in> set evs & NRR \<in> parts {Y}"
   264 apply auto
   265  apply (force dest!: Crypt_used_imp_spies NRR_authenticity_good)
   266 apply (force dest!: Crypt_used_imp_spies NRR_authenticity_bad)
   267 done
   268 
   269 
   270 subsection{*Proofs About @{term sub_K}*}
   271 
   272 text{*Below we prove that if @{term sub_K} exists then @{term A} definitely
   273 sent it, provided @{term A} is not broken.  *}
   274 
   275 text{*Strong conclusion for a good agent*}
   276 lemma sub_K_authenticity_good:
   277      "[| sub_K \<in> parts (spies evs);
   278          sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   279          A \<notin> bad;  evs \<in> zg |]
   280      ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
   281 apply (erule rev_mp)
   282 apply (erule zg.induct)
   283 apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   284 txt{*Fake*} 
   285 apply (blast dest!: Fake_parts_sing_imp_Un)
   286 done
   287 
   288 text{*A compromised agent: we can't be sure whether A or the Spy sends the
   289 message or of the precise form of the message*}
   290 lemma sub_K_authenticity_bad:
   291      "[| sub_K \<in> parts (spies evs);
   292          sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   293          A \<in> bad;  evs \<in> zg |]
   294      ==> \<exists>A' \<in> {A,Spy}. \<exists>C Y. Says A' C Y \<in> set evs & sub_K \<in> parts {Y}"
   295 apply clarify
   296 apply (erule rev_mp)
   297 apply (erule zg.induct)
   298 apply (frule_tac [5] ZG2_msg_in_parts_spies)
   299 apply (simp_all del: bex_simps)
   300 txt{*Fake*}
   301 apply (simp add: parts_insert_knows_A, blast)
   302 txt{*ZG1*}
   303 apply (auto simp del: bex_simps)
   304 txt{*ZG3*}
   305 apply (force intro!: exI)
   306 done
   307 
   308 theorem sub_K_authenticity:
   309      "[| sub_K \<in> used evs;
   310          sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   311          A \<notin> broken;  evs \<in> zg |]
   312      ==> \<exists>C Y. Says A C Y \<in> set evs & sub_K \<in> parts {Y}"
   313 apply auto
   314  apply (force dest!: Crypt_used_imp_spies sub_K_authenticity_good)
   315 apply (force dest!: Crypt_used_imp_spies sub_K_authenticity_bad)
   316 done
   317 
   318 
   319 subsection{*Proofs About @{term con_K}*}
   320 
   321 text{*Below we prove that if @{term con_K} exists, then @{term TTP} has it,
   322 and therefore @{term A} and @{term B}) can get it too.  Moreover, we know
   323 that @{term A} sent @{term sub_K}*}
   324 
   325 lemma con_K_authenticity:
   326      "[|con_K \<in> used evs;
   327         con_K = Crypt (priK TTP)
   328                   {|Number f_con, Agent A, Agent B, Nonce L, Key K|};
   329         evs \<in> zg |]
   330     ==> Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
   331           \<in> set evs"
   332 apply clarify
   333 apply (erule rev_mp)
   334 apply (erule zg.induct)
   335 apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   336 txt{*Fake*}
   337 apply (blast dest!: Fake_parts_sing_imp_Un)
   338 txt{*ZG2*}
   339 apply (blast dest: parts_cut)
   340 done
   341 
   342 text{*If @{term TTP} holds @{term con_K} then @{term A} sent
   343  @{term sub_K}.  We assume that @{term A} is not broken.  Nothing needs to
   344  be assumed about the form of @{term con_K}!*}
   345 lemma Notes_TTP_imp_Says_A:
   346      "[|Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
   347            \<in> set evs;
   348         sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   349         A \<notin> broken; evs \<in> zg|]
   350     ==> \<exists>C Y. Says A C Y \<in> set evs & sub_K \<in> parts {Y}"
   351 by (blast dest!: Notes_TTP_imp_Gets [THEN Gets_imp_knows_Spy, THEN parts.Inj] intro: sub_K_authenticity)
   352 
   353 text{*If @{term con_K} exists, then @{term A} sent @{term sub_K}.*}
   354 theorem B_sub_K_authenticity:
   355      "[|con_K \<in> used evs;
   356         con_K = Crypt (priK TTP) {|Number f_con, Agent A, Agent B,
   357                                    Nonce L, Key K|};
   358         sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   359         A \<notin> broken; B \<noteq> TTP; evs \<in> zg|]
   360     ==> \<exists>C Y. Says A C Y \<in> set evs & sub_K \<in> parts {Y}"
   361 by (blast dest: con_K_authenticity Notes_TTP_imp_Says_A)
   362 
   363 
   364 subsection{*Proving fairness*}
   365 
   366 text{*Cannot prove that, if @{term B} has NRO, then  @{term A} has her NRR.
   367 It would appear that @{term B} has a small advantage, though it is
   368 useless to win disputes: @{term B} needs to present @{term con_K} as well.*}
   369 
   370 text{*Strange: unicity of the label protects @{term A}?*}
   371 lemma A_unicity: 
   372      "[|NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
   373         NRO \<in> parts (spies evs);
   374         Says A B {|Number f_nro, Agent B, Nonce L, Crypt K M', NRO'|}
   375           \<in> set evs;
   376         A \<notin> bad; evs \<in> zg |]
   377      ==> M'=M"
   378 apply clarify
   379 apply (erule rev_mp)
   380 apply (erule rev_mp)
   381 apply (erule zg.induct)
   382 apply (frule_tac [5] ZG2_msg_in_parts_spies, auto) 
   383 txt{*ZG1: freshness*}
   384 apply (blast dest: parts.Body) 
   385 done
   386 
   387 
   388 text{*Fairness lemma: if @{term sub_K} exists, then @{term A} holds 
   389 NRR.  Relies on unicity of labels.*}
   390 lemma sub_K_implies_NRR:
   391      "[| sub_K \<in> parts (spies evs);
   392          NRO \<in> parts (spies evs);
   393          sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   394          NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
   395          NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, Crypt K M|};
   396          A \<notin> bad;  evs \<in> zg |]
   397      ==> Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
   398 apply clarify
   399 apply (erule rev_mp)
   400 apply (erule rev_mp)
   401 apply (erule zg.induct)
   402 apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   403 txt{*Fake*}
   404 apply blast 
   405 txt{*ZG1: freshness*}
   406 apply (blast dest: parts.Body) 
   407 txt{*ZG3*}
   408 apply (blast dest: A_unicity [OF refl]) 
   409 done
   410 
   411 
   412 lemma Crypt_used_imp_L_used:
   413      "[| Crypt (priK TTP) {|F, A, B, L, K|} \<in> used evs; evs \<in> zg |]
   414       ==> L \<in> used evs"
   415 apply (erule rev_mp)
   416 apply (erule zg.induct, auto)
   417 txt{*Fake*}
   418 apply (blast dest!: Fake_parts_sing_imp_Un)
   419 txt{*ZG2: freshness*}
   420 apply (blast dest: parts.Body) 
   421 done
   422 
   423 
   424 text{*Fairness for @{term A}: if @{term con_K} and @{term NRO} exist, 
   425 then @{term A} holds NRR.  @{term A} must be uncompromised, but there is no
   426 assumption about @{term B}.*}
   427 theorem A_fairness_NRO:
   428      "[|con_K \<in> used evs;
   429         NRO \<in> parts (spies evs);
   430         con_K = Crypt (priK TTP)
   431                       {|Number f_con, Agent A, Agent B, Nonce L, Key K|};
   432         NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
   433         NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, Crypt K M|};
   434         A \<notin> bad;  evs \<in> zg |]
   435     ==> Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
   436 apply clarify
   437 apply (erule rev_mp)
   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 (simp add: parts_insert_knows_A) 
   443    apply (blast dest: Fake_parts_sing_imp_Un) 
   444   txt{*ZG1*}
   445   apply (blast dest: Crypt_used_imp_L_used) 
   446  txt{*ZG2*}
   447  apply (blast dest: parts_cut)
   448 txt{*ZG4*}
   449 apply (blast intro: sub_K_implies_NRR [OF _ _ refl] 
   450              dest: Gets_imp_knows_Spy [THEN parts.Inj])
   451 done
   452 
   453 text{*Fairness for @{term B}: NRR exists at all, then @{term B} holds NRO.
   454 @{term B} must be uncompromised, but there is no assumption about @{term
   455 A}. *}
   456 theorem B_fairness_NRR:
   457      "[|NRR \<in> used evs;
   458         NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
   459         NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
   460         B \<notin> bad; evs \<in> zg |]
   461     ==> Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs"
   462 apply clarify
   463 apply (erule rev_mp)
   464 apply (erule zg.induct)
   465 apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   466 txt{*Fake*}
   467 apply (blast dest!: Fake_parts_sing_imp_Un)
   468 txt{*ZG2*}
   469 apply (blast dest: parts_cut)
   470 done
   471 
   472 
   473 text{*If @{term con_K} exists at all, then @{term B} can get it, by @{text
   474 con_K_authenticity}.  Cannot conclude that also NRO is available to @{term B},
   475 because if @{term A} were unfair, @{term A} could build message 3 without
   476 building message 1, which contains NRO. *}
   477 
   478 end