src/HOL/Auth/Yahalom.ML
author paulson
Wed Nov 18 16:24:33 1998 +0100 (1998-11-18)
changeset 5932 737559a43e71
parent 5535 678999604ee9
child 6335 7e4bffaa2a3e
permissions -rw-r--r--
tidied
paulson@1995
     1
(*  Title:      HOL/Auth/Yahalom
paulson@1985
     2
    ID:         $Id$
paulson@1985
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@1985
     4
    Copyright   1996  University of Cambridge
paulson@1985
     5
paulson@3432
     6
Inductive relation "yahalom" for the Yahalom protocol.
paulson@1985
     7
paulson@1985
     8
From page 257 of
paulson@1985
     9
  Burrows, Abadi and Needham.  A Logic of Authentication.
paulson@1985
    10
  Proc. Royal Soc. 426 (1989)
paulson@1985
    11
*)
paulson@1985
    12
paulson@2516
    13
Pretty.setdepth 25;
paulson@1985
    14
paulson@1995
    15
paulson@2322
    16
(*A "possibility property": there are traces that reach the end*)
paulson@5434
    17
Goal "A ~= Server \
paulson@5114
    18
\     ==> EX X NB K. EX evs: yahalom.          \
paulson@5114
    19
\            Says A B {|X, Crypt K (Nonce NB)|} : set evs";
paulson@1995
    20
by (REPEAT (resolve_tac [exI,bexI] 1));
paulson@2516
    21
by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS 
paulson@2516
    22
          yahalom.YM4) 2);
paulson@2516
    23
by possibility_tac;
paulson@2013
    24
result();
paulson@1995
    25
paulson@1995
    26
paulson@1985
    27
(**** Inductive proofs about yahalom ****)
paulson@1985
    28
paulson@1985
    29
paulson@1985
    30
(** For reasoning about the encrypted portion of messages **)
paulson@1985
    31
paulson@1995
    32
(*Lets us treat YM4 using a similar argument as for the Fake case.*)
paulson@5114
    33
Goal "Says S A {|Crypt (shrK A) Y, X|} : set evs ==> \
paulson@5114
    34
\             X : analz (spies evs)";
wenzelm@4091
    35
by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
paulson@3683
    36
qed "YM4_analz_spies";
paulson@1985
    37
paulson@3683
    38
bind_thm ("YM4_parts_spies",
paulson@3683
    39
          YM4_analz_spies RS (impOfSubs analz_subset_parts));
paulson@2110
    40
paulson@2133
    41
(*Relates to both YM4 and Oops*)
paulson@5114
    42
Goal "Says S A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} : set evs ==> \
paulson@5114
    43
\             K : parts (spies evs)";
wenzelm@4091
    44
by (blast_tac (claset() addSEs partsEs
paulson@4238
    45
                        addSDs [Says_imp_spies RS parts.Inj]) 1);
paulson@3683
    46
qed "YM4_Key_parts_spies";
paulson@2110
    47
paulson@3683
    48
(*For proving the easier theorems about X ~: parts (spies evs).*)
paulson@3683
    49
fun parts_spies_tac i = 
paulson@3683
    50
    forward_tac [YM4_Key_parts_spies] (i+6) THEN
paulson@3683
    51
    forward_tac [YM4_parts_spies] (i+5)     THEN
paulson@3519
    52
    prove_simple_subgoals_tac  i;
paulson@1985
    53
paulson@3519
    54
(*Induction for regularity theorems.  If induction formula has the form
paulson@3683
    55
   X ~: analz (spies evs) --> ... then it shortens the proof by discarding
paulson@3683
    56
   needless information about analz (insert X (spies evs))  *)
paulson@3519
    57
fun parts_induct_tac i = 
paulson@3519
    58
    etac yahalom.induct i
paulson@3519
    59
    THEN 
paulson@3519
    60
    REPEAT (FIRSTGOAL analz_mono_contra_tac)
paulson@3683
    61
    THEN  parts_spies_tac i;
paulson@1985
    62
paulson@1985
    63
paulson@3683
    64
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
paulson@2013
    65
    sends messages containing X! **)
paulson@1985
    66
paulson@3683
    67
(*Spy never sees another agent's shared key! (unless it's bad at start)*)
paulson@5114
    68
Goal "evs : yahalom ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
paulson@3519
    69
by (parts_induct_tac 1);
paulson@3121
    70
by (Fake_parts_insert_tac 1);
paulson@3961
    71
by (ALLGOALS Blast_tac);
paulson@2133
    72
qed "Spy_see_shrK";
paulson@2133
    73
Addsimps [Spy_see_shrK];
paulson@1985
    74
paulson@5114
    75
Goal "evs : yahalom ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
wenzelm@4091
    76
by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
paulson@2133
    77
qed "Spy_analz_shrK";
paulson@2133
    78
Addsimps [Spy_analz_shrK];
paulson@1985
    79
paulson@4471
    80
AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
paulson@4471
    81
	Spy_analz_shrK RSN (2, rev_iffD1)];
paulson@1985
    82
paulson@1985
    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
(*Fake*)
paulson@4509
    89
by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
paulson@3961
    90
(*YM2-4: Because Key K is not fresh, etc.*)
wenzelm@4091
    91
