src/HOL/Auth/NS_Shared.ML
author paulson
Thu Jan 08 18:10:34 1998 +0100 (1998-01-08)
changeset 4537 4e835bd9fada
parent 4509 828148415197
child 4831 dae4d63a1318
permissions -rw-r--r--
Expressed most Oops rules using Notes instead of Says, and other tidying
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@4509
   100
by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
paulson@2516
   101
(*NS2, NS4, NS5*)
paulson@4470
   102
by (ALLGOALS (Blast_tac));
paulson@2160
   103
qed_spec_mp "new_keys_not_used";
paulson@1934
   104
paulson@1934
   105
bind_thm ("new_keys_not_analzd",
paulson@2032
   106
          [analz_subset_parts RS keysFor_mono,
paulson@2032
   107
           new_keys_not_used] MRS contra_subsetD);
paulson@1934
   108
paulson@1934
   109
Addsimps [new_keys_not_used, new_keys_not_analzd];
paulson@1934
   110
paulson@1934
   111
paulson@1934
   112
(** Lemmas concerning the form of items passed in messages **)
paulson@1934
   113
paulson@2015
   114
(*Describes the form of K, X and K' when the Server sends this message.*)
paulson@1934
   115
goal thy 
paulson@3683
   116
 "!!evs. [| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) : set evs; \
paulson@3519
   117
\           evs : ns_shared |]                           \
paulson@4267
   118
\        ==> K ~: range shrK &                           \
paulson@4267
   119
\            X = (Crypt (shrK B) {|Key K, Agent A|}) &   \
paulson@2516
   120
\            K' = shrK A";
paulson@2032
   121
by (etac rev_mp 1);
paulson@2032
   122
by (etac ns_shared.induct 1);
paulson@4477
   123
by Auto_tac;
paulson@1934
   124
qed "Says_Server_message_form";
paulson@1934
   125
paulson@1934
   126
paulson@2070
   127
(*If the encrypted message appears then it originated with the Server*)
paulson@1934
   128
goal thy
paulson@3683
   129
 "!!evs. [| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
paulson@4267
   130
\           A ~: bad;  evs : ns_shared |]                                 \
paulson@4267
   131
\         ==> Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})    \
paulson@3651
   132
\               : set evs";
paulson@2070
   133
by (etac rev_mp 1);
paulson@3519
   134
by (parts_induct_tac 1);
paulson@4470
   135
by (Blast_tac 1);
paulson@2323
   136
qed "A_trusts_NS2";
paulson@1934
   137
paulson@1965
   138
paulson@4331
   139
goal thy
paulson@4331
   140
 "!!evs. [| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
paulson@4331
   141
\           A ~: bad;  evs : ns_shared |]                                 \
paulson@4331
   142
\         ==> K ~: range shrK &  X = (Crypt (shrK B) {|Key K, Agent A|})";
paulson@4331
   143
by (blast_tac (claset() addSDs [A_trusts_NS2, Says_Server_message_form]) 1);
paulson@4331
   144
qed "cert_A_form";
paulson@4331
   145
paulson@4331
   146
paulson@1965
   147
(*EITHER describes the form of X when the following message is sent, 
paulson@1965
   148
  OR     reduces it to the Fake case.
paulson@1965
   149
  Use Says_Server_message_form if applicable.*)
paulson@1934
   150
goal thy 
paulson@2284
   151
 "!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})      \
paulson@3651
   152
\              : set evs;                                                  \
paulson@3651
   153
\           evs : ns_shared |]                                             \
paulson@3121
   154
\        ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|}))   \
paulson@3683
   155
\            | X : analz (spies evs)";
paulson@3683
   156
by (case_tac "A : bad" 1);
wenzelm@4091
   157
by (fast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]
paulson@4237
   158
                       addss (simpset())) 1);
paulson@4470
   159
by (blast_tac (claset() addSDs [cert_A_form]) 1);
paulson@1934
   160
qed "Says_S_message_form";
paulson@1934
   161
paulson@1934
   162
paulson@3519
   163
(*For proofs involving analz.*)
paulson@3683
   164
