src/HOL/Auth/NS_Shared.ML
author paulson
Wed Dec 24 10:02:30 1997 +0100 (1997-12-24)
changeset 4477 b3e5857d8d99
parent 4470 af3239def3d4
child 4509 828148415197
permissions -rw-r--r--
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson@1934
     1
(*  Title:      HOL/Auth/NS_Shared
paulson@1934
     2
    ID:         $Id$
paulson@1934
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@1934
     4
    Copyright   1996  University of Cambridge
paulson@1934
     5
paulson@1934
     6
Inductive relation "ns_shared" for Needham-Schroeder Shared-Key protocol.
paulson@1934
     7
paulson@1934
     8
From page 247 of
paulson@1934
     9
  Burrows, Abadi and Needham.  A Logic of Authentication.
paulson@1934
    10
  Proc. Royal Soc. 426 (1989)
paulson@1934
    11
*)
paulson@1934
    12
paulson@1934
    13
open NS_Shared;
paulson@1934
    14
wenzelm@4449
    15
set proof_timing;
paulson@1997
    16
HOL_quantifiers := false;
paulson@1997
    17
paulson@4470
    18
AddEs spies_partsEs;
paulson@4470
    19
AddDs [impOfSubs analz_subset_parts];
paulson@4470
    20
AddDs [impOfSubs Fake_parts_insert];
paulson@4470
    21
paulson@1997
    22
paulson@2323
    23
(*A "possibility property": there are traces that reach the end*)
paulson@1997
    24
goal thy 
paulson@3466
    25
 "!!A B. [| A ~= B; A ~= Server; B ~= Server |]       \
paulson@4237
    26
\        ==> EX N K. EX evs: ns_shared.               \
nipkow@3465
    27
\               Says A B (Crypt K {|Nonce N, Nonce N|}) : set evs";
paulson@1997
    28
by (REPEAT (resolve_tac [exI,bexI] 1));
paulson@2516
    29
by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS 
paulson@2516
    30
          ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2);
paulson@2516
    31
by possibility_tac;
paulson@2015
    32
result();
paulson@2015
    33
paulson@3675
    34
goal thy 
paulson@3675
    35
 "!!A B. [| A ~= B; A ~= Server; B ~= Server |]       \
paulson@3675
    36
\        ==> EX evs: ns_shared.          \
paulson@3675
    37
\               Says A B (Crypt ?K {|Nonce ?N, Nonce ?N|}) : set evs";
paulson@3675
    38
by (REPEAT (resolve_tac [exI,bexI] 1));
paulson@3675
    39
by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS 
paulson@3675
    40
          ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2);
paulson@3675
    41
by possibility_tac;
paulson@1943
    42
paulson@1934
    43
(**** Inductive proofs about ns_shared ****)
paulson@1934
    44
paulson@1934
    45
(*Nobody sends themselves messages*)
paulson@3519
    46
goal thy "!!evs. evs : ns_shared ==> ALL A X. Says A A X ~: set evs";
paulson@2032
    47
by (etac ns_shared.induct 1);
paulson@4477
    48
by Auto_tac;
paulson@1934
    49
qed_spec_mp "not_Says_to_self";
paulson@1934
    50
Addsimps [not_Says_to_self];
paulson@1934
    51
AddSEs   [not_Says_to_self RSN (2, rev_notE)];
paulson@1934
    52
paulson@1943
    53
(*For reasoning about the encrypted portion of message NS3*)
nipkow@3465
    54
goal thy "!!evs. Says S A (Crypt KA {|N, B, K, X|}) : set evs \
paulson@3683
    55
\                ==> X : parts (spies evs)";
paulson@4470
    56
by (Blast_tac 1);
paulson@3683
    57
qed "NS3_msg_in_parts_spies";
paulson@2032
    58
                              
paulson@2070
    59
goal thy
nipkow@3465
    60
    "!!evs. Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set evs \
paulson@3683
    61
\           ==> K : parts (spies evs)";
paulson@4470
    62
by (Blast_tac 1);
paulson@3683
    63
qed "Oops_parts_spies";
paulson@2070
    64
paulson@3683
    65
(*For proving the easier theorems about X ~: parts (spies evs).*)
paulson@3519
    66
