src/HOL/Auth/NS_Shared.ML
author paulson
Fri Jul 04 17:34:55 1997 +0200 (1997-07-04)
changeset 3500 0d8ad2f192d8
parent 3466 30791e5a69c4
child 3516 470626799511
permissions -rw-r--r--
New constant "certificate"--just an abbreviation
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
paulson@1943
    15
proof_timing:=true;
paulson@1997
    16
HOL_quantifiers := false;
paulson@1997
    17
paulson@3121
    18
(*Replacing the variable by a constant improves search speed by 50%!*)
paulson@3121
    19
val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy;
paulson@3121
    20
paulson@1997
    21
paulson@2323
    22
(*A "possibility property": there are traces that reach the end*)
paulson@1997
    23
goal thy 
paulson@3466
    24
 "!!A B. [| A ~= B; A ~= Server; B ~= Server |]       \
paulson@2032
    25
\        ==> EX N K. EX evs: ns_shared lost.          \
nipkow@3465
    26
\               Says A B (Crypt K {|Nonce N, Nonce N|}) : set evs";
paulson@1997
    27
by (REPEAT (resolve_tac [exI,bexI] 1));
paulson@2516
    28
by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS 
paulson@2516
    29
          ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2);
paulson@2516
    30
by possibility_tac;
paulson@2015
    31
result();
paulson@2015
    32
paulson@1943
    33
paulson@1934
    34
(**** Inductive proofs about ns_shared ****)
paulson@1934
    35
paulson@2103
    36
(*Monotonicity*)
paulson@2032
    37
goal thy "!!evs. lost' <= lost ==> ns_shared lost' <= ns_shared lost";
paulson@2032
    38
by (rtac subsetI 1);
paulson@2032
    39
by (etac ns_shared.induct 1);
paulson@2032
    40
by (REPEAT_FIRST
paulson@3466
    41
    (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
paulson@2032
    42
                              :: ns_shared.intrs))));
paulson@2032
    43
qed "ns_shared_mono";
paulson@2032
    44
paulson@2032
    45
paulson@1934
    46
(*Nobody sends themselves messages*)
nipkow@3465
    47
goal thy "!!evs. evs : ns_shared lost ==> ALL A X. Says A A X ~: set evs";
paulson@2032
    48
by (etac ns_shared.induct 1);
paulson@1934
    49
by (Auto_tac());
paulson@1934
    50
qed_spec_mp "not_Says_to_self";
paulson@1934
    51
Addsimps [not_Says_to_self];
paulson@1934
    52
AddSEs   [not_Says_to_self RSN (2, rev_notE)];
paulson@1934
    53
paulson@1943
    54
(*For reasoning about the encrypted portion of message NS3*)
nipkow@3465
    55
goal thy "!!evs. Says S A (Crypt KA {|N, B, K, X|}) : set evs \
paulson@2131
    56
\                ==> X : parts (sees lost Spy evs)";
paulson@3121
    57
by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
paulson@2032
    58
qed "NS3_msg_in_parts_sees_Spy";
paulson@2032
    59
                              
paulson@2070
    60
goal thy
nipkow@3465
    61
    "!!evs. Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set evs \
paulson@2131
    62
\           ==> K : parts (sees lost Spy evs)";
paulson@3121
    63
by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
paulson@2131
    64
qed "Oops_parts_sees_Spy";
paulson@2070
    65
paulson@3121
    66
(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
paulson@3121
    67
  We instantiate the variable to "lost" since leaving it as a Var would
paulson@3121
    68
  interfere with simplification.*)
paulson@3121
    69
val parts_induct_tac = 
paulson@3121
    70
    etac ns_shared.induct 1  THEN 
paulson@3121
    71
    dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5  THEN
paulson@3121
    72
    forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 8  THEN
paulson@3121
    73
    prove_simple_subgoals_tac 1;
paulson@2070
    74
paulson@1934
    75
