src/HOL/Auth/NS_Public.ML
author paulson
Tue Nov 11 11:16:18 1997 +0100 (1997-11-11)
changeset 4198 c63639beeff1
parent 4197 1547bc6daa5a
child 4422 21238c9d363e
permissions -rw-r--r--
Fixed spelling error
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
paulson@3683
    15
AddIffs [Spy_in_bad];
paulson@2318
    16
paulson@2318
    17
(*A "possibility property": there are traces that reach the end*)
paulson@2318
    18
goal thy 
paulson@2318
    19
 "!!A B. A ~= B ==> EX NB. EX evs: ns_public.               \
nipkow@3465
    20
\                     Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
paulson@2318
    21
by (REPEAT (resolve_tac [exI,bexI] 1));
paulson@2318
    22
by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2);
paulson@2516
    23
by possibility_tac;
paulson@2318
    24
result();
paulson@2318
    25
paulson@2318
    26
paulson@2318
    27
(**** Inductive proofs about ns_public ****)
paulson@2318
    28
paulson@2318
    29
(*Nobody sends themselves messages*)
nipkow@3465
    30
goal thy "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set evs";
paulson@2318
    31
by (etac ns_public.induct 1);
paulson@2318
    32
by (Auto_tac());
paulson@2318
    33
qed_spec_mp "not_Says_to_self";
paulson@2318
    34
Addsimps [not_Says_to_self];
paulson@2318
    35
AddSEs   [not_Says_to_self RSN (2, rev_notE)];
paulson@2318
    36
paulson@2318
    37
paulson@3519
    38
(*Induction for regularity theorems.  If induction formula has the form
paulson@3683
    39
   X ~: analz (spies evs) --> ... then it shortens the proof by discarding
paulson@3683
    40
   needless information about analz (insert X (spies evs))  *)
paulson@3519
    41
fun parts_induct_tac i = 
paulson@3519
    42
    etac ns_public.induct i
paulson@3519
    43
    THEN 
paulson@3519
    44
    REPEAT (FIRSTGOAL analz_mono_contra_tac)
paulson@3519
    45
    THEN 
paulson@3519
    46
    prove_simple_subgoals_tac i;
paulson@3519
    47
paulson@3519
    48
paulson@3683
    49
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
paulson@2318
    50
    sends messages containing X! **)
paulson@2318
    51
paulson@3683
    52
(*Spy never sees another agent's private key! (unless it's bad at start)*)
paulson@2318
    53
goal thy 
paulson@3683
    54
 "!!A. evs: ns_public ==> (Key (priK A) : parts (spies evs)) = (A : bad)";
paulson@3519
    55
by (parts_induct_tac 1);
paulson@3121
    56
by (Fake_parts_insert_tac 1);
paulson@2318
    57
qed "Spy_see_priK";
paulson@2318
    58
Addsimps [Spy_see_priK];
paulson@2318
    59
paulson@2318
    60
goal thy 
paulson@3683
    61
 "!!A. evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
wenzelm@4091
    62
by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
paulson@2318
    63
qed "Spy_analz_priK";
paulson@2318
    64
Addsimps [Spy_analz_priK];
paulson@2318
    65
paulson@3683
    66
goal thy  "!!A. [| Key (priK A) : parts (spies evs);       \
paulson@3683
    67
\                  evs : ns_public |] ==> A:bad";
wenzelm@4091
    68
by (blast_tac (claset() addDs [Spy_see_priK]) 1);
paulson@2318
    69
qed "Spy_see_priK_D";
paulson@2318
    70
paulson@2318
    71
bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D);
paulson@2318
    72
AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
paulson@2318
    73
paulson@2318
    74
paulson@3519
    75
(**** Authenticity properties obtained from NS2 ****)
paulson@3519
    76
paulson@3519
    77
(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
paulson@3519
    78
  is secret.  (Honest users generate fresh nonces.)*)
paulson@3519
    79
goal thy 
paulson@3683
    80
 "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \
paulson@3683
    81
\           Nonce NA ~: analz (spies evs);       \
paulson@3519
    82
\           evs : ns_public |]                      \
paulson@3683
    83
