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