src/HOL/Auth/Kerberos_BAN.ML
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 7499 23e090051cb8
child 8741 61bc5ed22b62
permissions -rw-r--r--
tidied; added lemma restrict_to_left
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@5064
    11
paulson@5223
    12
  Confidentiality (secrecy) and authentication properties rely on 
paulson@5223
    13
  temporal checks: strong guarantees in a little abstracted - but
paulson@5223
    14
  very realistic - model (see .thy).
paulson@5053
    15
paulson@5223
    16
Tidied by lcp.
paulson@5053
    17
*)
paulson@5053
    18
paulson@5053
    19
AddEs spies_partsEs;
paulson@5053
    20
AddDs [impOfSubs analz_subset_parts];
paulson@5053
    21
AddDs [impOfSubs Fake_parts_insert];
paulson@5053
    22
paulson@5064
    23
AddIffs [SesKeyLife_LB, AutLife_LB];
paulson@5053
    24
paulson@5053
    25
paulson@5053
    26
(*A "possibility property": there are traces that reach the end.*)
paulson@5434
    27
Goal "EX Timestamp K. EX evs: kerberos_ban.    \
paulson@5114
    28
\            Says B A (Crypt K (Number Timestamp)) \
paulson@5114
    29
\                 : set evs";
paulson@5352
    30
by (cut_facts_tac [SesKeyLife_LB] 1);
paulson@5053
    31
by (REPEAT (resolve_tac [exI,bexI] 1));
paulson@5053
    32
by (rtac (kerberos_ban.Nil RS kerberos_ban.Kb1 RS kerberos_ban.Kb2 RS 
paulson@5053
    33
          kerberos_ban.Kb3 RS kerberos_ban.Kb4) 2);
paulson@5053
    34
by possibility_tac;
paulson@5352
    35
by (ALLGOALS Asm_simp_tac);
paulson@5053
    36
result();
paulson@5053
    37
paulson@5053
    38
paulson@5053
    39
paulson@5053
    40
(**** Inductive proofs about kerberos_ban ****)
paulson@5053
    41
paulson@5053
    42
(*Forwarding Lemma for reasoning about the encrypted portion of message Kb3*)
paulson@5114
    43
Goal "Says S A (Crypt KA {|Timestamp, B, K, X|}) : set evs \
paulson@5114
    44
\             ==> X : parts (spies evs)";
paulson@5053
    45
by (Blast_tac 1);
paulson@5053
    46
qed "Kb3_msg_in_parts_spies";
paulson@5053
    47
                              
paulson@5114
    48
Goal "Says Server A (Crypt (shrK A) {|Timestamp, B, K, X|}) : set evs \
paulson@5114
    49
\        ==> K : parts (spies evs)";
paulson@5053
    50
by (Blast_tac 1);
paulson@5053
    51
qed "Oops_parts_spies";
paulson@5053
    52
paulson@5053
    53
(*For proving the easier theorems about X ~: parts (spies evs).*)
paulson@5053
    54
fun parts_induct_tac i = 
paulson@5053
    55
    etac kerberos_ban.induct i  THEN 
wenzelm@7499
    56
    ftac Oops_parts_spies (i+6)  THEN
wenzelm@7499
    57
    ftac Kb3_msg_in_parts_spies (i+4)     THEN
paulson@5053
    58
    prove_simple_subgoals_tac i;
paulson@5053
    59
paulson@5053
    60
paulson@5053
    61
(*Spy never sees another agent's shared key! (unless it's bad at start)*)
paulson@5114
    62
Goal "evs : kerberos_ban ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
paulson@5053
    63
by (parts_induct_tac 1);
paulson@5053
    64
by (ALLGOALS Blast_tac);
paulson@5053
    65
qed "Spy_see_shrK";
paulson@5053
    66
Addsimps [Spy_see_shrK];
paulson@5053
    67
paulson@5053
    68
paulson@5114
    69
Goal "evs : kerberos_ban ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
paulson@5053
    70
by Auto_tac;
paulson@5053
    71