paulson@2032
    76
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
paulson@2015
    77
    sends messages containing X! **)
paulson@1934
    78
paulson@2131
    79
(*Spy never sees another agent's shared key! (unless it's lost at start)*)
paulson@1934
    80
goal thy 
paulson@2131
    81
 "!!evs. evs : ns_shared lost \
paulson@2131
    82
\        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
paulson@3121
    83
by parts_induct_tac;
paulson@3121
    84
by (Fake_parts_insert_tac 1);
paulson@3121
    85
by (Blast_tac 1);
paulson@2131
    86
qed "Spy_see_shrK";
paulson@2131
    87
Addsimps [Spy_see_shrK];
paulson@1934
    88
paulson@2131
    89
goal thy 
paulson@2131
    90
 "!!evs. evs : ns_shared lost \
paulson@2131
    91
\        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
paulson@2131
    92
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
paulson@2131
    93
qed "Spy_analz_shrK";
paulson@2131
    94
Addsimps [Spy_analz_shrK];
paulson@1934
    95
paulson@2131
    96
goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
paulson@2131
    97
\                  evs : ns_shared lost |] ==> A:lost";
paulson@3121
    98
by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
paulson@2131
    99
qed "Spy_see_shrK_D";
paulson@1934
   100
paulson@2131
   101
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
paulson@2131
   102
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
paulson@1934
   103
paulson@2070
   104
paulson@2516
   105
(*Nobody can have used non-existent keys!*)
paulson@2160
   106
goal thy "!!evs. evs : ns_shared lost ==>      \
paulson@2516
   107
\         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
paulson@3121
   108
by parts_induct_tac;
paulson@2516
   109
(*Fake*)
paulson@2516
   110
by (best_tac
paulson@2516
   111
      (!claset addIs [impOfSubs analz_subset_parts]
paulson@2516
   112
               addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
paulson@2516
   113
                      impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
paulson@3121
   114
               addss (!simpset)) 1);
paulson@2516
   115
(*NS2, NS4, NS5*)
paulson@3121
   116
by (ALLGOALS (blast_tac (!claset addSEs sees_Spy_partsEs)));
paulson@2160
   117
qed_spec_mp "new_keys_not_used";
paulson@1934
   118
paulson@1934
   119
bind_thm ("new_keys_not_analzd",
paulson@2032
   120
          [analz_subset_parts RS keysFor_mono,
paulson@2032
   121
           new_keys_not_used] MRS contra_subsetD);
paulson@1934
   122
paulson@1934
   123
Addsimps [new_keys_not_used, new_keys_not_analzd];
paulson@1934
   124
paulson@1934
   125
paulson@1934
   126
(** Lemmas concerning the form of items passed in messages **)
paulson@1934
   127
paulson@2015
   128
(*Describes the form of K, X and K' when the Server sends this message.*)
paulson@1934
   129
goal thy 
paulson@2516
   130
 "!!evs. [| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) \
paulson@3466
   131
\             : set evs;                                      \
paulson@2516
   132
\           evs : ns_shared lost |]                           \
paulson@2516
   133
\        ==> K ~: range shrK &                                \
paulson@2516
   134
\            X = (Crypt (shrK B) {|Key K, Agent A|}) &        \
paulson@2516
   135
\            K' = shrK A";
paulson@2032
   136
by (etac rev_mp 1);
paulson@2032
   137
by (etac ns_shared.induct 1);
paulson@2516
   138
by (Auto_tac());
paulson@1934
   139
qed "Says_Server_message_form";
paulson@1934
   140
paulson@1934
   141
paulson@2070
   142
(*If the encrypted message appears then it originated with the Server*)
paulson@1934
   143
goal thy
paulson@2284
   144
 "!!evs. [| Crypt (shrK A) {|NA, Agent B, Key K, X|}                   \
paulson@2070
   145
\            : parts (sees lost Spy evs);                              \
paulson@2070
   146