\ ==> Crypt (pubK C) {|NA', Nonce NA, Agent D|} ~: parts (spies evs)";
paulson@3519
    84
by (etac rev_mp 1);
paulson@3519
    85
by (etac rev_mp 1);
paulson@3519
    86
by (parts_induct_tac 1);
paulson@3519
    87
(*NS3*)
wenzelm@4091
    88
by (blast_tac (claset() addSEs partsEs) 3);
paulson@3519
    89
(*NS2*)
wenzelm@4091
    90
by (blast_tac (claset() addSEs partsEs) 2);
paulson@3519
    91
by (Fake_parts_insert_tac 1);
paulson@3519
    92
qed "no_nonce_NS1_NS2";
paulson@3519
    93
paulson@3519
    94
paulson@3519
    95
(*Unicity for NS1: nonce NA identifies agents A and B*)
paulson@3519
    96
goal thy 
paulson@3683
    97
 "!!evs. [| Nonce NA ~: analz (spies evs);  evs : ns_public |]      \
paulson@3709
    98
\ ==> EX A' B'. ALL A B.                                            \
paulson@3683
    99
\      Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs) --> \
paulson@3519
   100
\      A=A' & B=B'";
paulson@3519
   101
by (etac rev_mp 1);
paulson@3519
   102
by (parts_induct_tac 1);
paulson@3519
   103
by (ALLGOALS
wenzelm@4091
   104
    (asm_simp_tac (simpset() addsimps [all_conj_distrib, parts_insert_spies])));
paulson@3519
   105
(*NS1*)
wenzelm@4091
   106
by (expand_case_tac "NA = ?y" 2 THEN blast_tac (claset() addSEs partsEs) 2);
paulson@3519
   107
(*Fake*)
paulson@3709
   108
by (Clarify_tac 1);
paulson@3519
   109
by (ex_strip_tac 1);
paulson@3519
   110
by (Fake_parts_insert_tac 1);
paulson@3519
   111
val lemma = result();
paulson@3519
   112
paulson@3519
   113
goal thy 
paulson@3683
   114
 "!!evs. [| Crypt(pubK B)  {|Nonce NA, Agent A|}  : parts(spies evs); \
paulson@3683
   115
\           Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies evs); \
paulson@3683
   116
\           Nonce NA ~: analz (spies evs);                            \
paulson@3683
   117
\           evs : ns_public |]                                        \
paulson@3519
   118
\        ==> A=A' & B=B'";
paulson@3519
   119
by (prove_unique_tac lemma 1);
paulson@3519
   120
qed "unique_NA";
paulson@3519
   121
paulson@3519
   122
paulson@3519
   123
(*Tactic for proving secrecy theorems*)
paulson@2418
   124
fun analz_induct_tac i = 
paulson@3121
   125
    etac ns_public.induct i   THEN
paulson@2418
   126
    ALLGOALS (asm_simp_tac 
wenzelm@4091
   127
              (simpset() addsplits [expand_if]));
paulson@2318
   128
paulson@2318
   129
paulson@2318
   130
(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
paulson@2318
   131
goal thy 
paulson@3466
   132
 "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs;         \
paulson@3683
   133
\           A ~: bad;  B ~: bad;  evs : ns_public |]                        \
paulson@3683
   134
\        ==>  Nonce NA ~: analz (spies evs)";
paulson@2536
   135
by (etac rev_mp 1);
paulson@2418
   136
by (analz_induct_tac 1);
paulson@2318
   137
(*NS3*)
wenzelm@4091
   138
by (blast_tac (claset() addDs  [Says_imp_spies RS parts.Inj]
paulson@3121
   139
                       addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
paulson@2536
   140
(*NS2*)
wenzelm@4091
   141
by (blast_tac (claset() addSEs [MPair_parts]
paulson@3683
   142
		       addDs  [Says_imp_spies RS parts.Inj,
paulson@3121
   143
			       parts.Body, unique_NA]) 3);
paulson@2318
   144
(*NS1*)
wenzelm@4091
   145
by (blast_tac (claset() addSEs spies_partsEs
paulson@3519
   146
                       addIs  [impOfSubs analz_subset_parts]) 2);
paulson@2318
   147
(*Fake*)
paulson@2497
   148
by (spy_analz_tac 1);
paulson@2536
   149
qed "Spy_not_see_NA";
paulson@2318
   150
paulson@2318
   151
paulson@2318
   152
(*Authentication for A: if she receives message 2 and has used NA
paulson@2318
   153
  to start a run, then B has sent message 2.*)
paulson@2318
   154
goal thy 
paulson@3519
   155
 "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;  \
paulson@3519
   156
\           Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|})   \
paulson@3519
   157
\             : set evs;                                                \
paulson@3683
   158
\           A ~: bad;  B ~: bad;  evs : ns_public |]                  \
paulson@3519
   159
\        ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|})   \
nipkow@3465
   160
\              : set evs";
paulson@2536
   161
