src/HOL/Auth/NS_Public.ML
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 2637 e9b203f854ae
child 3121 cbb6c0c1c58a
permissions -rw-r--r--
Dep. on Provers/nat_transitive
paulson@2318
     1
(*  Title:      HOL/Auth/NS_Public
paulson@2318
     2
    ID:         $Id$
paulson@2318
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@2318
     4
    Copyright   1996  University of Cambridge
paulson@2318
     5
paulson@2318
     6
Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol.
paulson@2318
     7
Version incorporating Lowe's fix (inclusion of B's identify in round 2).
paulson@2318
     8
*)
paulson@2318
     9
paulson@2318
    10
open NS_Public;
paulson@2318
    11
paulson@2318
    12
proof_timing:=true;
paulson@2318
    13
HOL_quantifiers := false;
paulson@2318
    14
oheimb@2637
    15
val op addss = op unsafe_addss;
oheimb@2637
    16
paulson@2318
    17
AddIffs [Spy_in_lost];
paulson@2318
    18
paulson@2318
    19
(*Replacing the variable by a constant improves search speed by 50%!*)
paulson@2318
    20
val Says_imp_sees_Spy' = 
paulson@2318
    21
    read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
paulson@2318
    22
paulson@2318
    23
paulson@2318
    24
(*A "possibility property": there are traces that reach the end*)
paulson@2318
    25
goal thy 
paulson@2318
    26
 "!!A B. A ~= B ==> EX NB. EX evs: ns_public.               \
paulson@2318
    27
\                     Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list evs";
paulson@2318
    28
by (REPEAT (resolve_tac [exI,bexI] 1));
paulson@2318
    29
by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2);
paulson@2516
    30
by possibility_tac;
paulson@2318
    31
result();
paulson@2318
    32
paulson@2318
    33
paulson@2318
    34
(**** Inductive proofs about ns_public ****)
paulson@2318
    35
paulson@2318
    36
(*Nobody sends themselves messages*)
paulson@2318
    37
goal thy "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set_of_list evs";
paulson@2318
    38
by (etac ns_public.induct 1);
paulson@2318
    39
by (Auto_tac());
paulson@2318
    40
qed_spec_mp "not_Says_to_self";
paulson@2318
    41
Addsimps [not_Says_to_self];
paulson@2318
    42
AddSEs   [not_Says_to_self RSN (2, rev_notE)];
paulson@2318
    43
paulson@2318
    44
paulson@2318
    45
(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
paulson@2318
    46
fun parts_induct_tac i = SELECT_GOAL
paulson@2318
    47
    (DETERM (etac ns_public.induct 1 THEN 
paulson@2318
    48
             (*Fake message*)
paulson@2318
    49
             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
paulson@2318
    50
                                           impOfSubs Fake_parts_insert]
paulson@2318
    51
                                    addss (!simpset)) 2)) THEN
paulson@2318
    52
     (*Base case*)
paulson@2318
    53
     fast_tac (!claset addss (!simpset)) 1 THEN
paulson@2318
    54
     ALLGOALS Asm_simp_tac) i;
paulson@2318
    55
paulson@2318
    56
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
paulson@2318
    57
    sends messages containing X! **)
paulson@2318
    58
paulson@2318
    59
(*Spy never sees another agent's private key! (unless it's lost at start)*)
paulson@2318
    60
goal thy 
paulson@2318
    61
 "!!evs. evs : ns_public \
paulson@2318
    62
\        ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)";
paulson@2318
    63
by (parts_induct_tac 1);
paulson@2318
    64
by (Auto_tac());
paulson@2318
    65
qed "Spy_see_priK";
paulson@2318
    66
Addsimps [Spy_see_priK];
paulson@2318
    67
paulson@2318
    68
goal thy 
paulson@2318
    69
 "!!evs. evs : ns_public \
paulson@2318
    70
\        ==> (Key (priK A) : analz (sees lost Spy evs)) = (A : lost)";
paulson@2318
    71
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
paulson@2318
    72
qed "Spy_analz_priK";
paulson@2318
    73
Addsimps [Spy_analz_priK];
paulson@2318
    74
paulson@2318
    75
goal thy  "!!A. [| Key (priK A) : parts (sees lost Spy evs);       \
paulson@2318
    76
\                  evs : ns_public |] ==> A:lost";
paulson@2318
    77
by (fast_tac (!claset addDs [Spy_see_priK]) 1);
paulson@2318
    78
