src/HOL/UNITY/Simple/NSP_Bad.ML
author paulson
Sat Feb 08 16:05:33 2003 +0100 (2003-02-08)
changeset 13812 91713a1915ee
parent 13797 baefae13ad37
permissions -rw-r--r--
converting HOL/UNITY to use unconditional fairness
     1 (*  Title:      HOL/Auth/NSP_Bad
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol.
     7 Flawed version, vulnerable to Lowe's attack.
     8 
     9 From page 260 of
    10   Burrows, Abadi and Needham.  A Logic of Authentication.
    11   Proc. Royal Soc. 426 (1989)
    12 *)
    13 
    14 fun impOfAlways th =
    15   ObjectLogic.rulify (th RS Always_includes_reachable RS subsetD RS CollectD);
    16 
    17 AddEs spies_partsEs;
    18 AddDs [impOfSubs analz_subset_parts];
    19 AddDs [impOfSubs Fake_parts_insert];
    20 
    21 (*For other theories, e.g. Mutex and Lift, using AddIffs slows proofs down.
    22   Here, it facilitates re-use of the Auth proofs.*)
    23 
    24 AddIffs (map simp_of_act [Fake_def, NS1_def, NS2_def, NS3_def]);
    25 Addsimps [Nprg_def RS def_prg_Init];
    26 
    27 
    28 (*A "possibility property": there are traces that reach the end.
    29   Replace by LEADSTO proof!*)
    30 Goal "A ~= B ==> EX NB. EX s: reachable Nprg.                \
    31 \                  Says A B (Crypt (pubK B) (Nonce NB)) : set s";
    32 by (REPEAT (resolve_tac [exI,bexI] 1));
    33 by (res_inst_tac [("act", "totalize_act NS3")] reachable_Acts 2);
    34 by (res_inst_tac [("act", "totalize_act NS2")] reachable_Acts 3);
    35 by (res_inst_tac [("act", "totalize_act NS1")] reachable_Acts 4);
    36 by (rtac reachable_Init 5);
    37 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Nprg_def, totalize_act_def])));
    38   (*Now ignore the possibility of identity transitions*)
    39 by (REPEAT_FIRST (resolve_tac [disjI1, exI]));
    40 by possibility_tac;
    41 result();
    42 
    43 
    44 (**** Inductive proofs about ns_public ****)
    45 
    46 (*can be used to simulate analz_mono_contra_tac
    47 val analz_impI = read_instantiate_sg (sign_of thy)
    48                 [("P", "?Y ~: analz (spies ?evs)")] impI;
    49 
    50 val spies_Says_analz_contraD = 
    51     spies_subset_spies_Says RS analz_mono RS contra_subsetD;
    52 
    53 by (rtac analz_impI 2);
    54 by (auto_tac (claset() addSDs [spies_Says_analz_contraD], simpset()));
    55 *)
    56 
    57 val [prem] = 
    58 Goal "(!!act s s'. [| act: {Id, Fake, NS1, NS2, NS3};  \
    59 \                     (s,s') \\<in> act;  s \\<in> A |] ==> s': A')  \
    60 \     ==> Nprg \\<in> A co A'";
    61 by (asm_full_simp_tac (simpset() addsimps [Nprg_def, mk_total_program_def]) 1);
    62 by (rtac constrainsI 1); 
    63 by (rtac prem 1); 
    64 by Auto_tac; 
    65 qed "ns_constrainsI";
    66 
    67 
    68 fun ns_constrains_tac i = 
    69    SELECT_GOAL
    70       (EVERY [REPEAT (etac Always_ConstrainsI 1),
    71 	      REPEAT (resolve_tac [StableI, stableI,
    72 				   constrains_imp_Constrains] 1),
    73 	      rtac ns_constrainsI 1,
    74 	      Full_simp_tac 1,
    75 	      REPEAT (FIRSTGOAL (etac disjE)),
    76 	      ALLGOALS (clarify_tac (claset() delrules [impI,impCE])),
    77 	      REPEAT (FIRSTGOAL analz_mono_contra_tac),
    78 	      ALLGOALS Asm_simp_tac]) i;
    79 
    80 (*Tactic for proving secrecy theorems*)
    81 val ns_induct_tac = 
    82   (SELECT_GOAL o EVERY)
    83      [rtac AlwaysI 1,
    84       Force_tac 1,
    85       (*"reachable" gets in here*)
    86       rtac (Always_reachable RS Always_ConstrainsI RS StableI) 1,
    87       ns_constrains_tac 1];
    88 
    89 
    90 (** Theorems of the form X ~: parts (spies evs) imply that NOBODY
    91     sends messages containing X! **)
    92 
    93 (*Spy never sees another agent's private key! (unless it's bad at start)*)
    94 Goal "Nprg : Always {s. (Key (priK A) : parts (spies s)) = (A : bad)}";
    95 by (ns_induct_tac 1);
    96 by (Blast_tac 1);
    97 qed "Spy_see_priK";
    98 Addsimps [impOfAlways Spy_see_priK];
    99 
   100 Goal "Nprg : Always {s. (Key (priK A) : analz (spies s)) = (A : bad)}";
   101 by (rtac (Always_reachable RS Always_weaken) 1);
   102 by Auto_tac;
   103 qed "Spy_analz_priK";
   104 Addsimps [impOfAlways Spy_analz_priK];
   105 
   106 (**
   107 AddSDs [Spy_see_priK RSN (2, rev_iffD1), 
   108 	Spy_analz_priK RSN (2, rev_iffD1)];
   109 **)
   110 
   111 
   112 (**** Authenticity properties obtained from NS2 ****)
   113 
   114 (*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
   115   is secret.  (Honest users generate fresh nonces.)*)
   116 Goal
   117  "Nprg \
   118 \  : Always {s. Nonce NA ~: analz (spies s) -->  \
   119 \               Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies s) --> \
   120 \               Crypt (pubK C) {|NA', Nonce NA|} ~: parts (spies s)}";
   121 by (ns_induct_tac 1);
   122 by (ALLGOALS Blast_tac);
   123 qed "no_nonce_NS1_NS2";
   124 
   125 (*Adding it to the claset slows down proofs...*)
   126 val nonce_NS1_NS2_E = impOfAlways no_nonce_NS1_NS2 RSN (2, rev_notE);
   127 
   128 
   129 (*Unicity for NS1: nonce NA identifies agents A and B*)
   130 Goal "Nprg \
   131 \  : Always {s. Nonce NA ~: analz (spies s) --> \
   132 \               Crypt(pubK B) {|Nonce NA, Agent A|} : parts(spies s) --> \
   133 \               Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies s) --> \
   134 \               A=A' & B=B'}";
   135 by (ns_induct_tac 1);
   136 by Auto_tac;  
   137 (*Fake, NS1 are non-trivial*)
   138 val unique_NA_lemma = result();
   139 
   140 (*Unicity for NS1: nonce NA identifies agents A and B*)
   141 Goal "[| Crypt(pubK B)  {|Nonce NA, Agent A|}  : parts(spies s); \
   142 \        Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies s); \
   143 \        Nonce NA ~: analz (spies s);                            \
   144 \        s : reachable Nprg |]                                   \
   145 \     ==> A=A' & B=B'";
   146 by (blast_tac (claset() addDs [impOfAlways unique_NA_lemma]) 1); 
   147 qed "unique_NA";
   148 
   149 
   150 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
   151 Goal "[| A ~: bad;  B ~: bad |]                     \
   152 \ ==> Nprg : Always \
   153 \             {s. Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set s \
   154 \                 --> Nonce NA ~: analz (spies s)}";
   155 by (ns_induct_tac 1);
   156 (*NS3*)
   157 by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 4);
   158 (*NS2*)
   159 by (blast_tac (claset() addDs [unique_NA]) 3);
   160 (*NS1*)
   161 by (Blast_tac 2);
   162 (*Fake*)
   163 by (spy_analz_tac 1);
   164 qed "Spy_not_see_NA";
   165 
   166 
   167 (*Authentication for A: if she receives message 2 and has used NA
   168   to start a run, then B has sent message 2.*)
   169 val prems =
   170 goal thy "[| A ~: bad;  B ~: bad |]                     \
   171 \ ==> Nprg : Always \
   172 \             {s. Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set s &  \
   173 \                 Crypt(pubK A) {|Nonce NA, Nonce NB|} : parts (knows Spy s) \
   174 \        --> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set s}";
   175   (*insert an invariant for use in some of the subgoals*)
   176 by (cut_facts_tac ([prems MRS Spy_not_see_NA] @ prems) 1);
   177 by (ns_induct_tac 1);
   178 by (ALLGOALS Clarify_tac);
   179 (*NS2*)
   180 by (blast_tac (claset() addDs [unique_NA]) 3);
   181 (*NS1*)
   182 by (Blast_tac 2);
   183 (*Fake*)
   184 by (Blast_tac 1);
   185 qed "A_trusts_NS2";
   186 
   187 
   188 (*If the encrypted message appears then it originated with Alice in NS1*)
   189 Goal "Nprg : Always \
   190 \             {s. Nonce NA ~: analz (spies s) --> \
   191 \                 Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies s) \
   192 \        --> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set s}";
   193 by (ns_induct_tac 1);
   194 by (Blast_tac 1);
   195 qed "B_trusts_NS1";
   196 
   197 
   198 
   199 (**** Authenticity properties obtained from NS2 ****)
   200 
   201 (*Unicity for NS2: nonce NB identifies nonce NA and agent A
   202   [proof closely follows that for unique_NA] *)
   203 Goal
   204  "Nprg \
   205 \  : Always {s. Nonce NB ~: analz (spies s)  --> \
   206 \               Crypt (pubK A) {|Nonce NA, Nonce NB|} : parts (spies s) -->  \
   207 \               Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(spies s) -->  \
   208 \               A=A' & NA=NA'}";
   209 by (ns_induct_tac 1);
   210 by Auto_tac;  
   211 (*Fake, NS2 are non-trivial*)
   212 val unique_NB_lemma = result();
   213 
   214 Goal "[| Crypt(pubK A) {|Nonce NA, Nonce NB|}  : parts(spies s); \
   215 \        Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(spies s); \
   216 \        Nonce NB ~: analz (spies s);                            \
   217 \        s : reachable Nprg |]                                        \
   218 \     ==> A=A' & NA=NA'";
   219 by (blast_tac (claset() addDs [impOfAlways unique_NB_lemma]) 1); 
   220 qed "unique_NB";
   221 
   222 
   223 (*NB remains secret PROVIDED Alice never responds with round 3*)
   224 Goal "[| A ~: bad;  B ~: bad |]                     \
   225 \ ==> Nprg : Always \
   226 \             {s. Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set s &  \
   227 \                 (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set s) \
   228 \                 --> Nonce NB ~: analz (spies s)}";
   229 by (ns_induct_tac 1);
   230 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
   231 by (ALLGOALS Clarify_tac);
   232 (*NS3: because NB determines A*)
   233 by (blast_tac (claset() addDs [unique_NB]) 4);
   234 (*NS2: by freshness and unicity of NB*)
   235 by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 3);
   236 (*NS1: by freshness*)
   237 by (Blast_tac 2);
   238 (*Fake*)
   239 by (spy_analz_tac 1);
   240 qed "Spy_not_see_NB";
   241 
   242 
   243 
   244 (*Authentication for B: if he receives message 3 and has used NB
   245   in message 2, then A has sent message 3--to somebody....*)
   246 val prems =
   247 goal thy "[| A ~: bad;  B ~: bad |]                     \
   248 \ ==> Nprg : Always \
   249 \             {s. Crypt (pubK B) (Nonce NB) : parts (spies s) &  \
   250 \                 Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set s \
   251 \                 --> (EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set s)}";
   252   (*insert an invariant for use in some of the subgoals*)
   253 by (cut_facts_tac ([prems MRS Spy_not_see_NB] @ prems) 1);
   254 by (ns_induct_tac 1);
   255 by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
   256 by (ALLGOALS Clarify_tac);
   257 (*NS3: because NB determines A (this use of unique_NB is more robust) *)
   258 by (blast_tac (claset() addIs [unique_NB RS conjunct1]) 3);
   259 (*NS1: by freshness*)
   260 by (Blast_tac 2);
   261 (*Fake*)
   262 by (Blast_tac 1);
   263 qed "B_trusts_NS3";
   264 
   265 
   266 (*Can we strengthen the secrecy theorem?  NO*)
   267 Goal "[| A ~: bad;  B ~: bad |]                     \
   268 \ ==> Nprg : Always \
   269 \             {s. Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set s  \
   270 \                 --> Nonce NB ~: analz (spies s)}";
   271 by (ns_induct_tac 1);
   272 by (ALLGOALS Clarify_tac);
   273 (*NS2: by freshness and unicity of NB*)
   274 by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 3);
   275 (*NS1: by freshness*)
   276 by (Blast_tac 2);
   277 (*Fake*)
   278 by (spy_analz_tac 1);
   279 (*NS3: unicity of NB identifies A and NA, but not B*)
   280 by (forw_inst_tac [("A'","A")] (Says_imp_spies RS parts.Inj RS unique_NB) 1
   281     THEN REPEAT (eresolve_tac [asm_rl, Says_imp_spies RS parts.Inj] 1));
   282 by Auto_tac;
   283 by (rename_tac "s B' C" 1);
   284 
   285 (*
   286 THIS IS THE ATTACK!
   287 [| A ~: bad; B ~: bad |]
   288 ==> Nprg
   289     : Always
   290        {s. Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set s -->
   291            Nonce NB ~: analz (knows Spy s)}
   292  1. !!s B' C.
   293        [| A ~: bad; B ~: bad; s : reachable Nprg;
   294           Says A C (Crypt (pubK C) {|Nonce NA, Agent A|}) : set s;
   295           Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set s;
   296           C : bad; Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set s;
   297           Nonce NB ~: analz (knows Spy s) |]
   298        ==> False
   299 *)