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