qed "Spy_see_priK_D";
paulson@2318
    79
paulson@2318
    80
bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D);
paulson@2318
    81
AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
paulson@2318
    82
paulson@2318
    83
paulson@2418
    84
fun analz_induct_tac i = 
paulson@2516
    85
    etac ns_public.induct i     THEN
paulson@2418
    86
    ALLGOALS (asm_simp_tac 
paulson@2516
    87
              (!simpset addsimps [not_parts_not_analz]
paulson@2451
    88
                        setloop split_tac [expand_if]));
paulson@2318
    89
paulson@2318
    90
(**** Authenticity properties obtained from NS2 ****)
paulson@2318
    91
paulson@2318
    92
(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
paulson@2318
    93
  is secret.  (Honest users generate fresh nonces.)*)
paulson@2318
    94
goal thy 
paulson@2536
    95
 "!!evs. [| Nonce NA ~: analz (sees lost Spy evs);  \
paulson@2536
    96
\           Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs); \
paulson@2536
    97
\           evs : ns_public |]                      \
paulson@2536
    98
\ ==> Crypt (pubK C) {|NA', Nonce NA, Agent D|} ~: parts (sees lost Spy evs)";
paulson@2536
    99
by (etac rev_mp 1);
paulson@2536
   100
by (etac rev_mp 1);
paulson@2418
   101
by (analz_induct_tac 1);
paulson@2318
   102
(*NS3*)
paulson@2497
   103
by (fast_tac (!claset addSEs partsEs) 4);
paulson@2318
   104
(*NS2*)
paulson@2497
   105
by (fast_tac (!claset addSEs partsEs) 3);
paulson@2318
   106
(*Fake*)
paulson@2536
   107
by (deepen_tac (!claset addSIs [analz_insertI]
paulson@2536
   108
                        addDs [impOfSubs analz_subset_parts,
paulson@2536
   109
			       impOfSubs Fake_parts_insert]
paulson@2536
   110
			addss (!simpset)) 0 2);
paulson@2318
   111
(*Base*)
paulson@2374
   112
by (fast_tac (!claset addss (!simpset)) 1);
paulson@2536
   113
qed "no_nonce_NS1_NS2";
paulson@2318
   114
paulson@2318
   115
paulson@2480
   116
(*Unicity for NS1: nonce NA identifies agents A and B*)
paulson@2318
   117
goal thy 
paulson@2536
   118
 "!!evs. [| Nonce NA ~: analz (sees lost Spy evs);  evs : ns_public |]      \
paulson@2536
   119
\ ==> EX A' B'. ALL A B.                                                    \
paulson@2318
   120
\      Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \
paulson@2536
   121
\      A=A' & B=B'";
paulson@2536
   122
by (etac rev_mp 1);
paulson@2418
   123
by (analz_induct_tac 1);
paulson@2318
   124
(*NS1*)
paulson@2497
   125
by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
paulson@2318
   126
by (expand_case_tac "NA = ?y" 3 THEN
paulson@2497
   127
    REPEAT (fast_tac (!claset addSEs partsEs) 3));
paulson@2318
   128
(*Base*)
paulson@2318
   129
by (fast_tac (!claset addss (!simpset)) 1);
paulson@2318
   130
(*Fake*)
paulson@2497
   131
by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1);
paulson@2374
   132
by (step_tac (!claset addSIs [analz_insertI]) 1);
paulson@2318
   133
by (ex_strip_tac 1);
paulson@2318
   134
by (best_tac (!claset delrules [conjI]
paulson@2516
   135
                      addSDs [impOfSubs Fake_parts_insert]
paulson@2516
   136
                      addDs  [impOfSubs analz_subset_parts]
paulson@2318
   137
                      addss (!simpset)) 1);
paulson@2318
   138
val lemma = result();
paulson@2318
   139
paulson@2318
   140
goal thy 
paulson@2318
   141
 "!!evs. [| Crypt(pubK B)  {|Nonce NA, Agent A|}  : parts(sees lost Spy evs); \
paulson@2318
   142
\           Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(sees lost Spy evs); \
paulson@2318
   143
\           Nonce NA ~: analz (sees lost Spy evs);                            \
paulson@2318
   144
\           evs : ns_public |]                                                \
paulson@2318
   145
\        ==> A=A' & B=B'";
paulson@2480
   146
by (prove_unique_tac lemma 1);
paulson@2318
   147
qed "unique_NA";
paulson@2318
   148
