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