src/HOL/Auth/Yahalom2.ML
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 7499 23e090051cb8
child 10833 c0844a30ea4e
permissions -rw-r--r--
tidied; added lemma restrict_to_left
paulson@2111
     1
(*  Title:      HOL/Auth/Yahalom2
paulson@2111
     2
    ID:         $Id$
paulson@2111
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@2111
     4
    Copyright   1996  University of Cambridge
paulson@2111
     5
paulson@2111
     6
Inductive relation "yahalom" for the Yahalom protocol, Variant 2.
paulson@2111
     7
paulson@2111
     8
This version trades encryption of NB for additional explicitness in YM3.
paulson@2111
     9
paulson@2111
    10
From page 259 of
paulson@2111
    11
  Burrows, Abadi and Needham.  A Logic of Authentication.
paulson@2111
    12
  Proc. Royal Soc. 426 (1989)
paulson@2111
    13
*)
paulson@2111
    14
paulson@6335
    15
AddEs knows_Spy_partsEs;
paulson@5066
    16
AddDs [impOfSubs analz_subset_parts];
paulson@5066
    17
AddDs [impOfSubs Fake_parts_insert];
paulson@5066
    18
paulson@5066
    19
paulson@2323
    20
(*A "possibility property": there are traces that reach the end*)
paulson@5434
    21
Goal "EX X NB K. EX evs: yahalom.          \
paulson@5114
    22
\            Says A B {|X, Crypt K (Nonce NB)|} : set evs";
paulson@2111
    23
by (REPEAT (resolve_tac [exI,bexI] 1));
paulson@6335
    24
by (rtac (yahalom.Nil RS 
paulson@6335
    25
          yahalom.YM1 RS yahalom.Reception RS
paulson@6335
    26
          yahalom.YM2 RS yahalom.Reception RS 
paulson@6335
    27
          yahalom.YM3 RS yahalom.Reception RS yahalom.YM4) 2);
paulson@2516
    28
by possibility_tac;
paulson@2111
    29
result();
paulson@2111
    30
paulson@6335
    31
Goal "[| Gets B X : set evs; evs : yahalom |] ==> EX A. Says A B X : set evs";
paulson@6335
    32
by (etac rev_mp 1);
paulson@6335
    33
by (etac yahalom.induct 1);
paulson@6335
    34
by Auto_tac;
paulson@6335
    35
qed "Gets_imp_Says";
paulson@6335
    36
paulson@6335
    37
(*Must be proved separately for each protocol*)
paulson@6335
    38
Goal "[| Gets B X : set evs; evs : yahalom |]  ==> X : knows Spy evs";
paulson@6335
    39
by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1);
paulson@6335
    40
qed"Gets_imp_knows_Spy";
paulson@6335
    41
AddDs [Gets_imp_knows_Spy RS parts.Inj];
paulson@6335
    42
paulson@2111
    43
paulson@2111
    44
(**** Inductive proofs about yahalom ****)
paulson@2111
    45
paulson@2111
    46
(** For reasoning about the encrypted portion of messages **)
paulson@2111
    47
paulson@2111
    48
(*Lets us treat YM4 using a similar argument as for the Fake case.*)
paulson@6335
    49
Goal "[| Gets A {|NB, Crypt (shrK A) Y, X|} : set evs;  evs : yahalom |]  \
paulson@6335
    50
\     ==> X : analz (knows Spy evs)";
paulson@6335
    51
by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);
paulson@6335
    52
qed "YM4_analz_knows_Spy";
paulson@2111
    53
paulson@6335
    54
bind_thm ("YM4_parts_knows_Spy",
paulson@6335
    55
          YM4_analz_knows_Spy RS (impOfSubs analz_subset_parts));
paulson@2111
    56
paulson@6335
    57
(*For Oops*)
paulson@6335
    58
Goal "Says Server A {|NB, Crypt (shrK A) {|B,K,NA|}, X|} : set evs \
paulson@6335
    59
\     ==> K : parts (knows Spy evs)";
paulson@6335
    60
by (blast_tac (claset() addSEs partsEs
paulson@6335
    61
                        addSDs [Says_imp_knows_Spy RS parts.Inj]) 1);
paulson@6335
    62
qed "YM4_Key_parts_knows_Spy";
paulson@2111
    63
paulson@6335
    64
