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