by (REPEAT (blast_tac (claset() addSEs spies_partsEs) 1));
paulson@2160
    92
qed_spec_mp "new_keys_not_used";
paulson@1985
    93
paulson@1985
    94
bind_thm ("new_keys_not_analzd",
paulson@2032
    95
          [analz_subset_parts RS keysFor_mono,
paulson@2032
    96
           new_keys_not_used] MRS contra_subsetD);
paulson@1985
    97
paulson@1985
    98
Addsimps [new_keys_not_used, new_keys_not_analzd];
paulson@1985
    99
paulson@1985
   100
paulson@2133
   101
(*Describes the form of K when the Server sends this message.  Useful for
paulson@2133
   102
  Oops as well as main secrecy property.*)
paulson@5114
   103
Goal "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \
paulson@5434
   104
\          : set evs;   evs : yahalom |]                                \
paulson@5114
   105
\     ==> K ~: range shrK";
paulson@2133
   106
by (etac rev_mp 1);
paulson@2133
   107
by (etac yahalom.induct 1);
paulson@3121
   108
by (ALLGOALS Asm_simp_tac);
paulson@3121
   109
by (Blast_tac 1);
paulson@5073
   110
qed "Says_Server_not_range";
paulson@5073
   111
paulson@5073
   112
Addsimps [Says_Server_not_range];
paulson@2110
   113
paulson@2110
   114
paulson@3519
   115
(*For proofs involving analz.*)
paulson@5073
   116
val analz_spies_tac = forward_tac [YM4_analz_spies] 6;
paulson@1985
   117
paulson@1985
   118
(****
paulson@1985
   119
 The following is to prove theorems of the form
paulson@1985
   120
paulson@3683
   121
  Key K : analz (insert (Key KAB) (spies evs)) ==>
paulson@3683
   122
  Key K : analz (spies evs)
paulson@1985
   123
paulson@1985
   124
 A more general formula must be proved inductively.
paulson@1985
   125
****)
paulson@1985
   126
paulson@1985
   127
(** Session keys are not used to encrypt other session keys **)
paulson@1985
   128
paulson@5114
   129
Goal "evs : yahalom ==>                              \
paulson@5492
   130
\  ALL K KK. KK <= - (range shrK) -->                \
paulson@5114
   131
\         (Key K : analz (Key``KK Un (spies evs))) = \
paulson@5114
   132
\         (K : KK | Key K : analz (spies evs))";
paulson@2032
   133
by (etac yahalom.induct 1);
paulson@3683
   134
by analz_spies_tac;
paulson@2516
   135
by (REPEAT_FIRST (resolve_tac [allI, impI]));
paulson@3679
   136
by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
paulson@5073
   137
by (ALLGOALS (asm_simp_tac
paulson@5073
   138
	      (analz_image_freshK_ss addsimps [Says_Server_not_range])));
paulson@3450
   139
(*Fake*) 
paulson@4422
   140
by (spy_analz_tac 1);
paulson@2516
   141
qed_spec_mp "analz_image_freshK";
paulson@1985
   142
paulson@5114
   143
Goal "[| evs : yahalom;  KAB ~: range shrK |]              \
paulson@5114
   144
\      ==> Key K : analz (insert (Key KAB) (spies evs)) =  \
paulson@5114
   145
\          (K = KAB | Key K : analz (spies evs))";
paulson@2516
   146
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
paulson@2516
   147
qed "analz_insert_freshK";
paulson@1985
   148
paulson@1985
   149
paulson@2110
   150
(*** The Key K uniquely identifies the Server's  message. **)
paulson@2110
   151
paulson@5114
   152
Goal "evs : yahalom ==>                                     \
paulson@5114
   153
\   EX A' B' na' nb' X'. ALL A B na nb X.                   \
paulson@5114
   154
\       Says Server A                                       \
paulson@5114
   155
\        {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}   \
paulson@5114
   156
\       : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
paulson@2110
   157
by (etac yahalom.induct 1);
wenzelm@4091
   158
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
paulson@3708
   159
by (ALLGOALS Clarify_tac);
paulson@2133
   160
by (ex_strip_tac 2);
paulson@3121
   161
by (Blast_tac 2);
paulson@2110
   162
(*Remaining case: YM3*)
paulson@2110
   163
by (expand_case_tac "K = ?y" 1);
paulson@2110
   164
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
paulson@2516
   165
(*...we assume X is a recent message and handle this case by contradiction*)
wenzelm@4091
   166
by (blast_tac (claset() addSEs spies_partsEs
paulson@4238
   167
                        delrules [conjI]    (*no split-up to 4 subgoals*)) 1);
paulson@2110
   168
val lemma = result();
paulson@2110
   169
paulson@5114
   170
Goal "[| Says Server A                                                 \
paulson@5114
   171
\         {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} : set evs; \
paulson@5114
   172
\       Says Server A'                                                \
paulson@5114
   173
\         {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} : set evs; \
paulson@5114
   174
\       evs : yahalom |]                                    \
paulson@5114
   175
\    ==> A=A' & B=B' & na=na' & nb=nb'";
paulson@2451
   176