(*For proving the easier theorems about X ~: parts (knows Spy evs).*)
paulson@6335
    65
fun parts_knows_Spy_tac i = 
paulson@6335
    66
  EVERY
wenzelm@7499
    67
   [ftac YM4_Key_parts_knows_Spy (i+7),
wenzelm@7499
    68
    ftac YM4_parts_knows_Spy (i+6), assume_tac (i+6),
paulson@6335
    69
    prove_simple_subgoals_tac i];
paulson@2111
    70
paulson@3519
    71
(*Induction for regularity theorems.  If induction formula has the form
paulson@6335
    72
   X ~: analz (knows Spy evs) --> ... then it shortens the proof by discarding
paulson@6335
    73
   needless information about analz (insert X (knows Spy evs))  *)
paulson@3519
    74
fun parts_induct_tac i = 
paulson@3519
    75
    etac yahalom.induct i
paulson@3519
    76
    THEN 
paulson@3519
    77
    REPEAT (FIRSTGOAL analz_mono_contra_tac)
paulson@6335
    78
    THEN  parts_knows_Spy_tac i;
paulson@3432
    79
paulson@2111
    80
paulson@6335
    81
(** Theorems of the form X ~: parts (knows Spy evs) imply that NOBODY
paulson@2111
    82
    sends messages containing X! **)
paulson@2111
    83
paulson@3683
    84
(*Spy never sees another agent's shared key! (unless it's bad at start)*)
paulson@6335
    85
Goal "evs : yahalom ==> (Key (shrK A) : parts (knows Spy evs)) = (A : bad)";
paulson@3519
    86
by (parts_induct_tac 1);
paulson@5066
    87
by (ALLGOALS Blast_tac);
paulson@2516
    88
qed "Spy_see_shrK";
paulson@2516
    89
Addsimps [Spy_see_shrK];
paulson@2111
    90
paulson@6335
    91
Goal "evs : yahalom ==> (Key (shrK A) : analz (knows Spy evs)) = (A : bad)";
paulson@5066
    92
by Auto_tac;
paulson@2516
    93
qed "Spy_analz_shrK";
paulson@2516
    94
Addsimps [Spy_analz_shrK];
paulson@2111
    95
paulson@4471
    96
AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
paulson@4471
    97
	Spy_analz_shrK RSN (2, rev_iffD1)];
paulson@2111
    98
paulson@2111
    99
paulson@3432
   100
(*Nobody can have used non-existent keys!  Needed to apply analz_insert_Key*)
paulson@5114
   101
Goal "evs : yahalom ==>          \
paulson@6335
   102
\      Key K ~: used evs --> K ~: keysFor (parts (knows Spy evs))";
paulson@3519
   103
by (parts_induct_tac 1);
paulson@2516
   104
(*YM4: Key K is not fresh!*)
paulson@5066
   105
by (Blast_tac 3);
paulson@2516
   106
(*YM3*)
wenzelm@4091
   107
by (blast_tac (claset() addss (simpset())) 2);
paulson@2516
   108
(*Fake*)
paulson@4509
   109
by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
paulson@2160
   110
qed_spec_mp "new_keys_not_used";
paulson@2111
   111
paulson@2111
   112
bind_thm ("new_keys_not_analzd",
paulson@2111
   113
          [analz_subset_parts RS keysFor_mono,
paulson@2111
   114
           new_keys_not_used] MRS contra_subsetD);
paulson@2111
   115
paulson@2111
   116
Addsimps [new_keys_not_used, new_keys_not_analzd];
paulson@2111
   117
paulson@2155
   118
(*Describes the form of K when the Server sends this message.  Useful for
paulson@2155
   119
  Oops as well as main secrecy property.*)
paulson@5114
   120
Goal "[| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|} \
paulson@5114
   121
\         : set evs;                                            \
paulson@5114
   122
\        evs : yahalom |]                                       \
paulson@5434
   123
\     ==> K ~: range shrK";
paulson@2155
   124
by (etac rev_mp 1);
paulson@2155
   125
by (etac yahalom.induct 1);
paulson@3121
   126
by (ALLGOALS Asm_simp_tac);
paulson@2155
   127
qed "Says_Server_message_form";
paulson@2111
   128
paulson@2111
   129
paulson@3519
   130
(*For proofs involving analz.*)
paulson@6335
   131