fun parts_induct_tac i = 
paulson@4331
    67
  EVERY [etac ns_shared.induct i,
paulson@4331
    68
	 REPEAT (FIRSTGOAL analz_mono_contra_tac),
paulson@4331
    69
	 forward_tac [Oops_parts_spies] (i+7),
paulson@4331
    70
	 forward_tac [NS3_msg_in_parts_spies] (i+4),
paulson@4331
    71
	 prove_simple_subgoals_tac i];
paulson@2070
    72
paulson@1934
    73
paulson@3683
    74
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
paulson@2015
    75
    sends messages containing X! **)
paulson@1934
    76
paulson@3683
    77
(*Spy never sees another agent's shared key! (unless it's bad at start)*)
paulson@1934
    78
goal thy 
paulson@3683
    79
 "!!evs. evs : ns_shared ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
paulson@3519
    80
by (parts_induct_tac 1);
paulson@3961
    81
by (ALLGOALS Blast_tac);
paulson@2131
    82
qed "Spy_see_shrK";
paulson@2131
    83
Addsimps [Spy_see_shrK];
paulson@1934
    84
paulson@2131
    85
goal thy 
paulson@3683
    86
 "!!evs. evs : ns_shared ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
paulson@4477
    87
by Auto_tac;
paulson@2131
    88
qed "Spy_analz_shrK";
paulson@2131
    89
Addsimps [Spy_analz_shrK];
paulson@1934
    90
paulson@4470
    91
AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
paulson@4470
    92
	Spy_analz_shrK RSN (2, rev_iffD1)];
paulson@1934
    93
paulson@2070
    94
paulson@2516
    95
(*Nobody can have used non-existent keys!*)
paulson@3519
    96
goal thy "!!evs. evs : ns_shared ==>      \
paulson@3683
    97
\         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
paulson@3519
    98
by (parts_induct_tac 1);
paulson@2516
    99
(*Fake*)
paulson@2516
   100
by (best_tac
wenzelm@4091
   101
      (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
paulson@4237
   102
                addIs  [impOfSubs analz_subset_parts]
paulson@4237
   103
                addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
paulson@4237
   104
                addss  (simpset())) 1);
paulson@2516
   105
(*NS2, NS4, NS5*)
paulson@4470
   106
by (ALLGOALS (Blast_tac));
paulson@2160
   107
qed_spec_mp "new_keys_not_used";
paulson@1934
   108
paulson@1934
   109
bind_thm ("new_keys_not_analzd",
paulson@2032
   110
          [analz_subset_parts RS keysFor_mono,
paulson@2032
   111
           new_keys_not_used] MRS contra_subsetD);
paulson@1934
   112
paulson@1934
   113
Addsimps [new_keys_not_used, new_keys_not_analzd];
paulson@1934
   114
paulson@1934
   115
paulson@1934
   116
(** Lemmas concerning the form of items passed in messages **)
paulson@1934
   117
paulson@2015
   118
(*Describes the form of K, X and K' when the Server sends this message.*)
paulson@1934
   119
goal thy 
paulson@3683
   120
 "!!evs. [| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) : set evs; \
paulson@3519
   121
\           evs : ns_shared |]                           \
paulson@4267
   122
\        ==> K ~: range shrK &                           \
paulson@4267
   123
\            X = (Crypt (shrK B) {|Key K, Agent A|}) &   \
paulson@2516
   124
\            K' = shrK A";
paulson@2032
   125
by (etac rev_mp 1);
paulson@2032
   126
by (etac ns_shared.induct 1);
paulson@4477
   127
by Auto_tac;
paulson@1934
   128
qed "Says_Server_message_form";
paulson@1934
   129
paulson@1934
   130
paulson@2070
   131
(*If the encrypted message appears then it originated with the Server*)
paulson@1934
   132
goal thy
paulson@3683
   133
 "!!evs. [| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
paulson@4267
   134
\           A ~: bad;  evs : ns_shared |]                                 \
paulson@4267
   135
\         ==> Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})    \
paulson@3651
   136
\               : set evs";
paulson@2070
   137
by (etac rev_mp 1);
paulson@3519
   138
by (parts_induct_tac 1);
paulson@4470
   139
by (Blast_tac 1);
paulson@2323
   140
qed "A_trusts_NS2";
paulson@1934
   141
paulson@1965
   142
paulson@4331
   143
goal thy
paulson@4331
   144
 "!!evs. [| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
paulson@4331
   145
\           A ~: bad;  evs : ns_shared |]                                 \
paulson@4331
   146
\         ==> K ~: range shrK &  X = (Crypt (shrK B) {|Key K, Agent A|})";
paulson@4331
   147