by (prove_unique_tac lemma 1);
paulson@2110
   177
qed "unique_session_keys";
paulson@2110
   178
paulson@2110
   179
paulson@2110
   180
(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
paulson@2013
   181
paulson@5114
   182
Goal "[| A ~: bad;  B ~: bad;  evs : yahalom |]                \
paulson@5114
   183
\     ==> Says Server A                                        \
paulson@5114
   184
\           {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
paulson@5114
   185
\             Crypt (shrK B) {|Agent A, Key K|}|}              \
paulson@5114
   186
\          : set evs -->                                       \
paulson@5114
   187
\         Notes Spy {|na, nb, Key K|} ~: set evs -->           \
paulson@5114
   188
\         Key K ~: analz (spies evs)";
paulson@2032
   189
by (etac yahalom.induct 1);
paulson@3683
   190
by analz_spies_tac;
paulson@2013
   191
by (ALLGOALS
paulson@2013
   192
    (asm_simp_tac 
paulson@5535
   193
     (simpset() addsimps split_ifs @ pushes @
paulson@5535
   194
                         [analz_insert_eq, analz_insert_freshK])));
paulson@3450
   195
(*Oops*)
wenzelm@4091
   196
by (blast_tac (claset() addDs [unique_session_keys]) 3);
paulson@2013
   197
(*YM3*)
wenzelm@4091
   198
by (blast_tac (claset() delrules [impCE]
paulson@4238
   199
                        addSEs spies_partsEs
paulson@4238
   200
                        addIs [impOfSubs analz_subset_parts]) 2);
paulson@3450
   201
(*Fake*) 
paulson@3450
   202
by (spy_analz_tac 1);
paulson@2110
   203
val lemma = result() RS mp RS mp RSN(2,rev_notE);
paulson@2013
   204
paulson@2013
   205
paulson@3432
   206
(*Final version*)
paulson@5114
   207
Goal "[| Says Server A                                         \
paulson@5114
   208
\           {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
paulson@5114
   209
\             Crypt (shrK B) {|Agent A, Key K|}|}              \
paulson@5114
   210
\          : set evs;                                          \
paulson@5114
   211
\        Notes Spy {|na, nb, Key K|} ~: set evs;               \
paulson@5114
   212
\        A ~: bad;  B ~: bad;  evs : yahalom |]                \
paulson@5114
   213
\     ==> Key K ~: analz (spies evs)";
wenzelm@4091
   214
by (blast_tac (claset() addSEs [lemma]) 1);
paulson@2032
   215
qed "Spy_not_see_encrypted_key";
paulson@2001
   216
paulson@2001
   217
paulson@3444
   218
(** Security Guarantee for A upon receiving YM3 **)
paulson@3444
   219
paulson@3444
   220
(*If the encrypted message appears then it originated with the Server*)
paulson@5114
   221
Goal "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} : parts (spies evs); \
paulson@5114
   222
\        A ~: bad;  evs : yahalom |]                          \
paulson@5114
   223
\      ==> Says Server A                                            \
paulson@5114
   224
\           {|Crypt (shrK A) {|Agent B, Key K, na, nb|},            \
paulson@5114
   225
\             Crypt (shrK B) {|Agent A, Key K|}|}                   \
paulson@5114
   226
\          : set evs";
paulson@3444
   227
by (etac rev_mp 1);
paulson@3519
   228
by (parts_induct_tac 1);
paulson@3444
   229
by (Fake_parts_insert_tac 1);
paulson@3444
   230
qed "A_trusts_YM3";
paulson@3444
   231
paulson@4598
   232
(*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
paulson@5114
   233
Goal "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} : parts (spies evs); \
paulson@5114
   234
\        Notes Spy {|na, nb, Key K|} ~: set evs;               \
paulson@5114
   235
\        A ~: bad;  B ~: bad;  evs : yahalom |]                \
paulson@5114
   236
\     ==> Key K ~: analz (spies evs)";
paulson@4598
   237
by (blast_tac (claset() addSDs [A_trusts_YM3, Spy_not_see_encrypted_key]) 1);
paulson@4598
   238
qed "A_gets_good_key";
paulson@3444
   239
paulson@3444
   240
(** Security Guarantees for B upon receiving YM4 **)
paulson@2013
   241
paulson@2110
   242
(*B knows, by the first part of A's message, that the Server distributed 
paulson@2110
   243
  the key for A and B.  But this part says nothing about nonces.*)
paulson@5114
   244
Goal "[| Crypt (shrK B) {|Agent A, Key K|} : parts (spies evs);      \
paulson@5114
   245
\        B ~: bad;  evs : yahalom |]                                 \
paulson@5114
   246
\     ==> EX NA NB. Says Server A                                    \
paulson@5114
   247
\                     {|Crypt (shrK A) {|Agent B, Key K,             \
paulson@5114
   248
\                                        Nonce NA, Nonce NB|},       \
paulson@5114
   249
\                       Crypt (shrK B) {|Agent A, Key K|}|}          \
paulson@5114
   250
\                    : set evs";
paulson@2032
   251
by (etac rev_mp 1);
paulson@3519
   252
by (parts_induct_tac 1);
paulson@3121
   253
by (Fake_parts_insert_tac 1);
paulson@2110
   254
