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