val analz_spies_tac = 
paulson@3519
   165
    forward_tac [Says_Server_message_form] 8 THEN
paulson@3519
   166
    forward_tac [Says_S_message_form] 5 THEN 
paulson@2516
   167
    REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac);
paulson@2131
   168
paulson@1934
   169
paulson@1934
   170
(****
paulson@1934
   171
 The following is to prove theorems of the form
paulson@1934
   172
paulson@3683
   173
  Key K : analz (insert (Key KAB) (spies evs)) ==>
paulson@3683
   174
  Key K : analz (spies evs)
paulson@1934
   175
paulson@1934
   176
 A more general formula must be proved inductively.
paulson@1934
   177
****)
paulson@1934
   178
paulson@1934
   179
paulson@1934
   180
(*NOT useful in this form, but it says that session keys are not used
paulson@1934
   181
  to encrypt messages containing other keys, in the actual protocol.
paulson@1934
   182
  We require that agents should behave like this subsequently also.*)
paulson@1934
   183
goal thy 
paulson@3519
   184
 "!!evs. [| evs : ns_shared;  Kab ~: range shrK |] ==>  \
paulson@4237
   185
\           (Crypt KAB X) : parts (spies evs) &         \
paulson@3683
   186
\           Key K : parts {X} --> Key K : parts (spies evs)";
paulson@3519
   187
by (parts_induct_tac 1);
paulson@4470
   188
(*Fake*)
wenzelm@4091
   189
by (blast_tac (claset() addSEs partsEs
paulson@4237
   190
                        addDs [impOfSubs parts_insert_subset_Un]) 1);
paulson@1965
   191
(*Base, NS4 and NS5*)
paulson@4477
   192
by Auto_tac;
paulson@1934
   193
result();
paulson@1934
   194
paulson@1934
   195
paulson@1934
   196
(** Session keys are not used to encrypt other session keys **)
paulson@1934
   197
paulson@2015
   198
(*The equality makes the induction hypothesis easier to apply*)
paulson@1934
   199
goal thy  
paulson@4237
   200
 "!!evs. evs : ns_shared ==>                             \
paulson@4237
   201
\  ALL K KK. KK <= Compl (range shrK) -->                \
paulson@3683
   202
\            (Key K : analz (Key``KK Un (spies evs))) =  \
paulson@3683
   203
\            (K : KK | Key K : analz (spies evs))";
paulson@2032
   204
by (etac ns_shared.induct 1);
paulson@3683
   205
by analz_spies_tac;
paulson@2516
   206
by (REPEAT_FIRST (resolve_tac [allI, impI]));
paulson@3961
   207
by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
paulson@3961
   208
(*Takes 9 secs*)
paulson@2516
   209
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
paulson@3451
   210
(*Fake*) 
paulson@4422
   211
by (spy_analz_tac 1);
paulson@2516
   212
qed_spec_mp "analz_image_freshK";
paulson@1934
   213
paulson@1934
   214
paulson@1934
   215
goal thy
paulson@4237
   216
 "!!evs. [| evs : ns_shared;  KAB ~: range shrK |] ==>  \
paulson@3683
   217
\        Key K : analz (insert (Key KAB) (spies evs)) = \
paulson@3683
   218
\        (K = KAB | Key K : analz (spies evs))";
paulson@2516
   219
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
paulson@2516
   220
qed "analz_insert_freshK";
paulson@1934
   221
paulson@1934
   222
paulson@2558
   223
(** The session key K uniquely identifies the message **)
paulson@1965
   224
paulson@1934
   225
goal thy 
paulson@4267
   226
 "!!evs. evs : ns_shared ==>                                               \
paulson@4237
   227
\      EX A' NA' B' X'. ALL A NA B X.                                      \
paulson@3683
   228
\       Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs \
paulson@3683
   229
\       -->         A=A' & NA=NA' & B=B' & X=X'";
paulson@2032
   230
by (etac ns_shared.induct 1);
wenzelm@4091
   231
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
paulson@3730
   232
by Safe_tac;
paulson@2070
   233
(*NS3*)
paulson@2070
   234