(*YM3*)
paulson@3121
   255
by (Blast_tac 1);
paulson@2110
   256
qed "B_trusts_YM4_shrK";
paulson@2110
   257
paulson@3444
   258
(*B knows, by the second part of A's message, that the Server distributed 
paulson@3444
   259
  the key quoting nonce NB.  This part says nothing about agent names. 
paulson@5065
   260
  Secrecy of NB is crucial.  Note that  Nonce NB  ~: analz (spies evs)  must
paulson@5065
   261
  be the FIRST antecedent of the induction formula.*)
paulson@5114
   262
Goal "evs : yahalom                                          \
paulson@5114
   263
\     ==> Nonce NB ~: analz (spies evs) -->                  \
paulson@5114
   264
\         Crypt K (Nonce NB) : parts (spies evs) -->         \
paulson@5114
   265
\         (EX A B NA. Says Server A                          \
paulson@5114
   266
\                     {|Crypt (shrK A) {|Agent B, Key K,     \
paulson@5114
   267
\                               Nonce NA, Nonce NB|},        \
paulson@5114
   268
\                       Crypt (shrK B) {|Agent A, Key K|}|}  \
paulson@5114
   269
\                    : set evs)";
paulson@3519
   270
by (parts_induct_tac 1);
paulson@3708
   271
by (ALLGOALS Clarify_tac);
paulson@3444
   272
(*YM3 & Fake*)
paulson@3444
   273
by (Blast_tac 2);
paulson@3444
   274
by (Fake_parts_insert_tac 1);
paulson@3444
   275
(*YM4*)
paulson@3444
   276
(*A is uncompromised because NB is secure*)
paulson@3683
   277
by (not_bad_tac "A" 1);
paulson@3444
   278
(*A's certificate guarantees the existence of the Server message*)
wenzelm@4091
   279
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS
paulson@4238
   280
			       A_trusts_YM3]) 1);
paulson@3464
   281
bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp));
paulson@2133
   282
paulson@3444
   283
paulson@3444
   284
(**** Towards proving secrecy of Nonce NB ****)
paulson@3444
   285
paulson@3444
   286
(** Lemmas about the predicate KeyWithNonce **)
paulson@3444
   287
paulson@5076
   288
Goalw [KeyWithNonce_def]
paulson@5114
   289
 "Says Server A                                              \
paulson@5114
   290
\         {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \
paulson@5114
   291
\       : set evs ==> KeyWithNonce K NB evs";
paulson@3444
   292
by (Blast_tac 1);
paulson@3444
   293
qed "KeyWithNonceI";
paulson@3444
   294
paulson@5076
   295
Goalw [KeyWithNonce_def]
paulson@3444
   296
   "KeyWithNonce K NB (Says S A X # evs) =                                    \
paulson@5114
   297
\ (Server = S &                                                            \
paulson@5114
   298
\  (EX B n X'. X = {|Crypt (shrK A) {|Agent B, Key K, n, Nonce NB|}, X'|}) \
paulson@5114
   299
\ | KeyWithNonce K NB evs)";
paulson@3444
   300
by (Simp_tac 1);
paulson@3444
   301
by (Blast_tac 1);
paulson@3444
   302
qed "KeyWithNonce_Says";
paulson@3444
   303
Addsimps [KeyWithNonce_Says];
paulson@3444
   304
paulson@5076
   305
Goalw [KeyWithNonce_def]
paulson@4537
   306
   "KeyWithNonce K NB (Notes A X # evs) = KeyWithNonce K NB evs";
paulson@4537
   307
by (Simp_tac 1);
paulson@4537
   308
qed "KeyWithNonce_Notes";
paulson@4537
   309
Addsimps [KeyWithNonce_Notes];
paulson@4537
   310
paulson@3464
   311
(*A fresh key cannot be associated with any nonce 
paulson@3464
   312
  (with respect to a given trace). *)
paulson@5076
   313
Goalw [KeyWithNonce_def]
paulson@5114
   314
 "Key K ~: used evs ==> ~ KeyWithNonce K NB evs";
wenzelm@4091
   315
by (blast_tac (claset() addSEs spies_partsEs) 1);
paulson@3444
   316
qed "fresh_not_KeyWithNonce";
paulson@3444
   317
paulson@3444
   318
(*The Server message associates K with NB' and therefore not with any 
paulson@3444
   319
  other nonce NB.*)
paulson@5076
   320
Goalw [KeyWithNonce_def]
paulson@5114
   321
 "[| Says Server A                                                \
paulson@5114
   322
\             {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|} \
paulson@5114
   323
\          : set evs;                                                 \
paulson@5114
   324
\        NB ~= NB';  evs : yahalom |]                                 \
paulson@5114
   325
\     ==> ~ KeyWithNonce K NB evs";
wenzelm@4091
   326
by (blast_tac (claset() addDs [unique_session_keys]) 1);
paulson@3444
   327
qed "Says_Server_KeyWithNonce";
paulson@3444
   328
paulson@3444
   329
paulson@3444
   330
(*The only nonces that can be found with the help of session keys are
paulson@3444
   331
  those distributed as nonce NB by the Server.  The form of the theorem
paulson@3444
   332
  recalls analz_image_freshK, but it is much more complicated.*)
