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