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