paulson@3444
   333
paulson@3444
   334
paulson@3444
   335
(*As with analz_image_freshK, we take some pains to express the property
paulson@3444
   336
  as a logical equivalence so that the simplifier can apply it.*)
paulson@5114
   337
Goal "P --> (X : analz (G Un H)) --> (X : analz H)  ==> \
paulson@5114
   338
\     P --> (X : analz (G Un H)) = (X : analz H)";
wenzelm@4091
   339
by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
paulson@3961
   340
val Nonce_secrecy_lemma = result();
paulson@2133
   341
paulson@5114
   342
Goal "evs : yahalom ==>                                      \
paulson@5492
   343
\     (ALL KK. KK <= - (range shrK) -->                      \
paulson@5114
   344
\          (ALL K: KK. ~ KeyWithNonce K NB evs)   -->        \
paulson@5114
   345
\          (Nonce NB : analz (Key``KK Un (spies evs))) =     \
paulson@5114
   346
\          (Nonce NB : analz (spies evs)))";
paulson@3444
   347
by (etac yahalom.induct 1);
paulson@3683
   348
by analz_spies_tac;
paulson@3444
   349
by (REPEAT_FIRST (resolve_tac [impI RS allI]));
paulson@3961
   350
by (REPEAT_FIRST (rtac Nonce_secrecy_lemma));
paulson@3444
   351
(*For Oops, simplification proves NBa~=NB.  By Says_Server_KeyWithNonce,
paulson@5114
   352
  we get (~ KeyWithNonce K NB evs); then simplification can apply the
paulson@3444
   353
  induction hypothesis with KK = {K}.*)
paulson@5073
   354
by (ALLGOALS  (*4 seconds*)
paulson@3444
   355
    (asm_simp_tac 
paulson@3961
   356
     (analz_image_freshK_ss 
nipkow@4831
   357
       addsimps split_ifs
paulson@3961
   358
       addsimps [all_conj_distrib, analz_image_freshK,
paulson@4537
   359
		 KeyWithNonce_Says, KeyWithNonce_Notes,
paulson@5073
   360
		 fresh_not_KeyWithNonce, Says_Server_not_range,
paulson@3961
   361
		 imp_disj_not1,		     (*Moves NBa~=NB to the front*)
paulson@3961
   362
		 Says_Server_KeyWithNonce])));
paulson@3444
   363
(*Fake*) 
paulson@3444
   364
by (spy_analz_tac 1);
paulson@4422
   365
(*YM4*)  (** LEVEL 6 **)
paulson@3683
   366
by (not_bad_tac "A" 1);
paulson@3683
   367
by (dtac (Says_imp_spies RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
paulson@3444
   368
    THEN REPEAT (assume_tac 1));
wenzelm@4091
   369
by (blast_tac (claset() addIs [KeyWithNonceI]) 1);
paulson@3444
   370
qed_spec_mp "Nonce_secrecy";
paulson@3444
   371
paulson@3444
   372
paulson@3444
   373
(*Version required below: if NB can be decrypted using a session key then it
paulson@3444
   374
  was distributed with that key.  The more general form above is required
paulson@3444
   375
  for the induction to carry through.*)
paulson@5114
   376
Goal "[| Says Server A                                               \
paulson@5114
   377
\         {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|}  \
paulson@5114
   378
\        : set evs;                                                  \
paulson@5114
   379
\        NB ~= NB';  KAB ~: range shrK;  evs : yahalom |]            \
paulson@5114
   380
\     ==> (Nonce NB : analz (insert (Key KAB) (spies evs))) =        \
paulson@5114
   381
\         (Nonce NB : analz (spies evs))";
paulson@3444
   382
by (asm_simp_tac (analz_image_freshK_ss addsimps 
paulson@3444
   383
		  [Nonce_secrecy, Says_Server_KeyWithNonce]) 1);
paulson@3444
   384
qed "single_Nonce_secrecy";
paulson@3444
   385
paulson@3444
   386
paulson@3444
   387
(*** The Nonce NB uniquely identifies B's message. ***)
paulson@3444
   388
paulson@5114
   389
Goal "evs : yahalom ==>                                         \
paulson@5114
   390
\EX NA' A' B'. ALL NA A B.                                      \
paulson@5114
   391
\   Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts(spies evs) \
paulson@5114
   392
\   --> B ~: bad --> NA = NA' & A = A' & B = B'";
paulson@3519
   393
by (parts_induct_tac 1);
paulson@3121
   394
(*Fake*)
paulson@3121
   395
by (REPEAT (etac (exI RSN (2,exE)) 1)   (*stripping EXs makes proof faster*)
paulson@3121
   396
    THEN Fake_parts_insert_tac 1);
wenzelm@4091
   397
by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1); 
paulson@2133
   398
(*YM2: creation of new Nonce.  Move assertion into global context*)
paulson@3501
   399
by (expand_case_tac "nb = ?y" 1);
paulson@2516
   400
by (REPEAT (resolve_tac [exI, conjI, impI, refl] 1));
wenzelm@4091
   401
by (blast_tac (claset() addSEs spies_partsEs) 1);
paulson@2133
   402
val lemma = result();
paulson@2133
   403
paulson@5114
   404
Goal "[| Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts (spies evs);    \
paulson@5114
   405
\       Crypt (shrK B') {|Agent A', Nonce NA', nb|} : parts (spies evs); \
paulson@5114
   406
\       evs : yahalom;  B ~: bad;  B' ~: bad |]  \
paulson@5114
   407
\     ==> NA' = NA & A' = A & B' = B";
paulson@2451
   408
by (prove_unique_tac lemma 1);
paulson@2133
   409
qed "unique_NB";
paulson@2133
   410
paulson@2133
   411
paulson@3444
   412
(*Variant useful for proving secrecy of NB: the Says... form allows 
paulson@3683
   413
  not_bad_tac to remove the assumption B' ~: bad.*)
paulson@5114
   414
Goal "[| Says C D   {|X,  Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}    \
paulson@5114
   415
\         : set evs;          B ~: bad;                                \
paulson@5114
   416
\       Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|} \
paulson@5114
   417
\         : set evs;                                                   \
paulson@5114
   418
\       nb ~: analz (spies evs);  evs : yahalom |]                     \
paulson@5114
   419
\     ==> NA' = NA & A' = A & B' = B";
paulson@3683
   420
by (not_bad_tac "B'" 1);
wenzelm@4091
   421
by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj]
paulson@4238
   422
                        addSEs [MPair_parts]