qed "Spy_analz_shrK";
paulson@5053
    72
Addsimps [Spy_analz_shrK];
paulson@5053
    73
paulson@5114
    74
Goal  "[| Key (shrK A) : parts (spies evs);       \
paulson@5114
    75
\               evs : kerberos_ban |] ==> A:bad";
paulson@5053
    76
by (blast_tac (claset() addDs [Spy_see_shrK]) 1);
paulson@5053
    77
qed "Spy_see_shrK_D";
paulson@5053
    78
paulson@5053
    79
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
paulson@5053
    80
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
paulson@5053
    81
paulson@5053
    82
paulson@5053
    83
(*Nobody can have used non-existent keys!*)
paulson@5114
    84
Goal "evs : kerberos_ban ==>      \
paulson@5114
    85
\      Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
paulson@5053
    86
by (parts_induct_tac 1);
paulson@5053
    87
(*Fake*)
paulson@5053
    88
by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
paulson@5053
    89
(*Kb2, Kb3, Kb4*)
paulson@5053
    90
by (ALLGOALS Blast_tac);
paulson@5053
    91
qed_spec_mp "new_keys_not_used";
paulson@5053
    92
paulson@5053
    93
bind_thm ("new_keys_not_analzd",
paulson@5053
    94
          [analz_subset_parts RS keysFor_mono,
paulson@5053
    95
           new_keys_not_used] MRS contra_subsetD);
paulson@5053
    96
paulson@5053
    97
Addsimps [new_keys_not_used, new_keys_not_analzd];
paulson@5053
    98
paulson@5053
    99
paulson@5053
   100
(** Lemmas concerning the form of items passed in messages **)
paulson@5053
   101
paulson@5053
   102
(*Describes the form of K, X and K' when the Server sends this message.*)
paulson@5114
   103
Goal "[| Says Server A (Crypt K' {|Number Ts, Agent B, Key K, X|})  \
paulson@5114
   104
\        : set evs; evs : kerberos_ban |]                           \
paulson@5114
   105
\     ==> K ~: range shrK &                                         \
paulson@5114
   106
\         X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}) &      \
paulson@5114
   107
\         K' = shrK A";
paulson@5053
   108
by (etac rev_mp 1);
paulson@5053
   109
by (etac kerberos_ban.induct 1);
paulson@5053
   110
by Auto_tac;
paulson@5053
   111
qed "Says_Server_message_form";
paulson@5053
   112
paulson@5053
   113
paulson@5053
   114
(*If the encrypted message appears then it originated with the Server
paulson@5053
   115
  PROVIDED that A is NOT compromised!
paulson@5053
   116
paulson@5053
   117
  This shows implicitly the FRESHNESS OF THE SESSION KEY to A
paulson@5053
   118
*)
paulson@5114
   119
Goal "[| Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} \
paulson@5114
   120
\          : parts (spies evs);                          \
paulson@5114
   121
\        A ~: bad;  evs : kerberos_ban |]                \
paulson@5114
   122
\      ==> Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \
paulson@5114
   123
\            : set evs";
paulson@5053
   124
by (etac rev_mp 1);
paulson@5053
   125
by (parts_induct_tac 1);
paulson@5053
   126
by (Blast_tac 1);
paulson@5053
   127
qed "A_trusts_K_by_Kb2";
paulson@5053
   128
paulson@5053
   129
paulson@5053
   130
(*If the TICKET appears then it originated with the Server*)
paulson@5053
   131
(*FRESHNESS OF THE SESSION KEY to B*)
paulson@5114
   132
Goal "[| Crypt (shrK B) {|Number Ts, Agent A, Key K|} : parts (spies evs); \
paulson@5114
   133
\        B ~: bad;  evs : kerberos_ban |]                        \
paulson@5114
   134
\      ==> Says Server A                                         \
paulson@5114
   135
\           (Crypt (shrK A) {|Number Ts, Agent B, Key K,                   \
paulson@5114
   136
\                         Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})  \
paulson@5114
   137
\          : set evs";
paulson@5053
   138