val analz_knows_Spy_tac = 
paulson@6335
   132
    dtac YM4_analz_knows_Spy 7 THEN assume_tac 7 THEN
wenzelm@7499
   133
    ftac Says_Server_message_form 8 THEN
paulson@6335
   134
    assume_tac 8 THEN
paulson@6335
   135
    REPEAT ((etac conjE ORELSE' hyp_subst_tac) 8);
paulson@2111
   136
paulson@2111
   137
paulson@2111
   138
(****
paulson@2111
   139
 The following is to prove theorems of the form
paulson@2111
   140
paulson@6335
   141
          Key K : analz (insert (Key KAB) (knows Spy evs)) ==>
paulson@6335
   142
          Key K : analz (knows Spy evs)
paulson@2111
   143
paulson@2111
   144
 A more general formula must be proved inductively.
paulson@2111
   145
paulson@2111
   146
****)
paulson@2111
   147
paulson@2111
   148
(** Session keys are not used to encrypt other session keys **)
paulson@2111
   149
paulson@5114
   150
Goal "evs : yahalom ==>                               \
paulson@5492
   151
\  ALL K KK. KK <= - (range shrK) -->                 \
paulson@6335
   152
\         (Key K : analz (Key``KK Un (knows Spy evs))) =  \
paulson@6335
   153
\         (K : KK | Key K : analz (knows Spy evs))";
paulson@2111
   154
by (etac yahalom.induct 1);
paulson@6335
   155
by analz_knows_Spy_tac;
paulson@2516
   156
by (REPEAT_FIRST (resolve_tac [allI, impI]));
paulson@3961
   157
by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
paulson@2516
   158
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
paulson@3450
   159
(*Fake*) 
paulson@4422
   160
by (spy_analz_tac 1);
paulson@2516
   161
qed_spec_mp "analz_image_freshK";
paulson@2111
   162
paulson@5114
   163
Goal "[| evs : yahalom;  KAB ~: range shrK |] ==>     \
paulson@6335
   164
\     Key K : analz (insert (Key KAB) (knows Spy evs)) =  \
paulson@6335
   165
\     (K = KAB | Key K : analz (knows Spy evs))";
paulson@2516
   166
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
paulson@2516
   167
qed "analz_insert_freshK";
paulson@2111
   168
paulson@2111
   169
paulson@2111
   170
(*** The Key K uniquely identifies the Server's  message. **)
paulson@2111
   171
paulson@5114
   172
Goal "evs : yahalom ==>                                     \
paulson@5114
   173
\   EX A' B' na' nb' X'. ALL A B na nb X.                   \
paulson@5114
   174
\       Says Server A                                       \
paulson@5114
   175
\        {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|}   \
paulson@5114
   176
\       : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
paulson@2111
   177
by (etac yahalom.induct 1);
wenzelm@4091
   178
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
paulson@3730
   179
by (Clarify_tac 1);
paulson@2111
   180
(*Remaining case: YM3*)
paulson@2111
   181
by (expand_case_tac "K = ?y" 1);
paulson@2111
   182
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
paulson@2516
   183
(*...we assume X is a recent message and handle this case by contradiction*)
paulson@5066
   184
by (blast_tac (claset() delrules [conjI]    (*prevent splitup into 4 subgoals*)
paulson@4199
   185
                        addss (simpset() addsimps [parts_insertI])) 1);
paulson@2111
   186
val lemma = result();
paulson@2111
   187
paulson@5114
   188
Goal "[| Says Server A                                            \
paulson@5114
   189
\         {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} : set evs; \
paulson@5114
   190
\       Says Server A'                                           \
paulson@5114
   191
\         {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|} : set evs; \
paulson@5114
   192
\       evs : yahalom |]                                         \
paulson@5114
   193
\    ==> A=A' & B=B' & na=na' & nb=nb'";
paulson@2451
   194
by (prove_unique_tac lemma 1);
paulson@2111
   195
qed "unique_session_keys";
paulson@2111
   196
paulson@2111
   197
paulson@2111
   198
(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
paulson@2111
   199
paulson@5434
   200
Goal "[| A ~: bad;  B ~: bad;  evs : yahalom |]              \
paulson@5114
   201
\     ==> Says Server A                                      \
paulson@5114
   202
\           {|nb, Crypt (shrK A) {|Agent B, Key K, na|},     \
paulson@5114
   203
\                 Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} \
paulson@5114
   204
\          : set evs -->                                     \
paulson@5114
   205
\         Notes Spy {|na, nb, Key K|} ~: set evs -->         \
paulson@6335
   206
\         Key K ~: analz (knows Spy evs)";
paulson@2111
   207
by (etac yahalom.induct 1);
paulson@6335
   208
by analz_knows_Spy_tac;
paulson@2111
   209
by (ALLGOALS
paulson@2111
   210
    (asm_simp_tac 
nipkow@4831
   211
     (simpset() addsimps split_ifs
nipkow@4686
   212
	        addsimps [analz_insert_eq, analz_insert_freshK])));
paulson@3450
   213
(*Oops*)
wenzelm@4091
   214
by (blast_tac (claset() addDs [unique_session_keys]) 3);
paulson@5932
   215
(*YM3: delete a useless induction hypothesis*)
paulson@5932
   216
by (thin_tac "?P-->?Q" 2);
paulson@5932
   217
by (Blast_tac 2);
paulson@3450
   218
(*Fake*) 
paulson@3450
   219
by (spy_analz_tac 1);
paulson@2111
   220
val lemma = result() RS mp RS mp RSN(2,rev_notE);
paulson@2111
   221
paulson@2111
   222
paulson@3432
   223
(*Final version*)
paulson@5114
   224
Goal "[| Says Server A                                    \
paulson@5114
   225
\           {|nb, Crypt (shrK A) {|Agent B, Key K, na|},  \
paulson@5114
   226
\                 Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}    \
paulson@5114
   227
\        : set evs;                                       \
paulson@5114
   228
\        Notes Spy {|na, nb, Key K|} ~: set evs;          \
paulson@5114
   229
\        A ~: bad;  B ~: bad;  evs : yahalom |]           \
paulson@6335
   230
\     ==> Key K ~: analz (knows Spy evs)";
wenzelm@7499
   231
by (ftac Says_Server_message_form 1 THEN assume_tac 1);
wenzelm@4091
   232
by (blast_tac (claset() addSEs [lemma]) 1);
paulson@2111
   233
qed "Spy_not_see_encrypted_key";
paulson@2111
   234
paulson@2111
   235
paulson@3450
   236
(** Security Guarantee for A upon receiving YM3 **)
paulson@2155
   237
paulson@3432
   238
(*If the encrypted message appears then it originated with the Server.
paulson@3432
   239
  May now apply Spy_not_see_encrypted_key, subject to its conditions.*)
paulson@5114
   240
Goal "[| Crypt (shrK A) {|Agent B, Key K, na|}                      \
paulson@6335
   241
\         : parts (knows Spy evs);                                      \
paulson@5114
   242
\        A ~: bad;  evs : yahalom |]                                \
paulson@5114
   243
\      ==> EX nb. Says Server A                                     \
paulson@5114
   244
\                   {|nb, Crypt (shrK A) {|Agent B, Key K, na|},    \
paulson@5114
   245
\                         Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} \
paulson@5114
   246
\                 : set evs";
paulson@2155
   247
by (etac rev_mp 1);
paulson@3519
   248
by (parts_induct_tac 1);
paulson@5066
   249
by (ALLGOALS Blast_tac);
paulson@2323
   250
qed "A_trusts_YM3";
paulson@2155
   251
paulson@4598
   252
(*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
paulson@6335
   253
Goal "[| Crypt (shrK A) {|Agent B, Key K, na|} : parts (knows Spy evs); \
paulson@5114
   254
\        ALL nb. Notes Spy {|na, nb, Key K|} ~: set evs;            \
paulson@5114
   255
\        A ~: bad;  B ~: bad;  evs : yahalom |]                     \
paulson@6335
   256
\     ==> Key K ~: analz (knows Spy evs)";
paulson@4598
   257
by (blast_tac (claset() addSDs [A_trusts_YM3, Spy_not_see_encrypted_key]) 1);
paulson@4598
   258
qed "A_gets_good_key";
paulson@4598
   259
paulson@2111
   260
paulson@3450
   261
(** Security Guarantee for B upon receiving YM4 **)
paulson@3450
   262
paulson@2111
   263
(*B knows, by the first part of A's message, that the Server distributed 
paulson@5066
   264
  the key for A and B, and has associated it with NB.*)
paulson@5114
   265
Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|} \
paulson@6335
   266