paulson@4238
   423
                        addDs  [unique_NB]) 1);
paulson@2133
   424
qed "Says_unique_NB";
paulson@2133
   425
paulson@3444
   426
paulson@3444
   427
(** A nonce value is never used both as NA and as NB **)
paulson@3121
   428
paulson@5114
   429
Goal "evs : yahalom                     \
paulson@5073
   430
\ ==> Nonce NB ~: analz (spies evs) -->    \
paulson@5114
   431
\  Crypt (shrK B') {|Agent A', Nonce NB, nb'|} : parts(spies evs) --> \
paulson@5114
   432
\  Crypt (shrK B)  {|Agent A, na, Nonce NB|} ~: parts(spies evs)";
paulson@3519
   433
by (parts_induct_tac 1);
paulson@3121
   434
by (Fake_parts_insert_tac 1);
wenzelm@4091
   435
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]
paulson@4238
   436
                        addSIs [parts_insertI]
paulson@4238
   437
                        addSEs partsEs) 1);
paulson@3464
   438
bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2,rev_mp) RSN (2,rev_notE));
paulson@2133
   439
paulson@5065
   440
(*more readable version cited in Yahalom paper*)
paulson@5065
   441
standard (result() RS mp RSN (2,rev_mp));
paulson@5065
   442
paulson@3464
   443
(*The Server sends YM3 only in response to YM2.*)
paulson@5114
   444
Goal "[| Says Server A                                                \
paulson@5114
   445
\         {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set evs;     \
paulson@5114
   446
\        evs : yahalom |]                                             \
paulson@5114
   447
\     ==> EX B'. Says B' Server                                       \
paulson@5114
   448
\                   {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} \
paulson@5114
   449
\                : set evs";
paulson@2133
   450
by (etac rev_mp 1);
paulson@2133
   451
by (etac yahalom.induct 1);
paulson@5932
   452
by Auto_tac;
paulson@2133
   453
qed "Says_Server_imp_YM2";
paulson@2133
   454
paulson@2133
   455
paulson@3519
   456
(*A vital theorem for B, that nonce NB remains secure from the Spy.*)
paulson@5114
   457
Goal "[| A ~: bad;  B ~: bad;  evs : yahalom |]  \
paulson@2133
   458
\ ==> Says B Server                                                    \
paulson@5114
   459
\       {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
paulson@5114
   460
\  : set evs -->                                                    \
paulson@5114
   461
\  (ALL k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs) -->      \
paulson@5114
   462
\  Nonce NB ~: analz (spies evs)";
paulson@2133
   463
by (etac yahalom.induct 1);
paulson@3683
   464
by analz_spies_tac;
paulson@2133
   465
by (ALLGOALS
paulson@2133
   466
    (asm_simp_tac 
paulson@5535
   467
     (simpset() addsimps split_ifs @ pushes @
paulson@5535
   468
	                 [analz_insert_eq, analz_insert_freshK])));
paulson@3450
   469
(*Prove YM3 by showing that no NB can also be an NA*)
wenzelm@4091
   470
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj]
paulson@4238
   471
	                addSEs [MPair_parts]
paulson@5932
   472
		        addDs  [no_nonce_YM1_YM2, Says_unique_NB]) 4);
paulson@3444
   473
(*YM2: similar freshness reasoning*) 
wenzelm@4091
   474
by (blast_tac (claset() addSEs partsEs
paulson@4238
   475
		        addDs  [Says_imp_spies RS analz.Inj,
paulson@4238
   476
				impOfSubs analz_subset_parts]) 3);
paulson@3450
   477
(*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*)
wenzelm@4091
   478
by (blast_tac (claset() addSIs [parts_insertI]
paulson@4238
   479
                        addSEs spies_partsEs) 2);
paulson@2377
   480
