src/HOL/Auth/ZhouGollmann.thy
author wenzelm
Mon Jan 11 21:21:02 2016 +0100 (2016-01-11)
changeset 62145 5b946c81dfbf
parent 61956 38b73f7940af
child 67443 3abf6a722518
permissions -rw-r--r--
eliminated old defs;
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    
wenzelm@61830
    24
    \<comment>\<open>the compromised honest agents; TTP is included as it's not allowed to
wenzelm@61830
    25
        use the protocol\<close>
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@61956
    46
           NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, C\<rbrace>|]
wenzelm@61956
    47
       ==> Says A B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> # 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@61956
    51
           Gets B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<in> set evs2;
wenzelm@61956
    52
           NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, C\<rbrace>;
wenzelm@61956
    53
           NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, C\<rbrace>|]
wenzelm@61956
    54
       ==> Says B A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> # 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@61956
    59
           Says A B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<in> set evs3;
wenzelm@61956
    60
           Gets A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<in> set evs3;
wenzelm@61956
    61
           NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, C\<rbrace>;
wenzelm@61956
    62
           sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>|]
wenzelm@61956
    63
       ==> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace>
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@61956
    73
           Gets TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace>
wenzelm@32960
    74
             \<in> set evs4;
wenzelm@61956
    75
           sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
wenzelm@61956
    76
           con_K = Crypt (priK TTP) \<lbrace>Number f_con, Agent A, Agent B,
wenzelm@61956
    77
                                      Nonce L, Key K\<rbrace>|]
paulson@14736
    78
       ==> Says TTP Spy con_K
paulson@14736
    79
           #
wenzelm@61956
    80
           Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace>
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
wenzelm@61830
    92
text\<open>A "possibility property": there are traces that reach the end\<close>
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.
wenzelm@61956
    95
           Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K,
wenzelm@61956
    96
               Crypt (priK TTP) \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K\<rbrace>\<rbrace>
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
wenzelm@61830
   107
subsection \<open>Basic Lemmas\<close>
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
wenzelm@61830
   120
text\<open>Lets us replace proofs about @{term "used evs"} by simpler proofs 
wenzelm@61830
   121
about @{term "parts (spies evs)"}.\<close>
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:
wenzelm@61956
   131
     "[|Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace>
paulson@14145
   132
           \<in> set evs;
wenzelm@61956
   133
        sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
paulson@14145
   134
        evs \<in> zg|]
wenzelm@61956
   135
    ==> Gets TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<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
wenzelm@61830
   140
text\<open>For reasoning about C, which is encrypted in message ZG2\<close>
paulson@14145
   141
lemma ZG2_msg_in_parts_spies:
wenzelm@61956
   142
     "[|Gets B \<lbrace>F, B', L, C, X\<rbrace> \<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
wenzelm@61830
   153
text\<open>So that blast can use it too\<close>
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
wenzelm@61830
   161
subsection\<open>About NRO: Validity for @{term B}\<close>
paulson@14145
   162
wenzelm@61830
   163
text\<open>Below we prove that if @{term NRO} exists then @{term A} definitely
wenzelm@61830
   164
sent it, provided @{term A} is not broken.\<close>
paulson@14145
   165
wenzelm@61830
   166
text\<open>Strong conclusion for a good agent\<close>
paulson@15068
   167
lemma NRO_validity_good:
wenzelm@61956
   168
     "[|NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, C\<rbrace>;
paulson@14741
   169
        NRO \<in> parts (spies evs);
paulson@14741
   170
        A \<notin> bad;  evs \<in> zg |]
wenzelm@61956
   171
     ==> Says A B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<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:
wenzelm@61956
   179
     "[|Says A' B \<lbrace>n, b, l, C, Crypt (priK A) X\<rbrace> \<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
wenzelm@61830
   185
text\<open>Holds also for @{term "A = Spy"}!\<close>
paulson@15068
   186
theorem NRO_validity:
wenzelm@61956
   187
     "[|Gets B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<in> set evs;
wenzelm@61956
   188
        NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, C\<rbrace>;
paulson@14741
   189
        A \<notin> broken;  evs \<in> zg |]
wenzelm@61956
   190
     ==> Says A B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<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)
wenzelm@61830
   194
txt\<open>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"}. 
wenzelm@61830
   196
  Thus theorem \<open>NRO_validity_good\<close> applies.\<close>
paulson@15068
   197
apply (blast dest: NRO_validity_good [OF refl])
paulson@14145
   198
done
paulson@14145
   199
paulson@14145
   200
wenzelm@61830
   201
subsection\<open>About NRR: Validity for @{term A}\<close>
paulson@14145
   202
wenzelm@61830
   203
text\<open>Below we prove that if @{term NRR} exists then @{term B} definitely
wenzelm@61830
   204
sent it, provided @{term B} is not broken.\<close>
paulson@14145
   205
wenzelm@61830
   206
text\<open>Strong conclusion for a good agent\<close>
paulson@15068
   207
lemma NRR_validity_good:
wenzelm@61956
   208
     "[|NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, C\<rbrace>;