\          : parts (knows Spy evs);                               \
paulson@5114
   267
\        B ~: bad;  evs : yahalom |]                          \
paulson@5066
   268
\ ==> EX NA. Says Server A                                       \
paulson@5114
   269
\            {|Nonce NB,                                      \
paulson@5114
   270
\              Crypt (shrK A) {|Agent B, Key K, Nonce NA|},   \
paulson@5114
   271
\              Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|} \
paulson@5114
   272
\            : set evs";
paulson@2111
   273
by (etac rev_mp 1);
paulson@3519
   274
by (parts_induct_tac 1);
paulson@5066
   275
by (ALLGOALS Blast_tac);
paulson@2111
   276
qed "B_trusts_YM4_shrK";
paulson@2111
   277
paulson@3450
   278
paulson@3450
   279
(*With this protocol variant, we don't need the 2nd part of YM4 at all:
paulson@3450
   280
  Nonce NB is available in the first part.*)
paulson@2111
   281
paulson@2155
   282
(*What can B deduce from receipt of YM4?  Stronger and simpler than Yahalom
paulson@2155
   283
  because we do not have to show that NB is secret. *)
paulson@6335
   284
Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \
paulson@5114
   285
\                    X|}                                         \
paulson@5114
   286
\          : set evs;                                            \
paulson@5114
   287