(*Fake*)
paulson@2377
   481
by (spy_analz_tac 1);
paulson@3444
   482
(** LEVEL 7: YM4 and Oops remain **)
paulson@5932
   483
by (ALLGOALS (Clarify_tac THEN' 
paulson@5932
   484
	      full_simp_tac (simpset() addsimps [all_conj_distrib])));
paulson@3444
   485
(*YM4: key K is visible to Spy, contradicting session key secrecy theorem*) 
paulson@3683
   486
by (not_bad_tac "Aa" 1);
paulson@3683
   487
by (dtac (Says_imp_spies RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
paulson@5073
   488
by (forward_tac [Says_Server_imp_YM2] 3);
paulson@5932
   489
by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
paulson@5932
   490
(*  use Says_unique_NB to identify message components: Aa=A, Ba=B*)
paulson@5932
   491
by (blast_tac (claset() addDs [Says_unique_NB, Spy_not_see_encrypted_key]) 1);
paulson@5073
   492
(** LEVEL 13 **)
paulson@3444
   493
(*Oops case: if the nonce is betrayed now, show that the Oops event is 
paulson@3444
   494
  covered by the quantified Oops assumption.*)
paulson@2133
   495
by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
paulson@2133
   496
by (expand_case_tac "NB = NBa" 1);
paulson@3444
   497
(*If NB=NBa then all other components of the Oops message agree*)
paulson@5932
   498
by (blast_tac (claset() addDs [Says_unique_NB]) 1);
paulson@3444
   499
(*case NB ~= NBa*)
wenzelm@4091
   500
by (asm_simp_tac (simpset() addsimps [single_Nonce_secrecy]) 1);
paulson@4471
   501
by (Clarify_tac 1);
wenzelm@4091
   502
by (blast_tac (claset() addSEs [MPair_parts]
paulson@4238
   503
		        addDs  [Says_imp_spies RS parts.Inj, 
paulson@4238
   504
			        no_nonce_YM1_YM2 (*to prove NB~=NAa*) ]) 1);
paulson@3444
   505
bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp));
paulson@2133
   506
paulson@2001
   507
paulson@3464
   508
(*B's session key guarantee from YM4.  The two certificates contribute to a
paulson@4537
   509
  single conclusion about the Server's message.  Note that the "Notes Spy"
paulson@3464
   510
  assumption must quantify over ALL POSSIBLE keys instead of our particular K.
paulson@3464
   511
  If this run is broken and the spy substitutes a certificate containing an
paulson@3464
   512
  old key, B has no means of telling.*)
paulson@5114
   513
Goal "[| Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
paulson@5114
   514
\                    Crypt K (Nonce NB)|} : set evs;                     \
paulson@5114
   515
\        Says B Server                                                   \
paulson@5114
   516
\          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
paulson@5114
   517
\          : set evs;                                                    \
paulson@5114
   518
\        ALL k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs;          \
paulson@5114
   519
\        A ~: bad;  B ~: bad;  evs : yahalom |]       \
paulson@5114
   520
\      ==> Says Server A                                                 \
paulson@5114
   521
\                  {|Crypt (shrK A) {|Agent B, Key K,                    \
paulson@5114
   522
\                            Nonce NA, Nonce NB|},                       \
paulson@5114
   523
\                    Crypt (shrK B) {|Agent A, Key K|}|}                 \
paulson@5114
   524
\            : set evs";
paulson@2133
   525
by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
paulson@3683
   526
by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1 THEN
paulson@2133
   527
    dtac B_trusts_YM4_shrK 1);
paulson@2170
   528
by (dtac B_trusts_YM4_newK 3);
paulson@2110
   529
by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
paulson@2133
   530
by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1);
paulson@2170
   531
by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1));
wenzelm@4091
   532
by (blast_tac (claset() addDs [Says_unique_NB]) 1);
paulson@2322
   533
qed "B_trusts_YM4";
paulson@3444
   534
paulson@3444
   535
paulson@4598
   536
(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
paulson@5114
   537
Goal "[| Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
paulson@5114
   538
\                    Crypt K (Nonce NB)|} : set evs;                     \
paulson@5114
   539
\        Says B Server                                                   \
paulson@5114
   540
\          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
paulson@5114
   541
\          : set evs;                                                    \
paulson@5114
   542
\        ALL k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs;          \
paulson@5114
   543
\        A ~: bad;  B ~: bad;  evs : yahalom |]                \
paulson@5114
   544
\     ==> Key K ~: analz (spies evs)";
paulson@4598
   545
by (blast_tac (claset() addSDs [B_trusts_YM4, Spy_not_see_encrypted_key]) 1);
paulson@4598
   546
qed "B_gets_good_key";
paulson@4598
   547
paulson@3444
   548
paulson@3444
   549
(*** Authenticating B to A ***)
paulson@3444
   550
paulson@3444
   551
(*The encryption in message YM2 tells us it cannot be faked.*)
paulson@5114
   552
Goal "evs : yahalom                                            \
paulson@3683
   553
\  ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts (spies evs) --> \
paulson@5114
   554
\   B ~: bad -->                                              \
paulson@5114
   555
\   Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}  \
paulson@5114
   556
\      : set evs";
paulson@3519
   557
