src/HOL/Auth/Kerberos_BAN.thy
author paulson
Thu Jul 24 16:36:29 2003 +0200 (2003-07-24)
changeset 14126 28824746d046
parent 13926 6e62e5357a10
child 14200 d8598e24f8fa
permissions -rw-r--r--
Tidying and replacement of some axioms by specifications
paulson@5053
     1
(*  Title:      HOL/Auth/Kerberos_BAN
paulson@5053
     2
    ID:         $Id$
paulson@5053
     3
    Author:     Giampaolo Bella, Cambridge University Computer Laboratory
paulson@5053
     4
    Copyright   1998  University of Cambridge
paulson@5053
     5
paulson@5053
     6
The Kerberos protocol, BAN version.
paulson@5053
     7
paulson@5053
     8
From page 251 of
paulson@5053
     9
  Burrows, Abadi and Needham.  A Logic of Authentication.
paulson@5053
    10
  Proc. Royal Soc. 426 (1989)
paulson@13926
    11
paulson@13926
    12
  Confidentiality (secrecy) and authentication properties rely on 
paulson@13926
    13
  temporal checks: strong guarantees in a little abstracted - but
paulson@13926
    14
  very realistic - model (see .thy).
paulson@13926
    15
paulson@13926
    16
Tidied and converted to Isar by lcp.
paulson@5053
    17
*)
paulson@5053
    18
paulson@13926
    19
theory Kerberos_BAN = Shared:
paulson@5053
    20
paulson@5053
    21
(* Temporal modelization: session keys can be leaked 
paulson@5053
    22
                          ONLY when they have expired *)
paulson@5053
    23
paulson@5053
    24
syntax
paulson@13926
    25
    CT :: "event list=>nat"
paulson@13926
    26
    Expired :: "[nat, event list] => bool"
paulson@13926
    27
    RecentAuth :: "[nat, event list] => bool"
paulson@5053
    28
paulson@5053
    29
consts
paulson@5053
    30
paulson@5053
    31
    (*Duration of the session key*)
paulson@5053
    32
    SesKeyLife   :: nat
paulson@5053
    33
paulson@5053
    34
    (*Duration of the authenticator*)
paulson@5053
    35
    AutLife :: nat
paulson@5053
    36
paulson@14126
    37
text{*The ticket should remain fresh for two journeys on the network at least*}
paulson@14126
    38
specification (SesKeyLife)
paulson@14126
    39
  SesKeyLife_LB [iff]: "2 \<le> SesKeyLife"
paulson@14126
    40
    by blast
paulson@5053
    41
paulson@14126
    42
text{*The authenticator only for one journey*}
paulson@14126
    43
specification (AutLife)
paulson@14126
    44
  AutLife_LB [iff]:    "Suc 0 \<le> AutLife"
paulson@14126
    45
    by blast
paulson@14126
    46
paulson@5053
    47
paulson@5053
    48
translations
paulson@5053
    49
   "CT" == "length"
paulson@5053
    50
  
paulson@5053
    51
   "Expired T evs" == "SesKeyLife + T < CT evs"
paulson@5053
    52
paulson@14126
    53
   "RecentAuth T evs" == "CT evs \<le> AutLife + T"
paulson@5053
    54
paulson@13926
    55
consts  kerberos_ban   :: "event list set"
paulson@5053
    56
inductive "kerberos_ban"
paulson@13926
    57
 intros 
paulson@13926
    58
paulson@13926
    59
   Nil:  "[] \<in> kerberos_ban"
paulson@13926
    60
paulson@13926
    61
   Fake: "[| evsf \<in> kerberos_ban;  X \<in> synth (analz (spies evsf)) |]
paulson@13926
    62
	  ==> Says Spy B X # evsf \<in> kerberos_ban"
paulson@13926
    63
paulson@13926
    64
paulson@13926
    65
   Kb1:  "[| evs1 \<in> kerberos_ban |]
paulson@13926
    66
	  ==> Says A Server {|Agent A, Agent B|} # evs1
paulson@13926
    67
		\<in>  kerberos_ban"