by (etac rev_mp 1);
paulson@5053
   139
by (parts_induct_tac 1);
paulson@5053
   140
by (Blast_tac 1);
paulson@5053
   141
qed "B_trusts_K_by_Kb3";
paulson@5053
   142
paulson@5053
   143
paulson@5053
   144
(*EITHER describes the form of X when the following message is sent, 
paulson@5053
   145
  OR     reduces it to the Fake case.
paulson@5053
   146
  Use Says_Server_message_form if applicable.*)
paulson@5114
   147
Goal "[| Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})     \
paulson@5114
   148
\           : set evs;                                                  \
paulson@5114
   149
\        evs : kerberos_ban |]                                          \
paulson@5114
   150
\==> (K ~: range shrK & X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}))\
paulson@5114
   151
\         | X : analz (spies evs)";
paulson@5053
   152
by (case_tac "A : bad" 1);
paulson@5053
   153
by (fast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]
paulson@5053
   154
                      addss (simpset())) 1);
paulson@5053
   155
by (forward_tac [Says_imp_spies RS parts.Inj] 1);
paulson@5053
   156
by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2, 
paulson@5053
   157
				Says_Server_message_form]) 1);
paulson@5053
   158
qed "Says_S_message_form";
paulson@5053
   159
paulson@5053
   160
paulson@5053
   161
(*For proofs involving analz.*)
paulson@5053
   162
val analz_spies_tac = 
wenzelm@7499
   163
    ftac Says_Server_message_form 7 THEN
wenzelm@7499
   164
    ftac Says_S_message_form 5 THEN 
paulson@5053
   165
    REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac);
paulson@5053
   166
paulson@5053
   167
paulson@5053
   168
(****
paulson@5053
   169
 The following is to prove theorems of the form
paulson@5053
   170
paulson@5053
   171
  Key K : analz (insert (Key KAB) (spies evs)) ==>
paulson@5053
   172
  Key K : analz (spies evs)
paulson@5053
   173
paulson@5053
   174
 A more general formula must be proved inductively.
paulson@5053
   175
paulson@5053
   176
****)
paulson@5053
   177
paulson@5053
   178
paulson@5053
   179
(** Session keys are not used to encrypt other session keys **)
paulson@5053
   180
paulson@5114
   181
Goal "evs : kerberos_ban ==>                          \
paulson@5492
   182
\  ALL K KK. KK <= - (range shrK) -->                 \
paulson@5114
   183
\         (Key K : analz (Key``KK Un (spies evs))) =  \
paulson@5114
   184
\         (K : KK | Key K : analz (spies evs))";
paulson@5053
   185
by (etac kerberos_ban.induct 1);
paulson@5053
   186
by analz_spies_tac;
paulson@5053
   187
by (REPEAT_FIRST (resolve_tac [allI, impI]));
paulson@5053
   188
by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
paulson@5053
   189
(*Takes 5 secs*)
paulson@5053
   190
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
paulson@5053
   191
(*Fake*) 
paulson@5053
   192
by (spy_analz_tac 1);
paulson@5053
   193
qed_spec_mp "analz_image_freshK";
paulson@5053
   194
paulson@5053
   195
paulson@5114
   196
Goal "[| evs : kerberos_ban;  KAB ~: range shrK |] ==>     \
paulson@5114
   197
\     Key K : analz (insert (Key KAB) (spies evs)) =       \
paulson@5114
   198
\     (K = KAB | Key K : analz (spies evs))";
paulson@5053
   199
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
paulson@5053
   200
qed "analz_insert_freshK";
paulson@5053
   201
paulson@5053
   202
paulson@5053
   203
(** The session key K uniquely identifies the message **)
paulson@5053
   204
paulson@5114
   205
Goal "evs : kerberos_ban ==>                                         \
paulson@5114
   206
\   EX A' Ts' B' X'. ALL A Ts B X.                                   \
paulson@5114
   207
\    Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \
paulson@5114
   208
\          : set evs \
paulson@5114
   209