by (ex_strip_tac 2);
paulson@3121
   235
by (Blast_tac 2);
paulson@2070
   236
(*NS2: it can't be a new key*)
paulson@2070
   237
by (expand_case_tac "K = ?y" 1);
paulson@2070
   238
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
paulson@4470
   239
by (Blast_tac 1);
paulson@1934
   240
val lemma = result();
paulson@1934
   241
paulson@1934
   242
(*In messages of this form, the session key uniquely identifies the rest*)
paulson@1934
   243
goal thy 
paulson@4237
   244
 "!!evs. [| Says Server A                                               \
paulson@4237
   245
\             (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs;     \ 
paulson@4237
   246
\           Says Server A'                                              \
paulson@3683
   247
\             (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) : set evs; \
paulson@3519
   248
\           evs : ns_shared |] ==> A=A' & NA=NA' & B=B' & X = X'";
paulson@2451
   249
by (prove_unique_tac lemma 1);
paulson@1934
   250
qed "unique_session_keys";
paulson@1934
   251
paulson@1934
   252
paulson@2032
   253
(** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
paulson@2015
   254
paulson@1934
   255
goal thy 
paulson@3961
   256
 "!!evs. [| A ~: bad;  B ~: bad;  evs : ns_shared |]                   \
paulson@2015
   257
\        ==> Says Server A                                             \
paulson@2284
   258
\              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
paulson@2284
   259
\                                Crypt (shrK B) {|Key K, Agent A|}|})  \
paulson@3466
   260
\             : set evs -->                                            \
paulson@4537
   261
\        (ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs) -->          \
paulson@3683
   262
\        Key K ~: analz (spies evs)";
paulson@2032
   263
by (etac ns_shared.induct 1);
paulson@3683
   264
by analz_spies_tac;
paulson@1934
   265
by (ALLGOALS 
paulson@2015
   266
    (asm_simp_tac 
wenzelm@4091
   267
     (simpset() addsimps ([analz_insert_eq, analz_insert_freshK] @ 
paulson@4237
   268
			  pushes @ expand_ifs))));
paulson@3451
   269
(*Oops*)
paulson@4509
   270
by (blast_tac (claset() addSDs [unique_session_keys]) 5);
paulson@3679
   271
(*NS3, replay sub-case*) 
paulson@3451
   272
by (Blast_tac 4);
paulson@1934
   273
(*NS2*)
paulson@4470
   274
by (Blast_tac 2);
paulson@3451
   275
(*Fake*) 
paulson@3451
   276
by (spy_analz_tac 1);
paulson@3679
   277
(*NS3, Server sub-case*) (**LEVEL 6 **)
wenzelm@4091
   278
by (clarify_tac (claset() delrules [impCE]) 1);
paulson@3683
   279
by (forward_tac [Says_imp_spies RS parts.Inj RS A_trusts_NS2] 1);
paulson@2170
   280
by (assume_tac 2);
wenzelm@4091
   281
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS
paulson@4470
   282
			       Crypt_Spy_analz_bad]) 1);
wenzelm@4091
   283
by (blast_tac (claset() addDs [unique_session_keys]) 1);
paulson@2070
   284
val lemma = result() RS mp RS mp RSN(2,rev_notE);
paulson@2015
   285
paulson@2015
   286
paulson@2015
   287
(*Final version: Server's message in the most abstract form*)
paulson@2015
   288
goal thy 
paulson@4237
   289
 "!!evs. [| Says Server A                                        \
paulson@4331
   290
\              (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;   \
paulson@4537
   291
\           ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs;      \
paulson@3683
   292
\           A ~: bad;  B ~: bad;  evs : ns_shared                \
paulson@3683
   293
\        |] ==> Key K ~: analz (spies evs)";
paulson@2015
   294
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
wenzelm@4091
   295
by (blast_tac (claset() addSDs [lemma]) 1);
paulson@2032
   296
qed "Spy_not_see_encrypted_key";
paulson@2032
   297
paulson@2032
   298
paulson@2070
   299
(**** Guarantees available at various stages of protocol ***)
paulson@2070
   300
paulson@3651
   301
A_trusts_NS2 RS Spy_not_see_encrypted_key;
paulson@2070
   302
paulson@2070
   303
paulson@2070
   304
(*If the encrypted message appears then it originated with the Server*)
paulson@2070
   305
goal thy
paulson@4237
   306
 "!!evs. [| Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs);     \
paulson@4237
   307
\           B ~: bad;  evs : ns_shared |]                              \
paulson@2070
   308