paulson@13926
    68
paulson@13926
    69
paulson@13926
    70
   Kb2:  "[| evs2 \<in> kerberos_ban;  Key KAB \<notin> used evs2;
paulson@13926
    71
	     Says A' Server {|Agent A, Agent B|} \<in> set evs2 |]
paulson@13926
    72
	  ==> Says Server A 
paulson@13926
    73
		(Crypt (shrK A)
paulson@13926
    74
		   {|Number (CT evs2), Agent B, Key KAB,  
paulson@13926
    75
		    (Crypt (shrK B) {|Number (CT evs2), Agent A, Key KAB|})|}) 
paulson@13926
    76
		# evs2 \<in> kerberos_ban"
paulson@13926
    77
paulson@13926
    78
paulson@13926
    79
   Kb3:  "[| evs3 \<in> kerberos_ban;  
paulson@13926
    80
	     Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) 
paulson@13926
    81
	       \<in> set evs3;
paulson@13926
    82
	     Says A Server {|Agent A, Agent B|} \<in> set evs3;
paulson@13926
    83
	     ~ Expired Ts evs3 |]
paulson@13926
    84
	  ==> Says A B {|X, Crypt K {|Agent A, Number (CT evs3)|} |} 
paulson@13926
    85
	       # evs3 \<in> kerberos_ban"
paulson@13926
    86
paulson@13926
    87
paulson@13926
    88
   Kb4:  "[| evs4 \<in> kerberos_ban;  
paulson@13926
    89
	     Says A' B {|(Crypt (shrK B) {|Number Ts, Agent A, Key K|}), 
paulson@13926
    90
			 (Crypt K {|Agent A, Number Ta|}) |}: set evs4;
paulson@13926
    91
	     ~ Expired Ts evs4;  RecentAuth Ta evs4 |]
paulson@13926
    92
	  ==> Says B A (Crypt K (Number Ta)) # evs4
paulson@13926
    93
		\<in> kerberos_ban"
paulson@5053
    94
paulson@13926
    95
	(*Old session keys may become compromised*)
paulson@13926
    96
   Oops: "[| evso \<in> kerberos_ban;  
paulson@13926
    97
	     Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
paulson@13926
    98
	       \<in> set evso;
paulson@13926
    99
	     Expired Ts evso |]
paulson@13926
   100
	  ==> Notes Spy {|Number Ts, Key K|} # evso \<in> kerberos_ban"
paulson@13926
   101
paulson@13926
   102
paulson@13926
   103
declare Says_imp_knows_Spy [THEN parts.Inj, dest] parts.Body [dest]
paulson@13926
   104
declare analz_subset_parts [THEN subsetD, dest]
paulson@13926
   105
declare Fake_parts_insert [THEN subsetD, dest]
paulson@13926
   106
paulson@13926
   107
(*A "possibility property": there are traces that reach the end.*)
paulson@13926
   108
lemma "\<exists>Timestamp K. \<exists>evs \<in> kerberos_ban.     
paulson@13926
   109
             Says B A (Crypt K (Number Timestamp))  
paulson@13926
   110
                  \<in> set evs"
paulson@13926
   111
apply (cut_tac SesKeyLife_LB)
paulson@13926
   112
apply (intro exI bexI)
paulson@13926
   113
apply (rule_tac [2] 
paulson@13926
   114
           kerberos_ban.Nil [THEN kerberos_ban.Kb1, THEN kerberos_ban.Kb2, 
paulson@13926
   115
                             THEN kerberos_ban.Kb3, THEN kerberos_ban.Kb4], possibility)
paulson@13926
   116
apply (simp_all (no_asm_simp))
paulson@13926
   117
done
paulson@13926
   118
paulson@13926
   119
paulson@13926
   120
(**** Inductive proofs about kerberos_ban ****)
paulson@13926
   121
paulson@13926
   122
(*Forwarding Lemma for reasoning about the encrypted portion of message Kb3*)
paulson@13926
   123
lemma Kb3_msg_in_parts_spies:
paulson@13926
   124
     "Says S A (Crypt KA {|Timestamp, B, K, X|}) \<in> set evs  