by (etac rev_mp 1);
paulson@2536
   162
(*prepare induction over Crypt (pubK A) {|NA,NB,B|} : parts H*)
paulson@3683
   163
by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
paulson@2318
   164
by (etac ns_public.induct 1);
paulson@2318
   165
by (ALLGOALS Asm_simp_tac);
paulson@2318
   166
(*NS1*)
wenzelm@4091
   167
by (blast_tac (claset() addSEs spies_partsEs) 2);
paulson@2318
   168
(*Fake*)
wenzelm@4091
   169
by (blast_tac (claset() addSDs [impOfSubs Fake_parts_insert]
paulson@3121
   170
                       addDs  [Spy_not_see_NA, 
paulson@3121
   171
			       impOfSubs analz_subset_parts]) 1);
paulson@2318
   172
qed "A_trusts_NS2";
paulson@2318
   173
paulson@2318
   174
(*If the encrypted message appears then it originated with Alice in NS1*)
paulson@2318
   175
goal thy 
paulson@3683
   176
 "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \
paulson@3683
   177
\           Nonce NA ~: analz (spies evs);                 \
paulson@3683
   178
\           evs : ns_public |]                             \
nipkow@3465
   179
\   ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs";
paulson@2536
   180
by (etac rev_mp 1);
paulson@2536
   181
by (etac rev_mp 1);
paulson@3519
   182
by (parts_induct_tac 1);
paulson@3519
   183
by (Fake_parts_insert_tac 1);
paulson@2536
   184
qed "B_trusts_NS1";
paulson@2318
   185
paulson@2318
   186
paulson@2318
   187
paulson@2318
   188
(**** Authenticity properties obtained from NS2 ****)
paulson@2318
   189
paulson@2480
   190
(*Unicity for NS2: nonce NB identifies nonce NA and agents A, B 
paulson@2318
   191
  [unicity of B makes Lowe's fix work]
paulson@2318
   192
  [proof closely follows that for unique_NA] *)
paulson@2318
   193
goal thy 
paulson@3709
   194
 "!!evs. [| Nonce NB ~: analz (spies evs);  evs : ns_public |]            \
paulson@3709
   195
\ ==> EX A' NA' B'. ALL A NA B.                                           \
paulson@3683
   196
\      Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|} : parts (spies evs) \
paulson@3683
   197
\         -->  A=A' & NA=NA' & B=B'";
paulson@2536
   198
by (etac rev_mp 1);
paulson@3519
   199
by (parts_induct_tac 1);
paulson@3519
   200
by (ALLGOALS
wenzelm@4091
   201
    (asm_simp_tac (simpset() addsimps [all_conj_distrib, parts_insert_spies])));
paulson@2318
   202
(*NS2*)
wenzelm@4091
   203
by (expand_case_tac "NB = ?y" 2 THEN blast_tac (claset() addSEs partsEs) 2);
paulson@2318
   204
(*Fake*)
paulson@3709
   205
by (Clarify_tac 1);
paulson@2318
   206
by (ex_strip_tac 1);
paulson@3519
   207
by (Fake_parts_insert_tac 1);
paulson@2318
   208
val lemma = result();
paulson@2318
   209
paulson@2318
   210
goal thy 
paulson@2318
   211
 "!!evs. [| Crypt(pubK A)  {|Nonce NA, Nonce NB, Agent B|}   \
paulson@3709
   212
\             : parts(spies evs);                            \
paulson@2318
   213
\           Crypt(pubK A') {|Nonce NA', Nonce NB, Agent B'|} \
paulson@3709
   214
\             : parts(spies evs);                            \
paulson@3709
   215
\           Nonce NB ~: analz (spies evs);                   \
paulson@2318
   216
\           evs : ns_public |]                               \
paulson@2318
   217
\        ==> A=A' & NA=NA' & B=B'";
paulson@2418
   218
by (prove_unique_tac lemma 1);
paulson@2318
   219
qed "unique_NB";
paulson@2318
   220
paulson@2318
   221
paulson@2318
   222
(*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*)
paulson@2318
   223
goal thy 
paulson@2536
   224
 "!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
paulson@3466
   225
\             : set evs;                                              \
paulson@3683
   226
\           A ~: bad;  B ~: bad;  evs : ns_public |]                \
paulson@3683
   227
\ ==> Nonce NB ~: analz (spies evs)";
paulson@2536
   228
by (etac rev_mp 1);
paulson@2418
   229
by (analz_induct_tac 1);
paulson@2318
   230
(*NS3*)
wenzelm@4091
   231
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, unique_NB]) 4);
paulson@3709
   232
