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