\    -->         A=A' & Ts=Ts' & B=B' & X=X'";
paulson@5053
   210
by (etac kerberos_ban.induct 1);
paulson@5053
   211
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
paulson@5053
   212
by Safe_tac;
paulson@5053
   213
(*Kb2: it can't be a new key*)
paulson@5053
   214
by (expand_case_tac "K = ?y" 1);
paulson@5053
   215
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
paulson@5053
   216
by (blast_tac (claset() delrules [conjI]) 1);
paulson@5053
   217
val lemma = result();
paulson@5053
   218
paulson@5053
   219
(*In messages of this form, the session key uniquely identifies the rest*)
paulson@5114
   220
Goal "[| Says Server A                                    \
paulson@5114
   221
\          (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) : set evs; \ 
paulson@5114
   222
\        Says Server A'                                   \
paulson@5114
   223
\         (Crypt (shrK A') {|Number Ts', Agent B', Key K, X'|}) : set evs;\
paulson@5114
   224
\        evs : kerberos_ban |] ==> A=A' & Ts=Ts' & B=B' & X = X'";
paulson@5053
   225
by (prove_unique_tac lemma 1);
paulson@5053
   226
qed "unique_session_keys";
paulson@5053
   227
paulson@5053
   228
paulson@5053
   229
(** Lemma: the session key sent in msg Kb2 would be EXPIRED
paulson@5053
   230
    if the spy could see it!
paulson@5053
   231
**)
paulson@5053
   232
paulson@5114
   233
Goal "[| A ~: bad;  B ~: bad;  evs : kerberos_ban |]           \
paulson@5114
   234
\ ==> Says Server A                                            \
paulson@5114
   235
\         (Crypt (shrK A) {|Number Ts, Agent B, Key K,         \
paulson@5114
   236
\                           Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})\
paulson@5114
   237
\        : set evs -->                                         \
paulson@5114
   238
\     Key K : analz (spies evs) --> Expired Ts evs"; 
paulson@5053
   239
by (etac kerberos_ban.induct 1);
paulson@5053
   240
by analz_spies_tac;
paulson@5053
   241
by (ALLGOALS
paulson@5535
   242
    (asm_simp_tac (simpset() addsimps [analz_insert_eq, analz_insert_freshK]
paulson@5535
   243
				      @ pushes)));
paulson@5053
   244
(*Oops*)
paulson@5053
   245
by (blast_tac (claset() addDs [unique_session_keys] addIs [less_SucI]) 4);
paulson@5053
   246
(*Kb2*)
paulson@5064
   247
by (blast_tac (claset() addIs [parts_insertI, less_SucI]) 2);
paulson@5053
   248
(*Fake*) 
paulson@5053
   249
by (spy_analz_tac 1);
paulson@5053
   250
(**LEVEL 6 **)
paulson@5064
   251
(*Kb3*)
paulson@5053
   252
by (case_tac "Aa : bad" 1);
paulson@5064
   253
by (blast_tac (claset() addDs [A_trusts_K_by_Kb2, unique_session_keys]) 2);
paulson@5064
   254
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj,
paulson@5064
   255
                               Crypt_Spy_analz_bad, analz.Fst, analz.Snd]
paulson@5053
   256
                        addIs [less_SucI]) 1);
paulson@5479
   257
qed_spec_mp "lemma2";
paulson@5053
   258
paulson@5053
   259
paulson@5053
   260
(** CONFIDENTIALITY for the SERVER:
paulson@5053
   261
                     Spy does not see the keys sent in msg Kb2 
paulson@5053
   262
                     as long as they have NOT EXPIRED
paulson@5053
   263
**)
paulson@5114
   264
Goal "[| Says Server A                                           \
paulson@5114
   265
\         (Crypt K' {|Number T, Agent B, Key K, X|}) : set evs;  \
paulson@5114
   266
\        ~ Expired T evs;                                        \
paulson@5114
   267
\        A ~: bad;  B ~: bad;  evs : kerberos_ban                \
paulson@5114
   268
\     |] ==> Key K ~: analz (spies evs)";
wenzelm@7499
   269