by (blast_tac (claset() addSDs [A_trusts_NS2, Says_Server_message_form]) 1);
paulson@4331
   148
qed "cert_A_form";
paulson@4331
   149
paulson@4331
   150
paulson@1965
   151
(*EITHER describes the form of X when the following message is sent, 
paulson@1965
   152
  OR     reduces it to the Fake case.
paulson@1965
   153
  Use Says_Server_message_form if applicable.*)
paulson@1934
   154
goal thy 
paulson@2284
   155
 "!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})      \
paulson@3651
   156
\              : set evs;                                                  \
paulson@3651
   157
\           evs : ns_shared |]                                             \
paulson@3121
   158
\        ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|}))   \
paulson@3683
   159
\            | X : analz (spies evs)";
paulson@3683
   160
by (case_tac "A : bad" 1);
wenzelm@4091
   161
by (fast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]
paulson@4237
   162
                       addss (simpset())) 1);
paulson@4470
   163
by (blast_tac (claset() addSDs [cert_A_form]) 1);
paulson@1934
   164
qed "Says_S_message_form";
paulson@1934
   165
paulson@1934
   166
paulson@3519
   167
(*For proofs involving analz.*)
paulson@3683
   168
val analz_spies_tac = 
paulson@3519
   169
    forward_tac [Says_Server_message_form] 8 THEN
paulson@3519
   170
    forward_tac [Says_S_message_form] 5 THEN 
paulson@2516
   171
    REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac);
paulson@2131
   172
paulson@1934
   173
paulson@1934
   174
(****
paulson@1934
   175
 The following is to prove theorems of the form
paulson@1934
   176
paulson@3683
   177
  Key K : analz (insert (Key KAB) (spies evs)) ==>
paulson@3683
   178
  Key K : analz (spies evs)
paulson@1934
   179
paulson@1934
   180
 A more general formula must be proved inductively.
paulson@1934
   181
****)
paulson@1934
   182
paulson@1934
   183
paulson@1934
   184
(*NOT useful in this form, but it says that session keys are not used
paulson@1934
   185
  to encrypt messages containing other keys, in the actual protocol.
paulson@1934
   186
  We require that agents should behave like this subsequently also.*)
paulson@1934
   187
goal thy 
paulson@3519
   188
 "!!evs. [| evs : ns_shared;  Kab ~: range shrK |] ==>  \
paulson@4237
   189
\           (Crypt KAB X) : parts (spies evs) &         \
paulson@3683
   190
\           Key K : parts {X} --> Key K : parts (spies evs)";
paulson@3519
   191
by (parts_induct_tac 1);
paulson@4470
   192
(*Fake*)
wenzelm@4091
   193
by (blast_tac (claset() addSEs partsEs
paulson@4237
   194
                        addDs [impOfSubs parts_insert_subset_Un]) 1);
paulson@1965
   195
(*Base, NS4 and NS5*)
paulson@4477
   196
by Auto_tac;
paulson@1934
   197
result();
paulson@1934
   198
paulson@1934
   199
paulson@1934
   200
(** Session keys are not used to encrypt other session keys **)
paulson@1934
   201
paulson@2015
   202
(*The equality makes the induction hypothesis easier to apply*)
paulson@1934
   203
goal thy  
paulson@4237
   204
 "!!evs. evs : ns_shared ==>                             \
paulson@4237
   205
\  ALL K KK. KK <= Compl (range shrK) -->                \
paulson@3683
   206
\            (Key K : analz (Key``KK Un (spies evs))) =  \
paulson@3683
   207
\            (K : KK | Key K : analz (spies evs))";
paulson@2032
   208
by (etac ns_shared.induct 1);
paulson@3683
   209
by analz_spies_tac;
paulson@2516
   210
by (REPEAT_FIRST (resolve_tac [allI, impI]));
paulson@3961
   211
by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
paulson@3961
   212
(*Takes 9 secs*)
paulson@2516
   213
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
paulson@3451
   214
(*Fake*) 
paulson@4422
   215
by (spy_analz_tac 1);
paulson@2516
   216
qed_spec_mp "analz_image_freshK";
paulson@1934
   217
paulson@1934
   218
paulson@1934
   219
goal thy
paulson@4237
   220
 "!!evs. [| evs : ns_shared;  KAB ~: range shrK |] ==>  \
paulson@3683
   221
