src/HOL/Auth/NS_Public.ML
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 5434 9b4bed3f394c
child 8054 2ce57ef2a4aa
permissions -rw-r--r--
tidied; added lemma restrict_to_left
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@4470
    10
AddEs spies_partsEs;
paulson@4470
    11
AddDs [impOfSubs analz_subset_parts];
paulson@4470
    12
AddDs [impOfSubs Fake_parts_insert];
paulson@4470
    13
paulson@3683
    14
AddIffs [Spy_in_bad];
paulson@2318
    15
paulson@2318
    16
(*A "possibility property": there are traces that reach the end*)
paulson@5434
    17
Goal
paulson@5434
    18
   "EX NB. EX evs: ns_public. Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
paulson@2318
    19
by (REPEAT (resolve_tac [exI,bexI] 1));
paulson@2318
    20
by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2);
paulson@2516
    21
by possibility_tac;
paulson@2318
    22
result();
paulson@2318
    23
paulson@2318
    24
paulson@2318
    25
(**** Inductive proofs about ns_public ****)
paulson@2318
    26
paulson@3519
    27
(*Induction for regularity theorems.  If induction formula has the form
paulson@3683
    28
   X ~: analz (spies evs) --> ... then it shortens the proof by discarding
paulson@3683
    29
   needless information about analz (insert X (spies evs))  *)
paulson@3519
    30
fun parts_induct_tac i = 
paulson@3519
    31
    etac ns_public.induct i
paulson@3519
    32
    THEN 
paulson@3519
    33
    REPEAT (FIRSTGOAL analz_mono_contra_tac)
paulson@3519
    34
    THEN 
paulson@3519
    35
    prove_simple_subgoals_tac i;
paulson@3519
    36
paulson@3519
    37
paulson@3683
    38
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
paulson@2318
    39
    sends messages containing X! **)
paulson@2318
    40
paulson@3683
    41
(*Spy never sees another agent's private key! (unless it's bad at start)*)
paulson@5114
    42
Goal "evs: ns_public ==> (Key (priK A) : parts (spies evs)) = (A : bad)";
paulson@3519
    43
by (parts_induct_tac 1);
paulson@4470
    44
by (Blast_tac 1);
paulson@2318
    45
qed "Spy_see_priK";
paulson@2318
    46
Addsimps [Spy_see_priK];
paulson@2318
    47
paulson@5114
    48
Goal "evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
paulson@4477
    49
by Auto_tac;
paulson@2318
    50
qed "Spy_analz_priK";
paulson@2318
    51
Addsimps [Spy_analz_priK];
paulson@2318
    52
paulson@4470
    53
AddSDs [Spy_see_priK RSN (2, rev_iffD1), 
paulson@4470
    54
	Spy_analz_priK RSN (2, rev_iffD1)];
paulson@2318
    55
paulson@2318
    56
paulson@3519
    57
(**** Authenticity properties obtained from NS2 ****)
paulson@3519
    58
paulson@3519
    59
(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
paulson@3519
    60
  is secret.  (Honest users generate fresh nonces.)*)
paulson@5114
    61
Goal "[| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \
paulson@5114
    62
\        Nonce NA ~: analz (spies evs);   evs : ns_public |]       \
paulson@3683
    63
\ ==> Crypt (pubK C) {|NA', Nonce NA, Agent D|} ~: parts (spies evs)";
paulson@3519
    64
by (etac rev_mp 1);
paulson@3519
    65
by (etac rev_mp 1);
paulson@3519
    66
by (parts_induct_tac 1);
paulson@4470
    67
by (ALLGOALS Blast_tac);
paulson@3519
    68
qed "no_nonce_NS1_NS2";
paulson@3519
    69
paulson@4470
    70
(*Adding it to the claset slows down proofs...*)
paulson@4470
    71
val nonce_NS1_NS2_E = no_nonce_NS1_NS2 RSN (2, rev_notE);
paulson@4470
    72
paulson@3519
    73
paulson@3519
    74
(*Unicity for NS1: nonce NA identifies agents A and B*)
paulson@5114
    75
Goal "[| Nonce NA ~: analz (spies evs);  evs : ns_public |]      \
paulson@3709
    76
\ ==> EX A' B'. ALL A B.                                            \
paulson@5114
    77
\   Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs) --> \
paulson@5114
    78
\   A=A' & B=B'";
paulson@3519
    79
by (etac rev_mp 1);
paulson@3519
    80
by (parts_induct_tac 1);
paulson@4556
    81
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
paulson@3519
    82
(*NS1*)
paulson@4470
    83
by (expand_case_tac "NA = ?y" 2 THEN Blast_tac 2);
paulson@3519
    84
(*Fake*)
paulson@3709
    85
by (Clarify_tac 1);
paulson@4470
    86
by (Blast_tac 1);
paulson@3519
    87