\           A ~: lost;  evs : ns_shared lost |]                        \
paulson@2284
   147
\         ==> X = (Crypt (shrK B) {|Key K, Agent A|}) &                \
paulson@2070
   148
\             Says Server A                                            \
paulson@2284
   149
\              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
paulson@2284
   150
\                                Crypt (shrK B) {|Key K, Agent A|}|})  \
nipkow@3465
   151
\             : set evs";
paulson@2070
   152
by (etac rev_mp 1);
paulson@3121
   153
by parts_induct_tac;
paulson@3121
   154
by (Fake_parts_insert_tac 1);
paulson@2015
   155
by (Auto_tac());
paulson@2323
   156
qed "A_trusts_NS2";
paulson@1934
   157
paulson@1965
   158
paulson@1965
   159
(*EITHER describes the form of X when the following message is sent, 
paulson@1965
   160
  OR     reduces it to the Fake case.
paulson@1965
   161
  Use Says_Server_message_form if applicable.*)
paulson@1934
   162
goal thy 
paulson@2284
   163
 "!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})      \
paulson@3466
   164
\            : set evs;          evs : ns_shared lost |]                   \
paulson@3121
   165
\        ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|}))   \
paulson@2516
   166
\            | X : analz (sees lost Spy evs)";
paulson@2103
   167
by (case_tac "A : lost" 1);
paulson@3121
   168
by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]
paulson@3121
   169
                      addss (!simpset)) 1);
paulson@2070
   170
by (forward_tac [Says_imp_sees_Spy RS parts.Inj] 1);
paulson@3121
   171
by (blast_tac (!claset addEs  partsEs
paulson@3121
   172
                      addSDs [A_trusts_NS2, Says_Server_message_form]) 1);
paulson@1934
   173
qed "Says_S_message_form";
paulson@1934
   174
paulson@1934
   175
paulson@2131
   176
(*For proofs involving analz.  We again instantiate the variable to "lost".*)
paulson@3121
   177
val analz_sees_tac = 
paulson@2131
   178
    forw_inst_tac [("lost","lost")] Says_Server_message_form 8 THEN
paulson@2131
   179
    forw_inst_tac [("lost","lost")] Says_S_message_form 5 THEN 
paulson@2516
   180
    REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac);
paulson@2131
   181
paulson@1934
   182
paulson@1934
   183
(****
paulson@1934
   184
 The following is to prove theorems of the form
paulson@1934
   185
paulson@2516
   186
  Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
paulson@2451
   187
  Key K : analz (sees lost Spy evs)
paulson@1934
   188
paulson@1934
   189
 A more general formula must be proved inductively.
paulson@1934
   190
paulson@1934
   191
****)
paulson@1934
   192
paulson@1934
   193
paulson@1934
   194
(*NOT useful in this form, but it says that session keys are not used
paulson@1934
   195
  to encrypt messages containing other keys, in the actual protocol.
paulson@1934
   196
  We require that agents should behave like this subsequently also.*)
paulson@1934
   197
goal thy 
paulson@3466
   198
 "!!evs. [| evs : ns_shared lost;  Kab ~: range shrK |] ==>  \
paulson@3466
   199
\           (Crypt KAB X) : parts (sees lost Spy evs) &      \
paulson@3466
   200
\           Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
paulson@3121
   201
by parts_induct_tac;
paulson@1934
   202
(*Deals with Faked messages*)
paulson@3121
   203
by (blast_tac (!claset addSEs partsEs
paulson@3121
   204
                       addDs [impOfSubs parts_insert_subset_Un]) 1);
paulson@1965
   205
(*Base, NS4 and NS5*)
paulson@3121
   206
by (Auto_tac());
paulson@1934
   207
result();
paulson@1934
   208
paulson@1934
   209
paulson@1934
   210
(** Session keys are not used to encrypt other session keys **)
paulson@1934
   211
paulson@2015
   212