\        Key K : analz (insert (Key KAB) (spies evs)) = \
paulson@3683
   222
\        (K = KAB | Key K : analz (spies evs))";
paulson@2516
   223
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
paulson@2516
   224
qed "analz_insert_freshK";
paulson@1934
   225
paulson@1934
   226
paulson@2558
   227
(** The session key K uniquely identifies the message **)
paulson@1965
   228
paulson@1934
   229
goal thy 
paulson@4267
   230
 "!!evs. evs : ns_shared ==>                                               \
paulson@4237
   231
\      EX A' NA' B' X'. ALL A NA B X.                                      \
paulson@3683
   232
\       Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs \
paulson@3683
   233
\       -->         A=A' & NA=NA' & B=B' & X=X'";
paulson@2032
   234
by (etac ns_shared.induct 1);
wenzelm@4091
   235
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
paulson@3730
   236
by Safe_tac;
paulson@2070
   237
(*NS3*)
paulson@2070
   238
by (ex_strip_tac 2);
paulson@3121
   239
by (Blast_tac 2);
paulson@2070
   240
(*NS2: it can't be a new key*)
paulson@2070
   241
by (expand_case_tac "K = ?y" 1);
paulson@2070
   242
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
paulson@4470
   243
by (Blast_tac 1);
paulson@1934
   244
val lemma = result();
paulson@1934
   245
paulson@1934
   246
(*In messages of this form, the session key uniquely identifies the rest*)
paulson@1934
   247
goal thy 
paulson@4237
   248
 "!!evs. [| Says Server A                                               \
paulson@4237
   249
\             (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs;     \ 
paulson@4237
   250
\           Says Server A'                                              \
paulson@3683
   251
\             (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) : set evs; \
paulson@3519
   252
\           evs : ns_shared |] ==> A=A' & NA=NA' & B=B' & X = X'";
paulson@2451
   253
by (prove_unique_tac lemma 1);
paulson@1934
   254
qed "unique_session_keys";
paulson@1934
   255
paulson@1934
   256
paulson@2032
   257
(** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
paulson@2015
   258
paulson@1934
   259
goal thy 
paulson@3961
   260
 "!!evs. [| A ~: bad;  B ~: bad;  evs : ns_shared |]                   \
paulson@2015
   261
\        ==> Says Server A                                             \
paulson@2284
   262
\              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
paulson@2284
   263
\                                Crypt (shrK B) {|Key K, Agent A|}|})  \
paulson@3466
   264
\             : set evs -->                                            \
paulson@3466
   265
\        (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs) -->         \
paulson@3683
   266
\        Key K ~: analz (spies evs)";
paulson@2032
   267
by (etac ns_shared.induct 1);
paulson@3683
   268
by analz_spies_tac;
paulson@1934
   269
by (ALLGOALS 
paulson@2015
   270
    (asm_simp_tac 
wenzelm@4091
   271
     (simpset() addsimps ([analz_insert_eq, analz_insert_freshK] @ 
paulson@4237
   272
			  pushes @ expand_ifs))));
paulson@3451
   273
(*Oops*)
wenzelm@4091
   274
by (blast_tac (claset() addDs [unique_session_keys]) 5);
paulson@3679
   275
(*NS3, replay sub-case*) 
paulson@3451
   276
by (Blast_tac 4);
paulson@1934
   277
(*NS2*)
paulson@4470
   278
by (Blast_tac 2);
paulson@3451
   279
(*Fake*) 
paulson@3451
   280
by (spy_analz_tac 1);
paulson@3679
   281
(*NS3, Server sub-case*) (**LEVEL 6 **)
wenzelm@4091
   282
by (clarify_tac (claset() delrules [impCE]) 1);
paulson@3683
   283
by (forward_tac [Says_imp_spies RS parts.Inj RS A_trusts_NS2] 1);
paulson@2170
   284
by (assume_tac 2);
wenzelm@4091
   285
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS
paulson@4470
   286
			       Crypt_Spy_analz_bad]) 1);
wenzelm@4091
   287
by (blast_tac (claset() addDs [unique_session_keys]) 1);
paulson@2070
   288
val lemma = result() RS mp RS mp RSN(2,rev_notE);
paulson@2015
   289
paulson@2015
   290
paulson@2015
   291