paulson@13926
   125
      ==> X \<in> parts (spies evs)"
paulson@13926
   126
by blast
paulson@13926
   127
                              
paulson@13926
   128
lemma Oops_parts_spies:
paulson@13926
   129
     "Says Server A (Crypt (shrK A) {|Timestamp, B, K, X|}) \<in> set evs  
paulson@13926
   130
      ==> K \<in> parts (spies evs)"
paulson@13926
   131
by blast
paulson@13926
   132
paulson@13926
   133
paulson@13926
   134
(*Spy never sees another agent's shared key! (unless it's bad at start)*)
paulson@13926
   135
lemma Spy_see_shrK [simp]:
paulson@13926
   136
     "evs \<in> kerberos_ban ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
paulson@13926
   137
apply (erule kerberos_ban.induct) 
paulson@13926
   138
apply (frule_tac [7] Oops_parts_spies) 
paulson@13926
   139
apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all)  
paulson@13926
   140
apply blast+
paulson@13926
   141
done
paulson@5053
   142
paulson@5053
   143
paulson@13926
   144
lemma Spy_analz_shrK [simp]:
paulson@13926
   145
     "evs \<in> kerberos_ban ==> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
paulson@13926
   146
apply auto
paulson@13926
   147
done
paulson@13926
   148
paulson@13926
   149
paulson@13926
   150
lemma Spy_see_shrK_D [dest!]:
paulson@13926
   151
     "[| Key (shrK A) \<in> parts (spies evs);        
paulson@13926
   152
                evs \<in> kerberos_ban |] ==> A:bad"
paulson@13926
   153
apply (blast dest: Spy_see_shrK)
paulson@13926
   154
done
paulson@13926
   155
paulson@13926
   156
lemmas Spy_analz_shrK_D = analz_subset_parts [THEN subsetD, THEN Spy_see_shrK_D,  dest!]
paulson@13926
   157
paulson@13926
   158
paulson@13926
   159
(*Nobody can have used non-existent keys!*)
paulson@13926
   160
lemma new_keys_not_used [rule_format, simp]:
paulson@13926
   161
     "evs \<in> kerberos_ban ==>       
paulson@13926
   162
       Key K \<notin> used evs --> K \<notin> keysFor (parts (spies evs))"
paulson@13926
   163
apply (erule kerberos_ban.induct) 
paulson@13926
   164
apply (frule_tac [7] Oops_parts_spies) 
paulson@13926
   165
apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all)  
paulson@13926
   166
(*Fake*)
paulson@13926
   167
apply (force dest!: keysFor_parts_insert)
paulson@13926
   168
(*Kb2, Kb3, Kb4*)
paulson@13926
   169
apply blast+
paulson@13926
   170
done
paulson@13926
   171
paulson@13926
   172
(** Lemmas concerning the form of items passed in messages **)
paulson@13926
   173
paulson@13926
   174
(*Describes the form of K, X and K' when the Server sends this message.*)
paulson@13926
   175
lemma Says_Server_message_form:
paulson@13926
   176
     "[| Says Server A (Crypt K' {|Number Ts, Agent B, Key K, X|})   
paulson@13926
   177
         \<in> set evs; evs \<in> kerberos_ban |]                            
paulson@13926
   178
      ==> K \<notin> range shrK &                                          
paulson@13926
   179
          X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}) &       
paulson@13926
   180
          K' = shrK A"
paulson@13926
   181
apply (erule rev_mp)
paulson@13926
   182
apply (erule kerberos_ban.induct, auto)
paulson@13926
   183
done
paulson@5053
   184
paulson@5053
   185
paulson@13926
   186
(*If the encrypted message appears then it originated with the Server
paulson@13926
   187
  PROVIDED that A is NOT compromised!
paulson@13926
   188
paulson@13926
   189
  This shows implicitly the FRESHNESS OF THE SESSION KEY to A
paulson@13926
   190
*)
paulson@13926
   191
lemma A_trusts_K_by_Kb2:
paulson@13926
   192
     "[| Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}  