(*NS2: by freshness and unicity of NB*)
wenzelm@4091
   233
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj]
paulson@3709
   234
                       addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]
paulson@3709
   235
                       addEs partsEs
paulson@3709
   236
		       addIs [impOfSubs analz_subset_parts]) 3);
paulson@2318
   237
(*NS1*)
wenzelm@4091
   238
by (blast_tac (claset() addSEs spies_partsEs) 2);
paulson@2318
   239
(*Fake*)
paulson@2497
   240
by (spy_analz_tac 1);
paulson@2536
   241
qed "Spy_not_see_NB";
paulson@2318
   242
paulson@2318
   243
paulson@2318
   244
(*Authentication for B: if he receives message 3 and has used NB
paulson@2318
   245
  in message 2, then A has sent message 3.*)
paulson@2318
   246
goal thy 
paulson@2536
   247
 "!!evs. [| Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
paulson@3466
   248
\             : set evs;                                               \
paulson@3466
   249
\           Says A' B (Crypt (pubK B) (Nonce NB)): set evs;            \
paulson@4197
   250
\           A ~: bad;  B ~: bad;  evs : ns_public |]                   \
nipkow@3465
   251
\        ==> Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
paulson@2536
   252
by (etac rev_mp 1);
paulson@2536
   253
(*prepare induction over Crypt (pubK B) NB : parts H*)
paulson@3683
   254
by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
paulson@3519
   255
by (parts_induct_tac 1);
paulson@3709
   256
by (ALLGOALS Clarify_tac);
paulson@4197
   257
(*NS3: because NB determines A (this use of unique_NB is more robust) *)
paulson@4197
   258
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, Spy_not_see_NB]
paulson@4197
   259
			addIs [unique_NB RS conjunct1]) 3);
paulson@3709
   260
(*NS1: by freshness*)
wenzelm@4091
   261
by (blast_tac (claset() addSEs spies_partsEs) 2);
paulson@2318
   262
(*Fake*)
wenzelm@4091
   263
by (blast_tac (claset() addSDs [impOfSubs Fake_parts_insert]
paulson@4197
   264
                        addDs  [Spy_not_see_NB, 
paulson@4197
   265
			        impOfSubs analz_subset_parts]) 1);
paulson@2318
   266
qed "B_trusts_NS3";
paulson@2318
   267
paulson@2318
   268
paulson@2318
   269
(**** Overall guarantee for B*)
paulson@2318
   270
paulson@3121
   271
(*Matches only NS2, not NS1 (or NS3)*)
paulson@3683
   272
val Says_imp_spies' = 
paulson@3683
   273
    read_instantiate [("X","Crypt ?K {|?XX,?YY,?ZZ|}")] Says_imp_spies;
paulson@3121
   274
paulson@3121
   275
paulson@2318
   276
(*If B receives NS3 and the nonce NB agrees with the nonce he joined with
paulson@2536
   277
  NA, then A initiated the run using NA.  SAME proof as B_trusts_NS3!*)
paulson@2318
   278
goal thy 
paulson@2536
   279
 "!!evs. [| Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
paulson@3466
   280
\             : set evs;                                               \
paulson@3466
   281
\           Says A' B (Crypt (pubK B) (Nonce NB)): set evs;            \
paulson@3683
   282
\           A ~: bad;  B ~: bad;  evs : ns_public |]                 \
nipkow@3465
   283
\    ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs";
paulson@2536
   284
by (etac rev_mp 1);
paulson@2536
   285
(*prepare induction over Crypt (pubK B) {|NB|} : parts H*)
paulson@3683
   286
by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
paulson@2318
   287
by (etac ns_public.induct 1);
paulson@2318
   288
by (ALLGOALS Asm_simp_tac);
paulson@3709
   289
by (ALLGOALS Clarify_tac);
paulson@4197
   290
(*NS3: because NB determines A and NA*)
wenzelm@4091
   291
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, 
paulson@4197
   292
                               Spy_not_see_NB, unique_NB]) 3);
paulson@2318
   293
(*NS1*)
wenzelm@4091
   294
by (blast_tac (claset() addSEs spies_partsEs) 2);
paulson@2318
   295
(*Fake*)
wenzelm@4091
   296
by (blast_tac (claset() addSDs [impOfSubs Fake_parts_insert]
paulson@4197
   297
                        addDs  [Spy_not_see_NB, 
paulson@4197
   298
			        impOfSubs analz_subset_parts]) 1);
paulson@2536
   299
qed "B_trusts_protocol";
paulson@2318
   300