(*Final version: Server's message in the most abstract form*)
paulson@2015
   292
goal thy 
paulson@4237
   293
 "!!evs. [| Says Server A                                        \
paulson@4331
   294
\              (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;   \
paulson@4331
   295
\           ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs;     \
paulson@3683
   296
\           A ~: bad;  B ~: bad;  evs : ns_shared                \
paulson@3683
   297
\        |] ==> Key K ~: analz (spies evs)";
paulson@2015
   298
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
wenzelm@4091
   299
by (blast_tac (claset() addSDs [lemma]) 1);
paulson@2032
   300
qed "Spy_not_see_encrypted_key";
paulson@2032
   301
paulson@2032
   302
paulson@2070
   303
(**** Guarantees available at various stages of protocol ***)
paulson@2070
   304
paulson@3651
   305
A_trusts_NS2 RS Spy_not_see_encrypted_key;
paulson@2070
   306
paulson@2070
   307
paulson@2070
   308
(*If the encrypted message appears then it originated with the Server*)
paulson@2070
   309
goal thy
paulson@4237
   310
 "!!evs. [| Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs);     \
paulson@4237
   311
\           B ~: bad;  evs : ns_shared |]                              \
paulson@2070
   312
\         ==> EX NA. Says Server A                                     \
paulson@2284
   313
\              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
paulson@2284
   314
\                                Crypt (shrK B) {|Key K, Agent A|}|})  \
nipkow@3465
   315
\             : set evs";
paulson@2070
   316
by (etac rev_mp 1);
paulson@3519
   317
by (parts_induct_tac 1);
paulson@3121
   318
by (ALLGOALS Blast_tac);
paulson@2323
   319
qed "B_trusts_NS3";
paulson@2070
   320
paulson@2070
   321
paulson@2070
   322
goal thy
paulson@4331
   323
 "!!evs. [| Crypt K (Nonce NB) : parts (spies evs);                   \
paulson@4331
   324
\           Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
paulson@4331
   325
\              : set evs;                                             \
paulson@4331
   326
\           Key K ~: analz (spies evs);                               \
paulson@4331
   327
\           evs : ns_shared |]                  \
paulson@4331
   328
\        ==> Says B A (Crypt K (Nonce NB)) : set evs";
paulson@4331
   329
by (etac rev_mp 1);
paulson@4331
   330
by (etac rev_mp 1);
paulson@4331
   331
by (etac rev_mp 1);
paulson@4331
   332
by (parts_induct_tac 1);
paulson@4267
   333
(*NS3*)
paulson@4267
   334
by (Blast_tac 3);
paulson@4470
   335
by (Blast_tac 1);
paulson@4267
   336
(*NS2: contradiction from the assumptions  
paulson@4331
   337
  Key K ~: used evs2  and Crypt K (Nonce NB) : parts (spies evs2) *)
paulson@4331
   338
by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)]
paulson@4331
   339
			addSDs [Crypt_imp_keysFor]) 1);
paulson@4331
   340
(**LEVEL 7**)
paulson@4331
   341
(*NS4*)
paulson@4331
   342
by (Clarify_tac 1);
paulson@4331
   343
by (not_bad_tac "Ba" 1);
paulson@4470
   344
by (blast_tac (claset() addDs [B_trusts_NS3, unique_session_keys]) 1);
paulson@4331
   345
qed "A_trusts_NS4_lemma";
paulson@2103
   346
paulson@4331
   347
paulson@4331
   348
(*This version no longer assumes that K is secure*)
paulson@2103
   349
goal thy
paulson@4267
   350
 "!!evs. [| Crypt K (Nonce NB) : parts (spies evs);                   \
paulson@4331
   351
\           Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
paulson@3466
   352
\           ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs;          \
paulson@4267
   353
\           A ~: bad;  B ~: bad;  evs : ns_shared |]                  \
nipkow@3465
   354
\        ==> Says B A (Crypt K (Nonce NB)) : set evs";
paulson@4331
   355
by (blast_tac (claset() addSIs [A_trusts_NS2, A_trusts_NS4_lemma]
paulson@4267
   356
	         addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1);
paulson@2323
   357
qed "A_trusts_NS4";
paulson@4331
   358
paulson@4331
   359
paulson@4331
   360
(*If the session key has been used in NS4 then somebody has forwarded
paulson@4331
   361
  component X in some instance of NS4.  Perhaps an interesting property, 
paulson@4331
   362
  but not needed (after all) for the proofs below.*)
paulson@4331
   363
goal thy
paulson@4331
   364
 "!!evs. [| Crypt K (Nonce NB) : parts (spies evs);     \
paulson@4331
   365
\           Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
paulson@4331
   366
\             : set evs;                                              \
paulson@4331
   367
\           Key K ~: analz (spies evs);                               \
paulson@4331
   368
\           evs : ns_shared |]                              \
paulson@4331
   369