by (ftac Says_Server_message_form 1 THEN assume_tac 1);
paulson@5479
   270
by (blast_tac (claset() addIs [lemma2]) 1);
paulson@5053
   271
qed "Confidentiality_S";
paulson@5053
   272
paulson@5053
   273
(**** THE COUNTERPART OF CONFIDENTIALITY 
paulson@5053
   274
      [|...; Expired Ts evs; ...|] ==> Key K : analz (spies evs)
paulson@5053
   275
      WOULD HOLD ONLY IF AN OOPS OCCURRED! ---> Nothing to prove!   ****)
paulson@5053
   276
paulson@5053
   277
paulson@5053
   278
(** CONFIDENTIALITY for ALICE: **)
paulson@5053
   279
(** Also A_trusts_K_by_Kb2 RS Confidentiality_S **)
paulson@5114
   280
Goal "[| Crypt (shrK A) {|Number T, Agent B, Key K, X|} : parts (spies evs);\
paulson@5114
   281
\        ~ Expired T evs;          \
paulson@5114
   282
\        A ~: bad;  B ~: bad;  evs : kerberos_ban                \
paulson@5114
   283
\     |] ==> Key K ~: analz (spies evs)";
paulson@5064
   284
by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2, Confidentiality_S]) 1);
paulson@5053
   285
qed "Confidentiality_A";
paulson@5053
   286
paulson@5053
   287
paulson@5053
   288
(** CONFIDENTIALITY for BOB: **)
paulson@5053
   289
(** Also B_trusts_K_by_Kb3 RS Confidentiality_S **)
paulson@5114
   290
Goal "[| Crypt (shrK B) {|Number Tk, Agent A, Key K|} \
paulson@5114
   291
\         : parts (spies evs);              \
paulson@5114
   292
\       ~ Expired Tk evs;          \
paulson@5114
   293
\       A ~: bad;  B ~: bad;  evs : kerberos_ban                \
paulson@5114
   294
\     |] ==> Key K ~: analz (spies evs)";             
paulson@5053
   295
by (blast_tac (claset() addSDs [B_trusts_K_by_Kb3, 
paulson@5053
   296
                                Confidentiality_S]) 1);
paulson@5053
   297
qed "Confidentiality_B";
paulson@5053
   298
paulson@5053
   299
paulson@5114
   300
Goal "[| B ~: bad;  evs : kerberos_ban |]                        \
paulson@5114
   301
\     ==> Key K ~: analz (spies evs) -->                    \
paulson@5114
   302
\         Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \
paulson@5114
   303
\         : set evs -->                                             \
paulson@5114
   304
\         Crypt K (Number Ta) : parts (spies evs) -->        \
paulson@5114
   305
\         Says B A (Crypt K (Number Ta)) : set evs";
paulson@5053
   306
by (etac kerberos_ban.induct 1);
wenzelm@7499
   307
by (ftac Says_S_message_form 5 THEN assume_tac 5);     
paulson@5053
   308
by (dtac Kb3_msg_in_parts_spies 5);
wenzelm@7499
   309
by (ftac Oops_parts_spies 7);
paulson@5064
   310
by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
paulson@5053
   311
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
paulson@5064
   312
(**LEVEL 6**)
paulson@5053
   313
by (Blast_tac 1);
paulson@5064
   314
by (Clarify_tac 1);
paulson@5053
   315
(*
paulson@5053
   316
Subgoal 1: contradiction from the assumptions  
paulson@5053
   317
Key K ~: used evs2  and Crypt K (Number Ta) : parts (spies evs2)
paulson@5053
   318
*)
paulson@5053
   319
by (dtac Crypt_imp_invKey_keysFor 1);
paulson@5053
   320
by (Asm_full_simp_tac 1);
paulson@5064
   321
(* the two tactics above detect the contradiction*)
paulson@5053
   322
by (case_tac "Ba : bad" 1);  (*splits up the subgoal by the stated case*)
paulson@5053
   323
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS 
paulson@5053
   324
                              B_trusts_K_by_Kb3, 