(*The equality makes the induction hypothesis easier to apply*)
paulson@1934
   213
goal thy  
paulson@3466
   214
 "!!evs. evs : ns_shared lost ==>                                \
paulson@3466
   215
\  ALL K KK. KK <= Compl (range shrK) -->                        \
paulson@3466
   216
\            (Key K : analz (Key``KK Un (sees lost Spy evs))) =  \
paulson@2516
   217
\            (K : KK | Key K : analz (sees lost Spy evs))";
paulson@2032
   218
by (etac ns_shared.induct 1);
paulson@3121
   219
by analz_sees_tac;
paulson@2516
   220
by (REPEAT_FIRST (resolve_tac [allI, impI]));
paulson@2516
   221
by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
paulson@2516
   222
(*Takes 24 secs*)
paulson@2516
   223
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
paulson@3451
   224
(*Fake*) 
paulson@3451
   225
by (spy_analz_tac 2);
paulson@2516
   226
(*Base*)
paulson@3121
   227
by (Blast_tac 1);
paulson@2516
   228
qed_spec_mp "analz_image_freshK";
paulson@1934
   229
paulson@1934
   230
paulson@1934
   231
goal thy
paulson@2516
   232
 "!!evs. [| evs : ns_shared lost;  KAB ~: range shrK |] ==>     \
paulson@2516
   233
\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
paulson@2516
   234
\        (K = KAB | Key K : analz (sees lost Spy evs))";
paulson@2516
   235
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
paulson@2516
   236
qed "analz_insert_freshK";
paulson@1934
   237
paulson@1934
   238
paulson@2558
   239
(** The session key K uniquely identifies the message **)
paulson@1965
   240
paulson@1934
   241
goal thy 
paulson@2451
   242
 "!!evs. evs : ns_shared lost ==>                                        \
paulson@2451
   243
\      EX A' NA' B' X'. ALL A NA B X.                                    \
paulson@2284
   244
\       Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})         \
paulson@3466
   245
\       : set evs -->         A=A' & NA=NA' & B=B' & X=X'";
paulson@2032
   246
by (etac ns_shared.induct 1);
paulson@2070
   247
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
paulson@2131
   248
by (Step_tac 1);
paulson@2070
   249
(*NS3*)
paulson@2070
   250
by (ex_strip_tac 2);
paulson@3121
   251
by (Blast_tac 2);
paulson@2070
   252
(*NS2: it can't be a new key*)
paulson@2070
   253
by (expand_case_tac "K = ?y" 1);
paulson@2070
   254
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
paulson@3121
   255
by (blast_tac (!claset delrules [conjI]    (*prevent split-up into 4 subgoals*)
paulson@3121
   256
                      addSEs sees_Spy_partsEs) 1);
paulson@1934
   257
val lemma = result();
paulson@1934
   258
paulson@1934
   259
(*In messages of this form, the session key uniquely identifies the rest*)
paulson@1934
   260
goal thy 
paulson@2070
   261
 "!!evs. [| Says Server A                                    \
paulson@2284
   262
\             (Crypt (shrK A) {|NA, Agent B, Key K, X|})     \
paulson@3466
   263
\                  : set evs;                                \ 
paulson@2070
   264
\           Says Server A'                                   \
paulson@2284
   265
\             (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) \
paulson@3466
   266
\                  : set evs;                                \
paulson@2070
   267
\           evs : ns_shared lost |] ==> A=A' & NA=NA' & B=B' & X = X'";
paulson@2451
   268
by (prove_unique_tac lemma 1);
paulson@1934
   269
qed "unique_session_keys";
paulson@1934
   270
paulson@1934
   271
paulson@2032
   272
(** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
paulson@2015
   273
paulson@1934
   274
goal thy 
paulson@2323
   275
 "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_shared lost |]            \
paulson@2015
   276
\        ==> Says Server A                                             \
paulson@2284
   277
\              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
paulson@2284
   278
\                                Crypt (shrK B) {|Key K, Agent A|}|})  \
paulson@3466
   279