paulson@2318
   149
paulson@2318
   150
(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
paulson@2318
   151
goal thy 
paulson@2536
   152
 "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set_of_list evs; \
paulson@2536
   153
\           A ~: lost;  B ~: lost;  evs : ns_public |]                        \
paulson@2536
   154
\        ==>  Nonce NA ~: analz (sees lost Spy evs)";
paulson@2536
   155
by (etac rev_mp 1);
paulson@2418
   156
by (analz_induct_tac 1);
paulson@2318
   157
(*NS3*)
paulson@2318
   158
by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
paulson@2318
   159
                      addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
paulson@2536
   160
(*NS2*)
paulson@2536
   161
by (deepen_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
paulson@2536
   162
                        addSEs [MPair_parts]
paulson@2536
   163
			addDs  [parts.Body, unique_NA]) 0 3);
paulson@2318
   164
(*NS1*)
paulson@2536
   165
by (fast_tac (!claset addSEs sees_Spy_partsEs
paulson@2497
   166
                      addIs  [impOfSubs analz_subset_parts]) 2);
paulson@2318
   167
(*Fake*)
paulson@2497
   168
by (spy_analz_tac 1);
paulson@2536
   169
qed "Spy_not_see_NA";
paulson@2318
   170
paulson@2318
   171
paulson@2318
   172
(*Authentication for A: if she receives message 2 and has used NA
paulson@2318
   173
  to start a run, then B has sent message 2.*)
paulson@2318
   174
goal thy 
paulson@2536
   175
 "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs;\
paulson@2536
   176
\           Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
paulson@2536
   177
\             : set_of_list evs;\
paulson@2536
   178
\           A ~: lost;  B ~: lost;  evs : ns_public |]  \
paulson@2536
   179
\        ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
paulson@2536
   180
\              : set_of_list evs";
paulson@2536
   181
by (etac rev_mp 1);
paulson@2536
   182
(*prepare induction over Crypt (pubK A) {|NA,NB,B|} : parts H*)
paulson@2536
   183
by (etac (Says_imp_sees_Spy' RS parts.Inj RS rev_mp) 1);
paulson@2318
   184
by (etac ns_public.induct 1);
paulson@2318
   185
by (ALLGOALS Asm_simp_tac);
paulson@2318
   186
(*NS1*)
paulson@2536
   187
by (fast_tac (!claset addSEs sees_Spy_partsEs) 2);
paulson@2318
   188
(*Fake*)
paulson@2318
   189
by (REPEAT_FIRST (resolve_tac [impI, conjI]));
paulson@2318
   190
by (fast_tac (!claset addss (!simpset)) 1);
paulson@2318
   191
by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1));
paulson@2318
   192
by (best_tac (!claset addSIs [disjI2]
paulson@2516
   193
                      addSDs [impOfSubs Fake_parts_insert]
paulson@2516
   194
                      addDs  [impOfSubs analz_subset_parts]
paulson@2516
   195
                      addss (!simpset)) 1);
paulson@2318
   196
qed "A_trusts_NS2";
paulson@2318
   197
paulson@2318
   198
(*If the encrypted message appears then it originated with Alice in NS1*)
paulson@2318
   199
goal thy 
paulson@2536
   200
 "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs); \
paulson@2536
   201
\           Nonce NA ~: analz (sees lost Spy evs);                 \
paulson@2536
   202
\           evs : ns_public |]                                     \
paulson@2536
   203
\   ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs";
paulson@2536
   204
by (etac rev_mp 1);
paulson@2536
   205
by (etac rev_mp 1);
paulson@2480
   206
by (analz_induct_tac 1);
paulson@2318
   207
(*Fake*)
paulson@2318
   208
by (best_tac (!claset addSIs [disjI2]
paulson@2516
   209
                      addSDs [impOfSubs Fake_parts_insert]
paulson@2516
   210
                      addIs  [analz_insertI]
paulson@2516
   211
                      addDs  [impOfSubs analz_subset_parts]
paulson@2516
   212
                      addss (!simpset)) 2);
paulson@2318
   213
(*Base*)
paulson@2318
   214
by (fast_tac (!claset addss (!simpset)) 1);
paulson@2536
   215
qed "B_trusts_NS1";
paulson@2318
   216
paulson@2318
   217
paulson@2318
   218
paulson@2318
   219
(**** Authenticity properties obtained from NS2 ****)
paulson@2318
   220
paulson@2480
   221