\         ==> EX NA. Says Server A                                     \
paulson@2284
   309
\              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
paulson@2284
   310
\                                Crypt (shrK B) {|Key K, Agent A|}|})  \
nipkow@3465
   311
\             : set evs";
paulson@2070
   312
by (etac rev_mp 1);
paulson@3519
   313
by (parts_induct_tac 1);
paulson@3121
   314
by (ALLGOALS Blast_tac);
paulson@2323
   315
qed "B_trusts_NS3";
paulson@2070
   316
paulson@2070
   317
paulson@2070
   318
goal thy
paulson@4331
   319
 "!!evs. [| Crypt K (Nonce NB) : parts (spies evs);                   \
paulson@4331
   320
\           Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
paulson@4331
   321
\              : set evs;                                             \
paulson@4331
   322
\           Key K ~: analz (spies evs);                               \
paulson@4331
   323
\           evs : ns_shared |]                  \
paulson@4331
   324
\        ==> Says B A (Crypt K (Nonce NB)) : set evs";
paulson@4331
   325
by (etac rev_mp 1);
paulson@4331
   326
by (etac rev_mp 1);
paulson@4331
   327
by (etac rev_mp 1);
paulson@4331
   328
by (parts_induct_tac 1);
paulson@4267
   329
(*NS3*)
paulson@4267
   330
by (Blast_tac 3);
paulson@4470
   331
by (Blast_tac 1);
paulson@4267
   332
(*NS2: contradiction from the assumptions  
paulson@4331
   333
  Key K ~: used evs2  and Crypt K (Nonce NB) : parts (spies evs2) *)
paulson@4331
   334
by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)]
paulson@4331
   335
			addSDs [Crypt_imp_keysFor]) 1);
paulson@4331
   336
(**LEVEL 7**)
paulson@4331
   337
(*NS4*)
paulson@4331
   338
by (Clarify_tac 1);
paulson@4331
   339
by (not_bad_tac "Ba" 1);
paulson@4470
   340
by (blast_tac (claset() addDs [B_trusts_NS3, unique_session_keys]) 1);
paulson@4331
   341
qed "A_trusts_NS4_lemma";
paulson@2103
   342
paulson@4331
   343
paulson@4331
   344
(*This version no longer assumes that K is secure*)
paulson@2103
   345
goal thy
paulson@4267
   346
 "!!evs. [| Crypt K (Nonce NB) : parts (spies evs);                   \
paulson@4331
   347
\           Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
paulson@4537
   348
\           ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs;           \
paulson@4267
   349
\           A ~: bad;  B ~: bad;  evs : ns_shared |]                  \
nipkow@3465
   350
\        ==> Says B A (Crypt K (Nonce NB)) : set evs";
paulson@4331
   351
by (blast_tac (claset() addSIs [A_trusts_NS2, A_trusts_NS4_lemma]
paulson@4267
   352
	         addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1);
paulson@2323
   353
qed "A_trusts_NS4";
paulson@4331
   354
paulson@4331
   355
paulson@4331
   356
(*If the session key has been used in NS4 then somebody has forwarded
paulson@4331
   357
  component X in some instance of NS4.  Perhaps an interesting property, 
paulson@4331
   358
  but not needed (after all) for the proofs below.*)
paulson@4331
   359
goal thy
paulson@4331
   360
 "!!evs. [| Crypt K (Nonce NB) : parts (spies evs);     \
paulson@4331
   361
\           Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
paulson@4331
   362
\             : set evs;                                              \
paulson@4331
   363
\           Key K ~: analz (spies evs);                               \
paulson@4331
   364
\           evs : ns_shared |]                              \
paulson@4331
   365