\        ==> EX A'. Says A' B X : set evs";
paulson@4331
   370
by (etac rev_mp 1);
paulson@4331
   371
by (etac rev_mp 1);
paulson@4331
   372
by (etac rev_mp 1);
paulson@4331
   373
by (parts_induct_tac 1);
paulson@4331
   374
by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
paulson@4331
   375
by (ALLGOALS Clarify_tac);
paulson@4470
   376
by (Blast_tac 1);
paulson@4331
   377
(**LEVEL 7**)
paulson@4331
   378
(*NS2*)
paulson@4331
   379
by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)]
paulson@4331
   380
			addSDs [Crypt_imp_keysFor]) 1);
paulson@4331
   381
(*NS4*)
paulson@4331
   382
by (not_bad_tac "Ba" 1);
paulson@4331
   383
by (Asm_full_simp_tac 1);
paulson@4331
   384
by (forward_tac [Says_imp_spies RS parts.Inj RS B_trusts_NS3] 1);
paulson@4331
   385
by (ALLGOALS Clarify_tac);
paulson@4331
   386
by (blast_tac (claset() addDs [unique_session_keys]) 1);
paulson@4331
   387
qed "NS4_implies_NS3";
paulson@4331
   388
paulson@4331
   389
paulson@4331
   390
goal thy
paulson@4331
   391
 "!!evs. [| B ~: bad;  evs : ns_shared |]                              \
paulson@4331
   392
\        ==> Key K ~: analz (spies evs) -->                            \
paulson@4331
   393
\            Says Server A                                     \
paulson@4331
   394
\              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
paulson@4331
   395
\                                Crypt (shrK B) {|Key K, Agent A|}|})  \
paulson@4331
   396
\             : set evs -->         \
paulson@4331
   397
\            Says B A (Crypt K (Nonce NB))  : set evs -->  \
paulson@4331
   398
\            Crypt K {|Nonce NB, Nonce NB|} : parts (spies evs) --> \
paulson@4331
   399
\            Says A B (Crypt K {|Nonce NB, Nonce NB|}) : set evs";
paulson@4331
   400
by (parts_induct_tac 1);
paulson@4331
   401
(*NS4*)
paulson@4470
   402
by (Blast_tac 4);
paulson@4331
   403
(*NS3*)
paulson@4470
   404
by (blast_tac (claset() addSDs [cert_A_form]) 3);
paulson@4331
   405
(*NS2*)
paulson@4331
   406
by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)]
paulson@4331
   407
			addSDs [Crypt_imp_keysFor]) 2);
paulson@4470
   408
by (Blast_tac 1);
paulson@4331
   409
(**LEVEL 5**)
paulson@4331
   410
(*NS5*)
paulson@4331
   411
by (Clarify_tac 1);
paulson@4331
   412
by (not_bad_tac "Aa" 1);
paulson@4470
   413
by (blast_tac (claset() addDs [A_trusts_NS2, unique_session_keys]) 1);
paulson@4331
   414
val lemma = result();
paulson@4331
   415
paulson@4331
   416
paulson@4331
   417
(*Very strong Oops condition reveals protocol's weakness*)
paulson@4331
   418
goal thy
paulson@4331
   419
 "!!evs. [| Crypt K {|Nonce NB, Nonce NB|} : parts (spies evs);      \
paulson@4331
   420
\           Says B A (Crypt K (Nonce NB))  : set evs;                \
paulson@4331
   421
\           Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs);   \
paulson@4331
   422
\           ALL NA NB. Says A Spy {|NA, NB, Key K|} ~: set evs;      \
paulson@4331
   423
\           A ~: bad;  B ~: bad;  evs : ns_shared |]                 \
paulson@4331
   424
\        ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) : set evs";
paulson@4331
   425
by (dtac B_trusts_NS3 1);
paulson@4331
   426
by (ALLGOALS Clarify_tac);
paulson@4331
   427
by (blast_tac (claset() addSIs [normalize_thm [RSspec, RSmp] lemma]
paulson@4331
   428
	         addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1);
paulson@4331
   429
qed "B_trusts_NS5";