paulson@14741
   209
        NRR \<in> parts (spies evs);
paulson@14741
   210
        B \<notin> bad;  evs \<in> zg |]
wenzelm@61956
   211
     ==> Says B A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<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:
wenzelm@61956
   219
     "[|Says B' A \<lbrace>n, a, l, Crypt (priK B) X\<rbrace> \<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
wenzelm@61830
   225
text\<open>Holds also for @{term "B = Spy"}!\<close>
paulson@15068
   226
theorem NRR_validity:
wenzelm@61956
   227
     "[|Says B' A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<in> set evs;
wenzelm@61956
   228
        NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, C\<rbrace>;
paulson@14741
   229
        B \<notin> broken; evs \<in> zg|]
wenzelm@61956
   230
    ==> Says B A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<in> set evs"
paulson@14741
   231
apply clarify 
paulson@14741
   232
apply (frule NRR_sender, auto)
wenzelm@61830
   233
txt\<open>We are left with the case where @{term "B' = Spy"} and  @{term "B' \<noteq> B"},
wenzelm@61830
   234
  i.e. @{term "B \<notin> bad"}, when we can apply \<open>NRR_validity_good\<close>.\<close>
paulson@15068
   235
 apply (blast dest: NRR_validity_good [OF refl])
paulson@14145
   236
done
paulson@14145
   237
paulson@14145
   238
wenzelm@61830
   239
subsection\<open>Proofs About @{term sub_K}\<close>
paulson@14145
   240
wenzelm@61830
   241
text\<open>Below we prove that if @{term sub_K} exists then @{term A} definitely
wenzelm@61830
   242
sent it, provided @{term A} is not broken.\<close>
paulson@14145
   243
wenzelm@61830
   244
text\<open>Strong conclusion for a good agent\<close>
paulson@15068
   245
lemma sub_K_validity_good:
wenzelm@61956
   246
     "[|sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
paulson@14741
   247
        sub_K \<in> parts (spies evs);
paulson@14741
   248
        A \<notin> bad;  evs \<in> zg |]
wenzelm@61956
   249
     ==> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<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)
wenzelm@61830
   254
txt\<open>Fake\<close> 
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:
wenzelm@61956
   259
     "[|Says A' TTP \<lbrace>n, b, l, k, Crypt (priK A) X\<rbrace> \<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
wenzelm@61830
   265
text\<open>Holds also for @{term "A = Spy"}!\<close>
paulson@15068
   266
theorem sub_K_validity:
wenzelm@61956
   267
     "[|Gets TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs;
wenzelm@61956
   268
        sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
paulson@14741
   269
        A \<notin> broken;  evs \<in> zg |]
wenzelm@61956
   270
     ==> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<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)
wenzelm@61830
   274
txt\<open>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"}. 
wenzelm@61830
   276
  Thus theorem \<open>sub_K_validity_good\<close> applies.\<close>
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
wenzelm@61830
   282
subsection\<open>Proofs About @{term con_K}\<close>
paulson@14145
   283
wenzelm@61830
   284
text\<open>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
wenzelm@61830
   286
that @{term A} sent @{term sub_K}\<close>
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)
wenzelm@61956
   291
                  \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K\<rbrace>;
paulson@14145
   292
        evs \<in> zg |]
wenzelm@61956
   293
    ==> Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace>
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)
wenzelm@61830
   299
txt\<open>Fake\<close>
paulson@14145
   300
apply (blast dest!: Fake_parts_sing_imp_Un)
wenzelm@61830
   301
txt\<open>ZG2\<close> 
paulson@14145
   302
apply (blast dest: parts_cut)
paulson@14145
   303
done
paulson@14145
   304
wenzelm@61830
   305
text\<open>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
wenzelm@61830
   307
  needs to be assumed about the form of @{term con_K}!\<close>
paulson@14145
   308
lemma Notes_TTP_imp_Says_A:
wenzelm@61956
   309
     "[|Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace>
paulson@14145
   310
           \<in> set evs;
wenzelm@61956
   311
        sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
paulson@14145
   312
        A \<notin> broken; evs \<in> zg|]
wenzelm@61956
   313
     ==> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<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)
wenzelm@61830
   318
txt\<open>ZG4\<close>
paulson@15047
   319
apply clarify 
paulson@15068
   320
apply (rule sub_K_validity, auto) 
paulson@14741
   321
done
paulson@14145
   322
wenzelm@61830
   323
text\<open>If @{term con_K} exists, then @{term A} sent @{term sub_K}.  We again
wenzelm@61830
   324
   assume that @{term A} is not broken.\<close>
paulson@15068
   325
theorem B_sub_K_validity:
paulson@14145
   326
     "[|con_K \<in> used evs;
wenzelm@61956
   327
        con_K = Crypt (priK TTP) \<lbrace>Number f_con, Agent A, Agent B,
wenzelm@61956
   328
                                   Nonce L, Key K\<rbrace>;
wenzelm@61956
   329
        sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
paulson@14741
   330
        A \<notin> broken; evs \<in> zg|]
wenzelm@61956
   331
     ==> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs"
