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