\        A ~: bad;  B ~: bad;  evs : yahalom |]                  \
paulson@5066
   288
\ ==> EX NA. Says Server A                                          \
paulson@5114
   289
\            {|Nonce NB,                                         \
paulson@5114
   290
\              Crypt (shrK A) {|Agent B, Key K, Nonce NA|},      \
paulson@5114
   291
\              Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|} \
paulson@5114
   292
\           : set evs";
wenzelm@4091
   293
by (blast_tac (claset() addSDs [B_trusts_YM4_shrK]) 1);
paulson@2323
   294
qed "B_trusts_YM4";
paulson@3432
   295
paulson@3432
   296
paulson@4598
   297
(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
paulson@6335
   298
Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \
paulson@5114
   299
\                    X|}                                         \
paulson@5114
   300
\          : set evs;                                            \
paulson@5114
   301
\        ALL na. Notes Spy {|na, Nonce NB, Key K|} ~: set evs;   \
paulson@5114
   302
\        A ~: bad;  B ~: bad;  evs : yahalom |]                  \
paulson@6335
   303
\     ==> Key K ~: analz (knows Spy evs)";
paulson@4598
   304
by (blast_tac (claset() addSDs [B_trusts_YM4, Spy_not_see_encrypted_key]) 1);
paulson@4598
   305
qed "B_gets_good_key";
paulson@4598
   306
paulson@4598
   307
paulson@3432
   308
paulson@3432
   309
(*** Authenticating B to A ***)
paulson@3432
   310
paulson@3432
   311
(*The encryption in message YM2 tells us it cannot be faked.*)
paulson@6335
   312
Goal "[| Crypt (shrK B) {|Agent A, Nonce NA|} : parts (knows Spy evs);  \
paulson@5114
   313
\        B ~: bad;  evs : yahalom                                   \
paulson@5114
   314
\     |] ==> EX NB. Says B Server {|Agent B, Nonce NB,              \
paulson@5114
   315
\                            Crypt (shrK B) {|Agent A, Nonce NA|}|} \
paulson@5114
   316
\                     : set evs";
paulson@5066
   317
by (etac rev_mp 1);
paulson@5066
   318
by (etac rev_mp 1);
paulson@3519
   319
by (parts_induct_tac 1);
paulson@5066
   320
by (ALLGOALS Blast_tac);
paulson@5066
   321
qed "B_Said_YM2";
paulson@3432
   322
paulson@4598
   323
paulson@3432
   324
(*If the server sends YM3 then B sent YM2, perhaps with a different NB*)
paulson@5114
   325
Goal "[| Says Server A                                              \
paulson@5114
   326
\            {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
paulson@5114
   327
\          : set evs;                                               \
paulson@5114
   328
\        B ~: bad;  evs : yahalom                                   \
paulson@5114
   329
\     |] ==> EX nb'. Says B Server {|Agent B, nb',                  \
paulson@5114
   330
\                            Crypt (shrK B) {|Agent A, Nonce NA|}|} \
paulson@5114
   331
