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