val lemma = result();
paulson@3519
    88
paulson@5114
    89
Goal "[| Crypt(pubK B)  {|Nonce NA, Agent A|}  : parts(spies evs); \
paulson@5114
    90
\        Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies evs); \
paulson@5114
    91
\        Nonce NA ~: analz (spies evs);                            \
paulson@5114
    92
\        evs : ns_public |]                                        \
paulson@5114
    93
\     ==> A=A' & B=B'";
paulson@3519
    94
by (prove_unique_tac lemma 1);
paulson@3519
    95
qed "unique_NA";
paulson@3519
    96
paulson@3519
    97
paulson@3519
    98
(*Tactic for proving secrecy theorems*)
nipkow@4686
    99
fun analz_induct_tac i =
paulson@3121
   100
    etac ns_public.induct i   THEN
nipkow@4686
   101
    ALLGOALS Asm_simp_tac;
paulson@2318
   102
paulson@2318
   103
paulson@2318
   104
(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
paulson@5114
   105
Goal "[| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs;   \
paulson@5114
   106
\        A ~: bad;  B ~: bad;  evs : ns_public |]                    \
paulson@5114
   107
\     ==>  Nonce NA ~: analz (spies evs)";
paulson@2536
   108
by (etac rev_mp 1);
paulson@2418
   109
by (analz_induct_tac 1);
paulson@2318
   110
(*NS3*)
paulson@4470
   111
by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 4);
paulson@2536
   112
(*NS2*)
paulson@4470
   113
by (blast_tac (claset() addDs [unique_NA]) 3);
paulson@2318
   114
(*NS1*)
paulson@4470
   115
by (Blast_tac 2);
paulson@2318
   116
(*Fake*)
paulson@2497
   117
by (spy_analz_tac 1);
paulson@2536
   118
qed "Spy_not_see_NA";
paulson@2318
   119
paulson@2318
   120
paulson@2318
   121
(*Authentication for A: if she receives message 2 and has used NA
paulson@2318
   122
  to start a run, then B has sent message 2.*)
paulson@5114
   123
Goal "[| Says A  B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs;  \
paulson@5114
   124
\        Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|})   \
paulson@5114
   125
\          : set evs;                                                \
paulson@5114
   126
\        A ~: bad;  B ~: bad;  evs : ns_public |]                    \
paulson@5114
   127
\     ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|})   \
paulson@5114
   128
\           : set evs";
paulson@2536
   129
by (etac rev_mp 1);
paulson@2536
   130
(*prepare induction over Crypt (pubK A) {|NA,NB,B|} : parts H*)
paulson@3683
   131
by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
paulson@2318
   132
by (etac ns_public.induct 1);
paulson@2318
   133
by (ALLGOALS Asm_simp_tac);
paulson@2318
   134
(*NS1*)
paulson@4470
   135
by (Blast_tac 2);
paulson@2318
   136
(*Fake*)
paulson@4422
   137
by (blast_tac (claset() addDs [Spy_not_see_NA]) 1);
paulson@2318
   138
qed "A_trusts_NS2";
paulson@2318
   139
paulson@4556
   140
paulson@2318
   141
(*If the encrypted message appears then it originated with Alice in NS1*)
paulson@5114
   142
Goal "[| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \
paulson@5114
   143
\        Nonce NA ~: analz (spies evs);                            \
paulson@5114
   144
\        evs : ns_public |]                                        \
paulson@5114
   145
\==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs";
paulson@2536
   146
by (etac rev_mp 1);
paulson@2536
   147
by (etac rev_mp 1);
paulson@3519
   148
by (parts_induct_tac 1);
paulson@4470
   149
by (Blast_tac 1);
paulson@2536
   150
qed "B_trusts_NS1";
paulson@2318
   151
paulson@2318
   152
paulson@2318
   153
paulson@2318
   154
(**** Authenticity properties obtained from NS2 ****)
paulson@2318
   155
paulson@2480
   156
(*Unicity for NS2: nonce NB identifies nonce NA and agents A, B 
paulson@2318
   157
  [unicity of B makes Lowe's fix work]
paulson@2318
   158
  [proof closely follows that for unique_NA] *)
paulson@5114
   159
Goal "[| Nonce NB ~: analz (spies evs);  evs : ns_public |]            \
paulson@3709
   160
\ ==> EX A' NA' B'. ALL A NA B.                                           \
paulson@5114
   161
\   Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|} : parts (spies evs) \
paulson@5114
   162
\      -->  A=A' & NA=NA' & B=B'";
paulson@2536
   163
by (etac rev_mp 1);
paulson@3519
   164
by (parts_induct_tac 1);
paulson@4556
   165
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
paulson@2318
   166
(*NS2*)
paulson@4470
   167
by (expand_case_tac "NB = ?y" 2 THEN Blast_tac 2);
paulson@2318
   168
