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