paulson@13926
   193
           \<in> parts (spies evs);                           
paulson@13926
   194
         A \<notin> bad;  evs \<in> kerberos_ban |]                 
paulson@13926
   195
       ==> Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})  
paulson@13926
   196
             \<in> set evs"
paulson@13926
   197
apply (erule rev_mp)
paulson@13926
   198
apply (erule kerberos_ban.induct) 
paulson@13926
   199
apply (frule_tac [7] Oops_parts_spies) 
paulson@13926
   200
apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all)  
paulson@13926
   201
apply blast
paulson@13926
   202
done
paulson@13926
   203
paulson@13926
   204
paulson@13926
   205
(*If the TICKET appears then it originated with the Server*)
paulson@13926
   206
(*FRESHNESS OF THE SESSION KEY to B*)
paulson@13926
   207
lemma B_trusts_K_by_Kb3:
paulson@13926
   208
     "[| Crypt (shrK B) {|Number Ts, Agent A, Key K|} \<in> parts (spies evs);  
paulson@13926
   209
         B \<notin> bad;  evs \<in> kerberos_ban |]                         
paulson@13926
   210
       ==> Says Server A                                          
paulson@13926
   211
            (Crypt (shrK A) {|Number Ts, Agent B, Key K,                    
paulson@13926
   212
                          Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})   
paulson@13926
   213
           \<in> set evs"
paulson@13926
   214
apply (erule rev_mp)
paulson@13926
   215
apply (erule kerberos_ban.induct) 
paulson@13926
   216
apply (frule_tac [7] Oops_parts_spies) 
paulson@13926
   217
apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all)  
paulson@13926
   218
apply blast
paulson@13926
   219
done
paulson@13926
   220
paulson@13926
   221
paulson@13926
   222
(*EITHER describes the form of X when the following message is sent, 
paulson@13926
   223
  OR     reduces it to the Fake case.
paulson@13926
   224
  Use Says_Server_message_form if applicable.*)
paulson@13926
   225
lemma Says_S_message_form:
paulson@13926
   226
     "[| Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})      
paulson@13926
   227
            \<in> set evs;                                                   
paulson@13926
   228
         evs \<in> kerberos_ban |]                                           
paulson@13926
   229
 ==> (K \<notin> range shrK & X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|})) 
paulson@13926
   230
          | X \<in> analz (spies evs)"
paulson@13926
   231
apply (case_tac "A \<in> bad")
paulson@13926
   232
apply (force dest!: Says_imp_spies [THEN analz.Inj])
paulson@13926
   233
apply (frule Says_imp_spies [THEN parts.Inj])
paulson@13926
   234
apply (blast dest!: A_trusts_K_by_Kb2 Says_Server_message_form)
paulson@13926
   235
done
paulson@13926
   236
paulson@5053
   237
paulson@5053
   238
paulson@13926
   239
(****
paulson@13926
   240
 The following is to prove theorems of the form
paulson@13926
   241
paulson@13926
   242
  Key K \<in> analz (insert (Key KAB) (spies evs)) ==>
paulson@13926
   243
  Key K \<in> analz (spies evs)
paulson@13926
   244
paulson@13926
   245
 A more general formula must be proved inductively.
paulson@13926
   246
paulson@13926
   247
****)
paulson@13926
   248
paulson@13926
   249
paulson@13926
   250
(** Session keys are not used to encrypt other session keys **)
paulson@13926
   251
paulson@13926
   252
lemma analz_image_freshK [rule_format (no_asm)]:
paulson@13926
   253
     "evs \<in> kerberos_ban ==>                           
paulson@14126
   254
   \<forall>K KK. KK \<subseteq> - (range shrK) -->                  