(*Unicity for NS2: nonce NB identifies nonce NA and agents A, B 
paulson@2318
   222
  [unicity of B makes Lowe's fix work]
paulson@2318
   223
  [proof closely follows that for unique_NA] *)
paulson@2318
   224
goal thy 
paulson@2536
   225
 "!!evs. [| Nonce NB ~: analz (sees lost Spy evs);  evs : ns_public |]      \
paulson@2536
   226
\ ==> EX A' NA' B'. ALL A NA B.                                             \
paulson@2536
   227
\      Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}                       \
paulson@2536
   228
\        : parts (sees lost Spy evs)  -->  A=A' & NA=NA' & B=B'";
paulson@2536
   229
by (etac rev_mp 1);
paulson@2418
   230
by (analz_induct_tac 1);
paulson@2318
   231
(*NS2*)
paulson@2497
   232
by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
paulson@2318
   233
by (expand_case_tac "NB = ?y" 3 THEN
paulson@2497
   234
    REPEAT (fast_tac (!claset addSEs partsEs) 3));
paulson@2318
   235
(*Base*)
paulson@2318
   236
by (fast_tac (!claset addss (!simpset)) 1);
paulson@2318
   237
(*Fake*)
paulson@2497
   238
by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1);
paulson@2374
   239
by (step_tac (!claset addSIs [analz_insertI]) 1);
paulson@2318
   240
by (ex_strip_tac 1);
paulson@2318
   241
by (best_tac (!claset delrules [conjI]
paulson@2516
   242
                      addSDs [impOfSubs Fake_parts_insert]
paulson@2516
   243
                      addDs  [impOfSubs analz_subset_parts] 
paulson@2516
   244
                      addss (!simpset)) 1);
paulson@2318
   245
val lemma = result();
paulson@2318
   246
paulson@2318
   247
goal thy 
paulson@2318
   248
 "!!evs. [| Crypt(pubK A)  {|Nonce NA, Nonce NB, Agent B|}   \
paulson@2318
   249
\             : parts(sees lost Spy evs);                    \
paulson@2318
   250
\           Crypt(pubK A') {|Nonce NA', Nonce NB, Agent B'|} \
paulson@2318
   251
\             : parts(sees lost Spy evs);                    \
paulson@2318
   252
\           Nonce NB ~: analz (sees lost Spy evs);           \
paulson@2318
   253
\           evs : ns_public |]                               \
paulson@2318
   254
\        ==> A=A' & NA=NA' & B=B'";
paulson@2418
   255
by (prove_unique_tac lemma 1);
paulson@2318
   256
qed "unique_NB";
paulson@2318
   257
paulson@2318
   258
paulson@2318
   259
(*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*)
paulson@2318
   260
goal thy 
paulson@2536
   261
 "!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
paulson@2536
   262
\             : set_of_list evs;                                      \
paulson@2536
   263
\           A ~: lost;  B ~: lost;  evs : ns_public |]                \
paulson@2536
   264
\ ==> Nonce NB ~: analz (sees lost Spy evs)";
paulson@2536
   265
by (etac rev_mp 1);
paulson@2418
   266
by (analz_induct_tac 1);
paulson@2318
   267
(*NS3*)
paulson@2318
   268
by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
paulson@2318
   269
                      addDs  [unique_NB]) 4);
paulson@2318
   270
(*NS1*)
paulson@2536
   271
by (fast_tac (!claset addSEs sees_Spy_partsEs) 2);
paulson@2318
   272
(*Fake*)
paulson@2497
   273
by (spy_analz_tac 1);
paulson@2318
   274
(*NS2*)
paulson@2318
   275
by (Step_tac 1);
paulson@2536
   276
by (fast_tac (!claset addSEs sees_Spy_partsEs) 3);
paulson@2497
   277
by (best_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
paulson@2497
   278
                      addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 2);
paulson@2497
   279
by (fast_tac (!claset addIs  [impOfSubs analz_subset_parts]) 1);
paulson@2536
   280
qed "Spy_not_see_NB";
paulson@2318
   281
paulson@2318
   282
paulson@2318
   283
(*Matches only NS2, not NS1 (or NS3)*)
paulson@2318
   284
val Says_imp_sees_Spy'' = 
paulson@2318
   285
    read_instantiate [("X","Crypt ?K {|?XX,?YY,?ZZ|}")] Says_imp_sees_Spy';
paulson@2318
   286
paulson@2318
   287
paulson@2318
   288