by (parts_induct_tac 1);
paulson@3444
   558
by (Fake_parts_insert_tac 1);
paulson@3444
   559
bind_thm ("B_Said_YM2", result() RSN (2, rev_mp) RS mp);
paulson@3444
   560
paulson@3444
   561
(*If the server sends YM3 then B sent YM2*)
paulson@5114
   562
Goal "evs : yahalom                                                      \
paulson@3444
   563
\  ==> Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
paulson@5114
   564
\      : set evs -->                                                     \
paulson@5114
   565
\   B ~: bad -->                                                        \
paulson@5114
   566
\   Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}  \
paulson@5114
   567
\              : set evs";
paulson@3444
   568
by (etac yahalom.induct 1);
paulson@3444
   569
by (ALLGOALS Asm_simp_tac);
paulson@3444
   570
(*YM4*)
paulson@3444
   571
by (Blast_tac 2);
paulson@4509
   572
(*YM3 [blast_tac is 50% slower] *)
wenzelm@4091
   573
by (best_tac (claset() addSDs [B_Said_YM2, Says_imp_spies RS parts.Inj]
paulson@4238
   574
		       addSEs [MPair_parts]) 1);
paulson@3444
   575
val lemma = result() RSN (2, rev_mp) RS mp |> standard;
paulson@3444
   576
paulson@3444
   577
(*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
paulson@5114
   578
Goal "[| Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
paulson@5114
   579
\          : set evs;                                                    \
paulson@5114
   580
\        A ~: bad;  B ~: bad;  evs : yahalom |]                        \
paulson@5114
   581
\==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
paulson@5114
   582
\      : set evs";
wenzelm@4091
   583
by (blast_tac (claset() addSDs [A_trusts_YM3, lemma]
paulson@4238
   584
		        addEs spies_partsEs) 1);
paulson@3444
   585
qed "YM3_auth_B_to_A";
paulson@3444
   586
paulson@3444
   587
paulson@3444
   588
(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
paulson@3444
   589
paulson@3444
   590
(*Assuming the session key is secure, if both certificates are present then
paulson@3444
   591
  A has said NB.  We can't be sure about the rest of A's message, but only
paulson@3444
   592
  NB matters for freshness.*)  
paulson@5114
   593
Goal "evs : yahalom                                             \
paulson@5114
   594
\     ==> Key K ~: analz (spies evs) -->                     \
paulson@5114
   595
\         Crypt K (Nonce NB) : parts (spies evs) -->         \
paulson@5114
   596
\         Crypt (shrK B) {|Agent A, Key K|} : parts (spies evs) --> \
paulson@5114
   597
\         B ~: bad -->                                         \
paulson@5114
   598
\         (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
paulson@3519
   599
by (parts_induct_tac 1);
paulson@3444
   600
(*Fake*)
paulson@3444
   601
by (Fake_parts_insert_tac 1);
paulson@3444
   602
(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
paulson@4238
   603
by (fast_tac (claset() addSDs [Crypt_imp_keysFor] addss (simpset())) 1); 
paulson@3444
   604
(*YM4: was Crypt K (Nonce NB) the very last message?  If not, use ind. hyp.*)
wenzelm@4091
   605
by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);
paulson@3444
   606
(*yes: apply unicity of session keys*)
paulson@3683
   607
by (not_bad_tac "Aa" 1);
wenzelm@4091
   608
by (blast_tac (claset() addSEs [MPair_parts]
paulson@4238
   609
                        addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
paulson@4238
   610
		        addDs  [Says_imp_spies RS parts.Inj,
paulson@4238
   611
				unique_session_keys]) 1);
paulson@3444
   612
val lemma = normalize_thm [RSspec, RSmp] (result()) |> standard;
paulson@3444
   613
paulson@3444
   614
(*If B receives YM4 then A has used nonce NB (and therefore is alive).
paulson@3444
   615
  Moreover, A associates K with NB (thus is talking about the same run).
paulson@3444
   616
  Other premises guarantee secrecy of K.*)
paulson@5114
   617
Goal "[| Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
paulson@5114
   618
\                    Crypt K (Nonce NB)|} : set evs;                     \
paulson@5114
   619
\        Says B Server                                                   \
paulson@5114
   620
\          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
paulson@5114
   621
\          : set evs;                                                    \
paulson@5114
   622
\        (ALL NA k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs);     \
paulson@5114
   623
\        A ~: bad;  B ~: bad;  evs : yahalom |]       \
paulson@5114
   624
\     ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
paulson@4598
   625
by (forward_tac [B_trusts_YM4] 1);
paulson@3444
   626
by (REPEAT_FIRST (eresolve_tac [asm_rl, spec]));
paulson@3683
   627
by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1);
paulson@3444
   628
by (rtac lemma 1);
paulson@3444
   629
by (rtac Spy_not_see_encrypted_key 2);
paulson@3444
   630
by (REPEAT_FIRST assume_tac);
wenzelm@4091
   631
by (blast_tac (claset() addSEs [MPair_parts]
paulson@4238
   632
	       	        addDs [Says_imp_spies RS parts.Inj]) 1);
paulson@3444
   633
qed_spec_mp "YM4_imp_A_Said_YM3";