\                      : set evs";
paulson@5066
   332
by (etac rev_mp 1);
paulson@5066
   333
by (etac rev_mp 1);
paulson@3432
   334
by (etac yahalom.induct 1);
paulson@3432
   335
by (ALLGOALS Asm_simp_tac);
paulson@3432
   336
(*YM3*)
paulson@5066
   337
by (blast_tac (claset() addSDs [B_Said_YM2]) 3);
paulson@3432
   338
(*Fake, YM2*)
paulson@3432
   339
by (ALLGOALS Blast_tac);
paulson@5066
   340
val lemma = result();
paulson@3432
   341
paulson@3432
   342
(*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
paulson@6335
   343
Goal "[| Gets A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|}   \
paulson@5114
   344
\          : set evs;                                                    \
paulson@6335
   345
\        A ~: bad;  B ~: bad;  evs : yahalom |]                          \
paulson@5114
   346
\==> EX nb'. Says B Server                                               \
paulson@5114
   347
\                 {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|} \
paulson@5114
   348
\              : set evs";
paulson@5066
   349
by (blast_tac (claset() addSDs [A_trusts_YM3, lemma]) 1);
paulson@3432
   350
qed "YM3_auth_B_to_A";
paulson@3432
   351
paulson@3432
   352
paulson@3450
   353
(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
paulson@3450
   354
paulson@3450
   355
(*Assuming the session key is secure, if both certificates are present then
paulson@3432
   356
  A has said NB.  We can't be sure about the rest of A's message, but only
paulson@6335
   357
  NB matters for freshness.  Note that  Key K ~: analz (knows Spy evs)  must be
paulson@5066
   358
  the FIRST antecedent of the induction formula.*)  
paulson@5114
   359
Goal "evs : yahalom                                     \
paulson@6335
   360
\     ==> Key K ~: analz (knows Spy evs) -->                \
paulson@6335
   361
\         Crypt K (Nonce NB) : parts (knows Spy evs) -->    \
paulson@5114
   362
\         Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}      \
paulson@6335
   363
\           : parts (knows Spy evs) -->                     \
paulson@5114
   364
\         B ~: bad -->                                  \
paulson@5114
   365
\         (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
paulson@3519
   366
by (parts_induct_tac 1);
paulson@3432
   367
(*Fake*)
paulson@5066
   368
by (Blast_tac 1);
paulson@3432
   369
(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
paulson@5932
   370
by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); 
paulson@3450
   371
(*YM4: was Crypt K (Nonce NB) the very last message?  If not, use ind. hyp.*)
wenzelm@4091
   372
by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);
paulson@5932
   373
(*yes: delete a useless induction hypothesis; apply unicity of session keys*)
paulson@5932
   374
by (thin_tac "?P-->?Q" 1);
wenzelm@7499
   375
by (ftac Gets_imp_Says 1 THEN assume_tac 1);
paulson@3683
   376
by (not_bad_tac "Aa" 1);
paulson@5066
   377
by (blast_tac (claset() addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
paulson@5066
   378
			addDs  [unique_session_keys]) 1);
paulson@5066
   379
qed_spec_mp "Auth_A_to_B_lemma";
paulson@5066
   380
paulson@3432
   381
paulson@3432
   382
(*If B receives YM4 then A has used nonce NB (and therefore is alive).
paulson@3450
   383
  Moreover, A associates K with NB (thus is talking about the same run).
paulson@3432
   384
  Other premises guarantee secrecy of K.*)
paulson@6335
   385
Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \
paulson@5114
   386
\                    Crypt K (Nonce NB)|} : set evs;                 \
paulson@5114
   387
\        (ALL NA. Notes Spy {|Nonce NA, Nonce NB, Key K|} ~: set evs); \
paulson@5114
   388
\        A ~: bad;  B ~: bad;  evs : yahalom |]                    \
paulson@5114
   389
\     ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
paulson@6335
   390
by (subgoal_tac "Key K ~: analz (knows Spy evs)" 1);
paulson@5066
   391
by (blast_tac (claset() addIs [Auth_A_to_B_lemma]) 1);
paulson@5066
   392
by (blast_tac (claset() addDs  [Spy_not_see_encrypted_key,
paulson@5066
   393
				B_trusts_YM4_shrK]) 1);
paulson@3432
   394
qed_spec_mp "YM4_imp_A_Said_YM3";