(*Authentication for B: if he receives message 3 and has used NB
paulson@2318
   289
  in message 2, then A has sent message 3.*)
paulson@2318
   290
goal thy 
paulson@2536
   291
 "!!evs. [| Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
paulson@2536
   292
\             : set_of_list evs;                                       \
paulson@2536
   293
\           Says A' B (Crypt (pubK B) (Nonce NB)): set_of_list evs;    \
paulson@2536
   294
\           A ~: lost;  B ~: lost;  evs : ns_public |]                 \
paulson@2536
   295
\        ==> Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list evs";
paulson@2536
   296
by (etac rev_mp 1);
paulson@2536
   297
(*prepare induction over Crypt (pubK B) NB : parts H*)
paulson@2536
   298
by (etac (Says_imp_sees_Spy' RS parts.Inj RS rev_mp) 1);
paulson@2318
   299
by (etac ns_public.induct 1);
paulson@2318
   300
by (ALLGOALS Asm_simp_tac);
paulson@2318
   301
(*NS1*)
paulson@2536
   302
by (fast_tac (!claset addSEs sees_Spy_partsEs) 2);
paulson@2318
   303
(*Fake*)
paulson@2318
   304
by (REPEAT_FIRST (resolve_tac [impI, conjI]));
paulson@2318
   305
by (fast_tac (!claset addss (!simpset)) 1);
paulson@2318
   306
by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
paulson@2318
   307
by (best_tac (!claset addSIs [disjI2]
paulson@2516
   308
                      addSDs [impOfSubs Fake_parts_insert]
paulson@2516
   309
                      addDs  [impOfSubs analz_subset_parts] 
paulson@2516
   310
                      addss (!simpset)) 1);
paulson@2318
   311
(*NS3*)
paulson@2318
   312
by (Step_tac 1);
paulson@2318
   313
by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
paulson@2318
   314
by (best_tac (!claset addSDs [Says_imp_sees_Spy'' RS parts.Inj]
paulson@2516
   315
                      addDs  [unique_NB]) 1);
paulson@2318
   316
qed "B_trusts_NS3";
paulson@2318
   317
paulson@2318
   318
paulson@2318
   319
(**** Overall guarantee for B*)
paulson@2318
   320
paulson@2318
   321
(*If B receives NS3 and the nonce NB agrees with the nonce he joined with
paulson@2536
   322
  NA, then A initiated the run using NA.  SAME proof as B_trusts_NS3!*)
paulson@2318
   323
goal thy 
paulson@2536
   324
 "!!evs. [| Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
paulson@2536
   325
\             : set_of_list evs;                                       \
paulson@2536
   326
\           Says A' B (Crypt (pubK B) (Nonce NB)): set_of_list evs;    \
paulson@2536
   327
\           A ~: lost;  B ~: lost;  evs : ns_public |]                 \
paulson@2536
   328
\    ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs";
paulson@2536
   329
by (etac rev_mp 1);
paulson@2536
   330
(*prepare induction over Crypt (pubK B) {|NB|} : parts H*)
paulson@2536
   331
by (etac (Says_imp_sees_Spy' RS parts.Inj RS rev_mp) 1);
paulson@2318
   332
by (etac ns_public.induct 1);
paulson@2318
   333
by (ALLGOALS Asm_simp_tac);
paulson@2318
   334
(*Fake, NS2, NS3*)
paulson@2318
   335
(*NS1*)
paulson@2536
   336
by (fast_tac (!claset addSEs sees_Spy_partsEs) 2);
paulson@2318
   337
(*Fake*)
paulson@2318
   338
by (REPEAT_FIRST (resolve_tac [impI, conjI]));
paulson@2318
   339
by (fast_tac (!claset addss (!simpset)) 1);
paulson@2318
   340
by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
paulson@2318
   341
by (best_tac (!claset addSIs [disjI2]
paulson@2516
   342
                      addDs [impOfSubs analz_subset_parts,
paulson@2516
   343
                             impOfSubs Fake_parts_insert]
paulson@2516
   344
                      addss (!simpset)) 1);
paulson@2318
   345
(*NS3*)
paulson@2318
   346
by (Step_tac 1);
paulson@2318
   347
by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
paulson@2318
   348
by (best_tac (!claset addSDs [Says_imp_sees_Spy'' RS parts.Inj]
paulson@2516
   349
                      addDs  [unique_NB]) 1);
paulson@2536
   350
qed "B_trusts_protocol";
paulson@2318
   351