paulson@15068
   332
by (blast dest: con_K_validity Notes_TTP_imp_Says_A)
paulson@14145
   333
paulson@14145
   334
wenzelm@61830
   335
subsection\<open>Proving fairness\<close>
paulson@14145
   336
wenzelm@61830
   337
text\<open>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
wenzelm@61830
   339
useless to win disputes: @{term B} needs to present @{term con_K} as well.\<close>
paulson@14145
   340
wenzelm@61830
   341
text\<open>Strange: unicity of the label protects @{term A}?\<close>
paulson@14145
   342
lemma A_unicity: 
wenzelm@61956
   343
     "[|NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, Crypt K M\<rbrace>;
paulson@14145
   344
        NRO \<in> parts (spies evs);
wenzelm@61956
   345
        Says A B \<lbrace>Number f_nro, Agent B, Nonce L, Crypt K M', NRO'\<rbrace>
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) 
wenzelm@61830
   354
txt\<open>ZG1: freshness\<close>
paulson@14145
   355
apply (blast dest: parts.Body) 
paulson@14145
   356
done
paulson@14145
   357
paulson@14145
   358
wenzelm@61830
   359
text\<open>Fairness lemma: if @{term sub_K} exists, then @{term A} holds 
wenzelm@61830
   360
NRR.  Relies on unicity of labels.\<close>
paulson@14145
   361
lemma sub_K_implies_NRR:
wenzelm@61956
   362
     "[| NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, Crypt K M\<rbrace>;
wenzelm@61956
   363
         NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, Crypt K M\<rbrace>;
paulson@14741
   364
         sub_K \<in> parts (spies evs);
paulson@14145
   365
         NRO \<in> parts (spies evs);
wenzelm@61956
   366
         sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
paulson@14145
   367
         A \<notin> bad;  evs \<in> zg |]
wenzelm@61956
   368
     ==> Gets A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<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)
wenzelm@61830
   375
txt\<open>Fake\<close>
paulson@14145
   376
apply blast 
wenzelm@61830
   377
txt\<open>ZG1: freshness\<close>
paulson@14145
   378
apply (blast dest: parts.Body) 
wenzelm@61830
   379
txt\<open>ZG3\<close> 
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:
wenzelm@61956
   385
     "[| Crypt (priK TTP) \<lbrace>F, A, B, L, K\<rbrace> \<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)
wenzelm@61830
   389
txt\<open>Fake\<close>
paulson@14145
   390
apply (blast dest!: Fake_parts_sing_imp_Un)
wenzelm@61830
   391
txt\<open>ZG2: freshness\<close>
paulson@14145
   392
apply (blast dest: parts.Body) 
paulson@14145
   393
done
paulson@14145
   394
paulson@14145
   395
wenzelm@61830
   396
text\<open>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
wenzelm@61830
   398
assumption about @{term B}.\<close>
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)
wenzelm@61956
   403
                      \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K\<rbrace>;
wenzelm@61956
   404
        NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, Crypt K M\<rbrace>;
wenzelm@61956
   405
        NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, Crypt K M\<rbrace>;
paulson@14145
   406
        A \<notin> bad;  evs \<in> zg |]
wenzelm@61956
   407
    ==> Gets A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<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)
wenzelm@61830
   413
   txt\<open>Fake\<close>
paulson@14145
   414
   apply (simp add: parts_insert_knows_A) 
paulson@14145
   415
   apply (blast dest: Fake_parts_sing_imp_Un) 
wenzelm@61830
   416
  txt\<open>ZG1\<close>
paulson@14145
   417
  apply (blast dest: Crypt_used_imp_L_used) 
wenzelm@61830
   418
 txt\<open>ZG2\<close>
paulson@14145
   419
 apply (blast dest: parts_cut)
wenzelm@61830
   420
txt\<open>ZG4\<close> 
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
wenzelm@61830
   425
text\<open>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
wenzelm@61830
   427
A}.\<close>
paulson@14145
   428
theorem B_fairness_NRR:
paulson@14145
   429
     "[|NRR \<in> used evs;
wenzelm@61956
   430
        NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, C\<rbrace>;
wenzelm@61956
   431
        NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, C\<rbrace>;
paulson@14145
   432
        B \<notin> bad; evs \<in> zg |]
wenzelm@61956
   433
    ==> Gets B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<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)
wenzelm@61830
   438
txt\<open>Fake\<close>
paulson@14145
   439
apply (blast dest!: Fake_parts_sing_imp_Un)
wenzelm@61830
   440
txt\<open>ZG2\<close>
paulson@14145
   441
apply (blast dest: parts_cut)
paulson@14145
   442
done
paulson@14145
   443
paulson@14145
   444
wenzelm@61830
   445
text\<open>If @{term con_K} exists at all, then @{term B} can get it, by \<open>con_K_validity\<close>.  Cannot conclude that also NRO is available to @{term B},
paulson@14145
   446
because if @{term A} were unfair, @{term A} could build message 3 without
wenzelm@61830
   447
building message 1, which contains NRO.\<close>
paulson@14145
   448
paulson@14145
   449
end