paulson@13926
   255
          (Key K \<in> analz (Key`KK Un (spies evs))) =   
paulson@13926
   256
          (K \<in> KK | Key K \<in> analz (spies evs))"
paulson@13926
   257
apply (erule kerberos_ban.induct)
paulson@13926
   258
apply (drule_tac [7] Says_Server_message_form)
paulson@13926
   259
apply (erule_tac [5] Says_S_message_form [THEN disjE], analz_freshK, spy_analz)
paulson@13926
   260
done
paulson@13926
   261
paulson@13926
   262
paulson@13926
   263
paulson@13926
   264
lemma analz_insert_freshK:
paulson@13926
   265
     "[| evs \<in> kerberos_ban;  KAB \<notin> range shrK |] ==>      
paulson@13926
   266
      (Key K \<in> analz (insert (Key KAB) (spies evs))) =        
paulson@13926
   267
      (K = KAB | Key K \<in> analz (spies evs))"
paulson@13926
   268
by (simp only: analz_image_freshK analz_image_freshK_simps)
paulson@13926
   269
paulson@13926
   270
paulson@13926
   271
(** The session key K uniquely identifies the message **)
paulson@13926
   272
paulson@13926
   273
lemma unique_session_keys:
paulson@13926
   274
     "[| Says Server A                                     
paulson@13926
   275
           (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \<in> set evs;   
paulson@13926
   276
         Says Server A'                                    
paulson@13926
   277
          (Crypt (shrK A') {|Number Ts', Agent B', Key K, X'|}) \<in> set evs; 
paulson@13926
   278
         evs \<in> kerberos_ban |] ==> A=A' & Ts=Ts' & B=B' & X = X'"
paulson@13926
   279
apply (erule rev_mp)
paulson@13926
   280
apply (erule rev_mp)
paulson@13926
   281
apply (erule kerberos_ban.induct) 
paulson@13926
   282
apply (frule_tac [7] Oops_parts_spies) 
paulson@13926
   283
apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all)  
paulson@13926
   284
(*Kb2: it can't be a new key*)
paulson@13926
   285
apply blast
paulson@13926
   286
done
paulson@13926
   287
paulson@13926
   288
paulson@13926
   289
(** Lemma: the session key sent in msg Kb2 would be EXPIRED
paulson@13926
   290
    if the spy could see it!
paulson@13926
   291
**)
paulson@13926
   292
paulson@13926
   293
lemma lemma2 [rule_format (no_asm)]:
paulson@13926
   294
     "[| A \<notin> bad;  B \<notin> bad;  evs \<in> kerberos_ban |]            
paulson@13926
   295
  ==> Says Server A                                             
paulson@13926
   296
          (Crypt (shrK A) {|Number Ts, Agent B, Key K,          
paulson@13926
   297
                            Crypt (shrK B) {|Number Ts, Agent A, Key K|}|}) 
paulson@13926
   298
         \<in> set evs -->                                          
paulson@13926
   299
      Key K \<in> analz (spies evs) --> Expired Ts evs"
paulson@13926
   300
apply (erule kerberos_ban.induct)
paulson@13926
   301
apply (frule_tac [7] Says_Server_message_form)
paulson@13926
   302
apply (frule_tac [5] Says_S_message_form [THEN disjE])
paulson@13926
   303
apply (simp_all (no_asm_simp) add: less_SucI analz_insert_eq analz_insert_freshK pushes)
paulson@13926
   304
txt{*Fake*}
paulson@13926
   305
apply spy_analz
paulson@13926
   306
txt{*Kb2*}
paulson@13926
   307
apply (blast intro: parts_insertI less_SucI)
paulson@13926
   308
txt{*Kb3*}
paulson@13926
   309
apply (case_tac "Aa \<in> bad")
paulson@13926
   310
 prefer 2 apply (blast dest: A_trusts_K_by_Kb2 unique_session_keys)
paulson@13926
   311
apply (blast dest: Says_imp_spies [THEN analz.Inj] Crypt_Spy_analz_bad elim!: MPair_analz intro: less_SucI)
paulson@13926
   312
txt{*Oops: PROOF FAILED if addIs below*}
paulson@13926
   313
apply (blast dest: unique_session_keys intro!: less_SucI)
paulson@13926
   314
done
paulson@5053
   315
paulson@5053
   316
paulson@13926
   317
(** CONFIDENTIALITY for the SERVER:
paulson@13926
   318
                     Spy does not see the keys sent in msg Kb2 
paulson@13926
   319
                     as long as they have NOT EXPIRED
paulson@13926
   320
**)
paulson@13926
   321
lemma Confidentiality_S:
paulson@13926
   322
     "[| Says Server A                                            
paulson@13926
   323
          (Crypt K' {|Number T, Agent B, Key K, X|}) \<in> set evs;   
paulson@13926
   324
         ~ Expired T evs;                                         
paulson@13926
   325
         A \<notin> bad;  B \<notin> bad;  evs \<in> kerberos_ban                 
paulson@13926
   326
      |] ==> Key K \<notin> analz (spies evs)"
paulson@13926
   327
apply (frule Says_Server_message_form, assumption)
paulson@13926
   328
apply (blast intro: lemma2)
paulson@13926
   329
done
paulson@13926
   330
paulson@13926
   331
(**** THE COUNTERPART OF CONFIDENTIALITY 
paulson@13926
   332
      [|...; Expired Ts evs; ...|] ==> Key K \<in> analz (spies evs)
paulson@13926
   333
      WOULD HOLD ONLY IF AN OOPS OCCURRED! ---> Nothing to prove!   ****)
paulson@13926
   334
paulson@13926
   335
paulson@13926
   336
(** CONFIDENTIALITY for ALICE: **)
paulson@13926
   337
(** Also A_trusts_K_by_Kb2 RS Confidentiality_S **)
paulson@13926
   338
lemma Confidentiality_A:
paulson@13926
   339
     "[| Crypt (shrK A) {|Number T, Agent B, Key K, X|} \<in> parts (spies evs); 
paulson@13926
   340
         ~ Expired T evs;           
paulson@13926
   341
         A \<notin> bad;  B \<notin> bad;  evs \<in> kerberos_ban                 
paulson@13926
   342
      |] ==> Key K \<notin> analz (spies evs)"
paulson@13926
   343
apply (blast dest!: A_trusts_K_by_Kb2 Confidentiality_S)
paulson@13926
   344
done
paulson@13926
   345
paulson@13926
   346
paulson@13926
   347
(** CONFIDENTIALITY for BOB: **)
paulson@13926
   348
(** Also B_trusts_K_by_Kb3 RS Confidentiality_S **)
paulson@13926
   349
lemma Confidentiality_B:
paulson@13926
   350
     "[| Crypt (shrK B) {|Number Tk, Agent A, Key K|}  
paulson@13926
   351
          \<in> parts (spies evs);               
paulson@13926
   352
        ~ Expired Tk evs;           
paulson@13926
   353
        A \<notin> bad;  B \<notin> bad;  evs \<in> kerberos_ban                 
paulson@13926
   354
      |] ==> Key K \<notin> analz (spies evs)"
paulson@13926
   355
apply (blast dest!: B_trusts_K_by_Kb3 Confidentiality_S)
paulson@13926
   356
done
paulson@13926
   357
paulson@5053
   358
paulson@13926
   359
lemma lemma_B [rule_format]:
paulson@13926
   360
     "[| B \<notin> bad;  evs \<in> kerberos_ban |]                         
paulson@13926
   361
      ==> Key K \<notin> analz (spies evs) -->                     
paulson@13926
   362
          Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})  
paulson@13926
   363
          \<in> set evs -->                                              
paulson@13926
   364
          Crypt K (Number Ta) \<in> parts (spies evs) -->         
paulson@13926
   365
          Says B A (Crypt K (Number Ta)) \<in> set evs"
paulson@13926
   366
apply (erule kerberos_ban.induct)
paulson@13926
   367
apply (frule_tac [7] Oops_parts_spies)
paulson@13926
   368
apply (frule_tac [5] Says_S_message_form)
paulson@13926
   369
apply (drule_tac [6] Kb3_msg_in_parts_spies, analz_mono_contra)
paulson@13926
   370
apply (simp_all (no_asm_simp) add: all_conj_distrib)
paulson@13926
   371
txt{*Fake*}
paulson@13926
   372
apply blast
paulson@13926
   373
txt{*Kb2*}
paulson@13926
   374
apply (force dest: Crypt_imp_invKey_keysFor) 
paulson@13926
   375
txt{*Kb4*}
paulson@13926
   376
apply (blast dest: B_trusts_K_by_Kb3 unique_session_keys 
paulson@13926
   377
                   Says_imp_spies [THEN analz.Inj] Crypt_Spy_analz_bad)
paulson@13926
   378
done
paulson@13926
   379
paulson@13926
   380
paulson@13926
   381
(*AUTHENTICATION OF B TO A*)
paulson@13926
   382
lemma Authentication_B:
paulson@13926
   383
     "[| Crypt K (Number Ta) \<in> parts (spies evs);            
paulson@13926
   384
         Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}     
paulson@13926
   385
         \<in> parts (spies evs);                                
paulson@13926
   386
         ~ Expired Ts evs;                                   
paulson@13926
   387
         A \<notin> bad;  B \<notin> bad;  evs \<in> kerberos_ban |]         
paulson@13926
   388
      ==> Says B A (Crypt K (Number Ta)) \<in> set evs"
paulson@13926
   389
by (blast dest!: A_trusts_K_by_Kb2
paulson@13926
   390
          intro!: lemma_B elim!: Confidentiality_S [THEN [2] rev_notE])
paulson@13926
   391
paulson@13926
   392
paulson@13926
   393
paulson@13926
   394
lemma lemma_A [rule_format]:
paulson@13926
   395
     "[| A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |] 
paulson@13926
   396
      ==>           
paulson@13926
   397
         Key K \<notin> analz (spies evs) -->          
paulson@13926
   398
         Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})   
paulson@13926
   399
         \<in> set evs -->   
paulson@13926
   400
          Crypt K {|Agent A, Number Ta|} \<in> parts (spies evs) --> 
paulson@13926
   401
         Says A B {|X, Crypt K {|Agent A, Number Ta|}|}   
paulson@13926
   402
             \<in> set evs"
paulson@13926
   403
apply (erule kerberos_ban.induct)
paulson@13926
   404
apply (frule_tac [7] Oops_parts_spies)
paulson@13926
   405
apply (frule_tac [5] Says_S_message_form)
paulson@13926
   406
apply (frule_tac [6] Kb3_msg_in_parts_spies, analz_mono_contra)
paulson@13926
   407
apply (simp_all (no_asm_simp) add: all_conj_distrib)
paulson@13926
   408
txt{*Fake*}
paulson@13926
   409
apply blast
paulson@13926
   410
txt{*Kb2*}
paulson@13926
   411
apply (force dest: Crypt_imp_invKey_keysFor) 
paulson@13926
   412
txt{*Kb3*}
paulson@13926
   413
apply (blast dest: A_trusts_K_by_Kb2 unique_session_keys)
paulson@13926
   414
done
paulson@13926
   415
paulson@13926
   416
paulson@13926
   417
(*AUTHENTICATION OF A TO B*)
paulson@13926
   418
lemma Authentication_A:
paulson@13926
   419
     "[| Crypt K {|Agent A, Number Ta|} \<in> parts (spies evs);   
paulson@13926
   420
         Crypt (shrK B) {|Number Ts, Agent A, Key K|}          
paulson@13926
   421
         \<in> parts (spies evs);                                  
paulson@13926
   422
         ~ Expired Ts evs;                                     
paulson@13926
   423
         A \<notin> bad;  B \<notin> bad;  evs \<in> kerberos_ban |]           
paulson@13926
   424
      ==> Says A B {|Crypt (shrK B) {|Number Ts, Agent A, Key K|},      
paulson@13926
   425
                     Crypt K {|Agent A, Number Ta|}|} \<in> set evs"
paulson@13926
   426
by (blast dest!: B_trusts_K_by_Kb3
paulson@13926
   427
          intro!: lemma_A 
paulson@13926
   428
          elim!: Confidentiality_S [THEN [2] rev_notE])
paulson@5053
   429
paulson@5053
   430
end