\        ==> EX A'. Says A' B X : set evs";
paulson@4331
   366
by (etac rev_mp 1);
paulson@4331
   367
by (etac rev_mp 1);
paulson@4331
   368
by (etac rev_mp 1);
paulson@4331
   369
by (parts_induct_tac 1);
paulson@4331
   370
by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
paulson@4331
   371
by (ALLGOALS Clarify_tac);
paulson@4470
   372
by (Blast_tac 1);
paulson@4331
   373
(**LEVEL 7**)
paulson@4331
   374
(*NS2*)
paulson@4331
   375
by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)]
paulson@4331
   376
			addSDs [Crypt_imp_keysFor]) 1);
paulson@4331
   377
(*NS4*)
paulson@4331
   378
by (not_bad_tac "Ba" 1);
paulson@4331
   379
by (Asm_full_simp_tac 1);
paulson@4331
   380
by (forward_tac [Says_imp_spies RS parts.Inj RS B_trusts_NS3] 1);
paulson@4331
   381
by (ALLGOALS Clarify_tac);
paulson@4331
   382
by (blast_tac (claset() addDs [unique_session_keys]) 1);
paulson@4331
   383
qed "NS4_implies_NS3";
paulson@4331
   384
paulson@4331
   385
paulson@4331
   386
goal thy
paulson@4331
   387
 "!!evs. [| B ~: bad;  evs : ns_shared |]                              \
paulson@4331
   388
\        ==> Key K ~: analz (spies evs) -->                            \
paulson@4331
   389
\            Says Server A                                     \
paulson@4331
   390
\              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
paulson@4331
   391
\                                Crypt (shrK B) {|Key K, Agent A|}|})  \
paulson@4331
   392
\             : set evs -->         \
paulson@4331
   393
\            Says B A (Crypt K (Nonce NB))  : set evs -->  \
paulson@4331
   394
\            Crypt K {|Nonce NB, Nonce NB|} : parts (spies evs) --> \
paulson@4331
   395
\            Says A B (Crypt K {|Nonce NB, Nonce NB|}) : set evs";
paulson@4331
   396
by (parts_induct_tac 1);
paulson@4331
   397
(*NS4*)
paulson@4470
   398
by (Blast_tac 4);
paulson@4331
   399
(*NS3*)
paulson@4470
   400
by (blast_tac (claset() addSDs [cert_A_form]) 3);
paulson@4331
   401
(*NS2*)
paulson@4331
   402
by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)]
paulson@4331
   403
			addSDs [Crypt_imp_keysFor]) 2);
paulson@4470
   404
by (Blast_tac 1);
paulson@4331
   405
(**LEVEL 5**)
paulson@4331
   406
(*NS5*)
paulson@4331
   407
by (Clarify_tac 1);
paulson@4331
   408
by (not_bad_tac "Aa" 1);
paulson@4470
   409
by (blast_tac (claset() addDs [A_trusts_NS2, unique_session_keys]) 1);
paulson@4331
   410
val lemma = result();
paulson@4331
   411
paulson@4331
   412
paulson@4331
   413
(*Very strong Oops condition reveals protocol's weakness*)
paulson@4331
   414
goal thy
paulson@4331
   415
 "!!evs. [| Crypt K {|Nonce NB, Nonce NB|} : parts (spies evs);      \
paulson@4331
   416
\           Says B A (Crypt K (Nonce NB))  : set evs;                \
paulson@4331
   417
\           Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs);   \
paulson@4537
   418
\           ALL NA NB. Notes Spy {|NA, NB, Key K|} ~: set evs;       \
paulson@4331
   419
\           A ~: bad;  B ~: bad;  evs : ns_shared |]                 \
paulson@4331
   420
\        ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) : set evs";
paulson@4331
   421
by (dtac B_trusts_NS3 1);
paulson@4331
   422
by (ALLGOALS Clarify_tac);
paulson@4331
   423
by (blast_tac (claset() addSIs [normalize_thm [RSspec, RSmp] lemma]
paulson@4331
   424
	         addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1);
paulson@4331
   425
qed "B_trusts_NS5";