paulson@5053
   325
			      unique_session_keys]) 2);
paulson@5053
   326
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS analz.Fst RS 
paulson@5053
   327
			      Crypt_Spy_analz_bad]) 1);
paulson@5053
   328
val lemma_B = result();
paulson@5053
   329
paulson@5053
   330
paulson@5053
   331
(*AUTHENTICATION OF B TO A*)
paulson@5114
   332
Goal "[| Crypt K (Number Ta) : parts (spies evs);           \
paulson@5114
   333
\        Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}    \
paulson@5114
   334
\        : parts (spies evs);                               \
paulson@5114
   335
\        ~ Expired Ts evs;                                  \
paulson@5114
   336
\        A ~: bad;  B ~: bad;  evs : kerberos_ban |]        \
paulson@5114
   337
\     ==> Says B A (Crypt K (Number Ta)) : set evs";
paulson@5053
   338
by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2]
paulson@5053
   339
                        addSIs [lemma_B RS mp RS mp RS mp]
paulson@5053
   340
                        addSEs [Confidentiality_S RSN (2,rev_notE)]) 1);
paulson@5053
   341
qed "Authentication_B";
paulson@5053
   342
paulson@5053
   343
paulson@5114
   344
Goal "[| A ~: bad; B ~: bad; evs : kerberos_ban |]      ==>         \ 
paulson@5114
   345
\        Key K ~: analz (spies evs) -->         \
paulson@5114
   346
\        Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})  \
paulson@5114
   347
\        : set evs -->  \
paulson@5114
   348
\         Crypt K {|Agent A, Number Ta|} : parts (spies evs) -->\
paulson@5114
   349
\        Says A B {|X, Crypt K {|Agent A, Number Ta|}|}  \
paulson@5114
   350
\            : set evs";
paulson@5053
   351
by (etac kerberos_ban.induct 1);
wenzelm@7499
   352
by (ftac Says_S_message_form 5 THEN assume_tac 5);     
wenzelm@7499
   353
by (ftac Kb3_msg_in_parts_spies 5);
wenzelm@7499
   354
by (ftac Oops_parts_spies 7);
paulson@5064
   355
by (REPEAT (FIRSTGOAL analz_mono_contra_tac));
paulson@5053
   356
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
paulson@5064
   357
(**LEVEL 6**)
paulson@5053
   358
by (Blast_tac 1);
paulson@5064
   359
by (Clarify_tac 1);
paulson@5053
   360
by (dtac Crypt_imp_invKey_keysFor 1);
paulson@5053
   361
by (Asm_full_simp_tac 1);
paulson@5064
   362
by (blast_tac (claset() addDs [A_trusts_K_by_Kb2, unique_session_keys]) 1);
paulson@5053
   363
val lemma_A = result();
paulson@5053
   364
paulson@5053
   365
paulson@5053
   366
(*AUTHENTICATION OF A TO B*)
paulson@5114
   367
Goal "[| Crypt K {|Agent A, Number Ta|} : parts (spies evs);  \
paulson@5114
   368
\        Crypt (shrK B) {|Number Ts, Agent A, Key K|}         \
paulson@5114
   369
\        : parts (spies evs);                                 \
paulson@5114
   370
\        ~ Expired Ts evs;                                    \
paulson@5114
   371
\        A ~: bad;  B ~: bad;  evs : kerberos_ban |]          \
paulson@5114
   372
\     ==> Says A B {|Crypt (shrK B) {|Number Ts, Agent A, Key K|}, \    
paulson@5114
   373
\                    Crypt K {|Agent A, Number Ta|}|} : set evs";
paulson@5053
   374
by (blast_tac (claset() addSDs [B_trusts_K_by_Kb3]
paulson@5053
   375
                        addSIs [lemma_A RS mp RS mp RS mp]
paulson@5053
   376
                        addSEs [Confidentiality_S RSN (2,rev_notE)]) 1);
paulson@5053
   377
qed "Authentication_A";