\             : set evs -->                                            \
paulson@3466
   280
\        (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs) -->         \
paulson@2050
   281
\        Key K ~: analz (sees lost Spy evs)";
paulson@2032
   282
by (etac ns_shared.induct 1);
paulson@3121
   283
by analz_sees_tac;
paulson@1934
   284
by (ALLGOALS 
paulson@2015
   285
    (asm_simp_tac 
paulson@3451
   286
     (!simpset addsimps ([analz_insert_eq, not_parts_not_analz, 
paulson@3451
   287
			  analz_insert_freshK] @ pushes)
paulson@1934
   288
               setloop split_tac [expand_if])));
paulson@3451
   289
(*Oops*)
paulson@3451
   290
by (blast_tac (!claset addDs [unique_session_keys]) 5);
paulson@3451
   291
(*NS4*) 
paulson@3451
   292
by (Blast_tac 4);
paulson@1934
   293
(*NS2*)
paulson@3121
   294
by (blast_tac (!claset addSEs sees_Spy_partsEs
paulson@3451
   295
                       addIs [parts_insertI, impOfSubs analz_subset_parts]) 2);
paulson@3451
   296
(*Fake*) 
paulson@3451
   297
by (spy_analz_tac 1);
paulson@2529
   298
(*NS3*) (**LEVEL 6 **)
paulson@2070
   299
by (step_tac (!claset delrules [impCE]) 1);
paulson@3121
   300
by (forward_tac [Says_imp_sees_Spy' RS parts.Inj RS A_trusts_NS2] 1);
paulson@2170
   301
by (assume_tac 2);
paulson@3441
   302
by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj RS
paulson@3441
   303
			      Crypt_Spy_analz_lost]) 1);
paulson@3121
   304
by (blast_tac (!claset addDs [unique_session_keys]) 1);
paulson@2070
   305
val lemma = result() RS mp RS mp RSN(2,rev_notE);
paulson@2015
   306
paulson@2015
   307
paulson@2015
   308
(*Final version: Server's message in the most abstract form*)
paulson@2015
   309
goal thy 
paulson@2070
   310
 "!!evs. [| Says Server A                                               \
paulson@3466
   311
\            (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;            \
paulson@3466
   312
\           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs);          \
paulson@2070
   313
\           A ~: lost;  B ~: lost;  evs : ns_shared lost                \
paulson@2516
   314
\        |] ==> Key K ~: analz (sees lost Spy evs)";
paulson@2015
   315
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
paulson@3121
   316
by (blast_tac (!claset addSDs [lemma]) 1);
paulson@2032
   317
qed "Spy_not_see_encrypted_key";
paulson@2032
   318
paulson@2032
   319
paulson@2032
   320
goal thy 
paulson@2070
   321
 "!!evs. [| C ~: {A,B,Server};                                          \
paulson@2070
   322
\           Says Server A                                               \
paulson@3466
   323
\            (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;            \
paulson@3466
   324
\           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs);          \
paulson@2070
   325
\           A ~: lost;  B ~: lost;  evs : ns_shared lost |]             \
paulson@2516
   326
\        ==> Key K ~: analz (sees lost C evs)";
paulson@2032
   327
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
paulson@2032
   328
by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
paulson@2032
   329
by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
paulson@3121
   330
by (REPEAT_FIRST (blast_tac (!claset addIs [ns_shared_mono RS subsetD])));
paulson@2032
   331
qed "Agent_not_see_encrypted_key";
paulson@2070
   332
paulson@2070
   333
paulson@2070
   334
paulson@2070
   335
(**** Guarantees available at various stages of protocol ***)
paulson@2070
   336
paulson@2323
   337
A_trusts_NS2 RS conjunct2 RS Spy_not_see_encrypted_key;
paulson@2070
   338
paulson@2070
   339
