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