(*Fake*)
paulson@3709
   169
by (Clarify_tac 1);
paulson@4470
   170
by (Blast_tac 1);
paulson@2318
   171
val lemma = result();
paulson@2318
   172
paulson@5114
   173
Goal "[| Crypt(pubK A)  {|Nonce NA, Nonce NB, Agent B|}   \
paulson@5114
   174
\          : parts(spies evs);                            \
paulson@5114
   175
\        Crypt(pubK A') {|Nonce NA', Nonce NB, Agent B'|} \
paulson@5114
   176
\          : parts(spies evs);                            \
paulson@5114
   177
\        Nonce NB ~: analz (spies evs);                   \
paulson@5114
   178
\        evs : ns_public |]                               \
paulson@5114
   179
\     ==> A=A' & NA=NA' & B=B'";
paulson@2418
   180
by (prove_unique_tac lemma 1);
paulson@2318
   181
qed "unique_NB";
paulson@2318
   182
paulson@4470
   183
AddDs [unique_NB];
paulson@4470
   184
paulson@2318
   185
paulson@2318
   186
(*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*)
paulson@5114
   187
Goal "[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
paulson@5114
   188
\          : set evs;                                              \
paulson@5114
   189
\        A ~: bad;  B ~: bad;  evs : ns_public |]                \
paulson@3683
   190
\ ==> Nonce NB ~: analz (spies evs)";
paulson@2536
   191
by (etac rev_mp 1);
paulson@2418
   192
by (analz_induct_tac 1);
paulson@2318
   193
(*NS3*)
paulson@4470
   194
by (Blast_tac 4);
paulson@3709
   195
(*NS2: by freshness and unicity of NB*)
paulson@4470
   196
by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 3);
paulson@2318
   197
(*NS1*)
paulson@4470
   198
by (Blast_tac 2);
paulson@2318
   199
(*Fake*)
paulson@2497
   200
by (spy_analz_tac 1);
paulson@2536
   201
qed "Spy_not_see_NB";
paulson@2318
   202
paulson@4422
   203
AddDs [Spy_not_see_NB];
paulson@4422
   204
paulson@2318
   205
paulson@2318
   206
(*Authentication for B: if he receives message 3 and has used NB
paulson@2318
   207
  in message 2, then A has sent message 3.*)
paulson@5114
   208
Goal "[| Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
paulson@5114
   209
\          : set evs;                                               \
paulson@5114
   210
\        Says A' B (Crypt (pubK B) (Nonce NB)): set evs;            \
paulson@5114
   211
\        A ~: bad;  B ~: bad;  evs : ns_public |]                   \
paulson@5114
   212
\     ==> Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
paulson@2536
   213
by (etac rev_mp 1);
paulson@2536
   214
(*prepare induction over Crypt (pubK B) NB : parts H*)
paulson@3683
   215
by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
paulson@3519
   216
by (parts_induct_tac 1);
paulson@3709
   217
by (ALLGOALS Clarify_tac);
paulson@4470
   218
by (ALLGOALS Blast_tac);
paulson@2318
   219
qed "B_trusts_NS3";
paulson@2318
   220
paulson@2318
   221
paulson@2318
   222
(**** Overall guarantee for B*)
paulson@2318
   223
paulson@3121
   224
(*Matches only NS2, not NS1 (or NS3)*)
paulson@3683
   225
val Says_imp_spies' = 
paulson@3683
   226
    read_instantiate [("X","Crypt ?K {|?XX,?YY,?ZZ|}")] Says_imp_spies;
paulson@3121
   227
paulson@3121
   228
paulson@2318
   229
(*If B receives NS3 and the nonce NB agrees with the nonce he joined with
paulson@2536
   230
  NA, then A initiated the run using NA.  SAME proof as B_trusts_NS3!*)
paulson@5114
   231
Goal "[| Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
paulson@5114
   232
\          : set evs;                                               \
paulson@5114
   233
\        Says A' B (Crypt (pubK B) (Nonce NB)): set evs;            \
paulson@5114
   234
\        A ~: bad;  B ~: bad;  evs : ns_public |]                 \
paulson@5114
   235
\ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs";
paulson@2536
   236
by (etac rev_mp 1);
paulson@2536
   237
(*prepare induction over Crypt (pubK B) {|NB|} : parts H*)
paulson@3683
   238
by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
paulson@2318
   239
by (etac ns_public.induct 1);
paulson@2318
   240
by (ALLGOALS Asm_simp_tac);
paulson@3709
   241
by (ALLGOALS Clarify_tac);
paulson@4470
   242
(*NS3 holds because NB determines A and NA*)
paulson@4470
   243
by (ALLGOALS Blast_tac);
paulson@2536
   244
qed "B_trusts_protocol";
paulson@2318
   245