paulson@2070
   340
(*If the encrypted message appears then it originated with the Server*)
paulson@2070
   341
goal thy
paulson@2284
   342
 "!!evs. [| Crypt (shrK B) {|Key K, Agent A|} : parts (sees lost Spy evs); \
paulson@2070
   343
\           B ~: lost;  evs : ns_shared lost |]                        \
paulson@2070
   344
\         ==> EX NA. Says Server A                                     \
paulson@2284
   345
\              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
paulson@2284
   346
\                                Crypt (shrK B) {|Key K, Agent A|}|})  \
nipkow@3465
   347
\             : set evs";
paulson@2070
   348
by (etac rev_mp 1);
paulson@3121
   349
by parts_induct_tac;
paulson@3121
   350
by (Fake_parts_insert_tac 1);
paulson@2070
   351
(*Fake case*)
paulson@3121
   352
by (ALLGOALS Blast_tac);
paulson@2323
   353
qed "B_trusts_NS3";
paulson@2070
   354
paulson@2070
   355
paulson@2070
   356
goal thy
paulson@3466
   357
 "!!evs. [| B ~: lost;  evs : ns_shared lost |]                        \
paulson@3466
   358
\        ==> Key K ~: analz (sees lost Spy evs) -->                    \
paulson@2284
   359
\            Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
paulson@3466
   360
\            : set evs -->                                             \
paulson@3466
   361
\            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->        \
nipkow@3465
   362
\            Says B A (Crypt K (Nonce NB)) : set evs";
paulson@2070
   363
by (etac ns_shared.induct 1);
paulson@2070
   364
by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
paulson@3121
   365
by (dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5);
paulson@3121
   366
by (forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 8);
paulson@2103
   367
by (TRYALL (rtac impI));
paulson@2103
   368
by (REPEAT_FIRST
paulson@2103
   369
    (dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD)));
paulson@2103
   370
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
paulson@3121
   371
(**LEVEL 7**)
paulson@3121
   372
by (blast_tac (!claset addSDs [Crypt_Fake_parts_insert]
paulson@3121
   373
                       addDs [impOfSubs analz_subset_parts]) 1);
paulson@3121
   374
by (Blast_tac 2);
paulson@2103
   375
by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac));
paulson@2516
   376
(*Subgoal 1: contradiction from the assumptions  
paulson@2516
   377
  Key K ~: used evsa  and Crypt K (Nonce NB) : parts (sees lost Spy evsa) *)
paulson@2170
   378
by (dtac Crypt_imp_invKey_keysFor 1);
paulson@3121
   379
(**LEVEL 11**)
paulson@2070
   380
by (Asm_full_simp_tac 1);
paulson@2170
   381
by (rtac disjI1 1);
paulson@2070
   382
by (thin_tac "?PP-->?QQ" 1);
paulson@2070
   383
by (case_tac "Ba : lost" 1);
paulson@3121
   384
by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj RS B_trusts_NS3, 
paulson@3121
   385
			      unique_session_keys]) 2);
paulson@3441
   386
by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj RS
paulson@3441
   387
			      Crypt_Spy_analz_lost]) 1);
paulson@2103
   388
val lemma = result();
paulson@2103
   389
paulson@2103
   390
goal thy
paulson@2284
   391
 "!!evs. [| Crypt K (Nonce NB) : parts (sees lost Spy evs);           \
paulson@2284
   392
\           Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
paulson@3466
   393
\           : set evs;                                                \
paulson@3466
   394
\           ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs;          \
paulson@2131
   395
\           A ~: lost;  B ~: lost;  evs : ns_shared lost |]           \
nipkow@3465
   396
\        ==> Says B A (Crypt K (Nonce NB)) : set evs";
paulson@3121
   397
by (blast_tac (!claset addSIs [lemma RS mp RS mp RS mp]
paulson@3121
   398
                       addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1);
paulson@2323
   399
qed "A_trusts_NS4";