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