conversion of NSP_Bad to Isar script
authorpaulson
Tue Sep 23 15:49:17 2003 +0200 (2003-09-23)
changeset 1420397df98601d23
parent 14202 643fc73e2910
child 14204 2fa6ecb87d47
conversion of NSP_Bad to Isar script
src/HOL/UNITY/ROOT.ML
src/HOL/UNITY/Simple/NSP_Bad.ML
src/HOL/UNITY/Simple/NSP_Bad.thy
     1.1 --- a/src/HOL/UNITY/ROOT.ML	Tue Sep 23 15:44:25 2003 +0200
     1.2 +++ b/src/HOL/UNITY/ROOT.ML	Tue Sep 23 15:49:17 2003 +0200
     1.3 @@ -20,8 +20,9 @@
     1.4  time_use_thy "Simple/Reach";
     1.5  time_use_thy "Simple/Reachability";
     1.6  
     1.7 -with_path "../Auth"  (*to find Public.thy*)
     1.8 -  time_use_thy"Simple/NSP_Bad";
     1.9 +(*Verifying security protocols using UNITY*)
    1.10 +with_path "../Auth" (no_document use_thy) "Public";
    1.11 +with_path "../Auth" time_use_thy "Simple/NSP_Bad";
    1.12  
    1.13  (*Example of composition*)
    1.14  time_use_thy "Comp/Handshake";
     2.1 --- a/src/HOL/UNITY/Simple/NSP_Bad.ML	Tue Sep 23 15:44:25 2003 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,299 +0,0 @@
     2.4 -(*  Title:      HOL/Auth/NSP_Bad
     2.5 -    ID:         $Id$
     2.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 -    Copyright   1996  University of Cambridge
     2.8 -
     2.9 -Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol.
    2.10 -Flawed version, vulnerable to Lowe's attack.
    2.11 -
    2.12 -From page 260 of
    2.13 -  Burrows, Abadi and Needham.  A Logic of Authentication.
    2.14 -  Proc. Royal Soc. 426 (1989)
    2.15 -*)
    2.16 -
    2.17 -fun impOfAlways th =
    2.18 -  ObjectLogic.rulify (th RS Always_includes_reachable RS subsetD RS CollectD);
    2.19 -
    2.20 -AddEs spies_partsEs;
    2.21 -AddDs [impOfSubs analz_subset_parts];
    2.22 -AddDs [impOfSubs Fake_parts_insert];
    2.23 -
    2.24 -(*For other theories, e.g. Mutex and Lift, using AddIffs slows proofs down.
    2.25 -  Here, it facilitates re-use of the Auth proofs.*)
    2.26 -
    2.27 -AddIffs (map simp_of_act [Fake_def, NS1_def, NS2_def, NS3_def]);
    2.28 -Addsimps [Nprg_def RS def_prg_Init];
    2.29 -
    2.30 -
    2.31 -(*A "possibility property": there are traces that reach the end.
    2.32 -  Replace by LEADSTO proof!*)
    2.33 -Goal "A ~= B ==> EX NB. EX s: reachable Nprg.                \
    2.34 -\                  Says A B (Crypt (pubK B) (Nonce NB)) : set s";
    2.35 -by (REPEAT (resolve_tac [exI,bexI] 1));
    2.36 -by (res_inst_tac [("act", "totalize_act NS3")] reachable_Acts 2);
    2.37 -by (res_inst_tac [("act", "totalize_act NS2")] reachable_Acts 3);
    2.38 -by (res_inst_tac [("act", "totalize_act NS1")] reachable_Acts 4);
    2.39 -by (rtac reachable_Init 5);
    2.40 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [Nprg_def, totalize_act_def])));
    2.41 -  (*Now ignore the possibility of identity transitions*)
    2.42 -by (REPEAT_FIRST (resolve_tac [disjI1, exI]));
    2.43 -by possibility_tac;
    2.44 -result();
    2.45 -
    2.46 -
    2.47 -(**** Inductive proofs about ns_public ****)
    2.48 -
    2.49 -(*can be used to simulate analz_mono_contra_tac
    2.50 -val analz_impI = read_instantiate_sg (sign_of thy)
    2.51 -                [("P", "?Y ~: analz (spies ?evs)")] impI;
    2.52 -
    2.53 -val spies_Says_analz_contraD = 
    2.54 -    spies_subset_spies_Says RS analz_mono RS contra_subsetD;
    2.55 -
    2.56 -by (rtac analz_impI 2);
    2.57 -by (auto_tac (claset() addSDs [spies_Says_analz_contraD], simpset()));
    2.58 -*)
    2.59 -
    2.60 -val [prem] = 
    2.61 -Goal "(!!act s s'. [| act: {Id, Fake, NS1, NS2, NS3};  \
    2.62 -\                     (s,s') \\<in> act;  s \\<in> A |] ==> s': A')  \
    2.63 -\     ==> Nprg \\<in> A co A'";
    2.64 -by (asm_full_simp_tac (simpset() addsimps [Nprg_def, mk_total_program_def]) 1);
    2.65 -by (rtac constrainsI 1); 
    2.66 -by (rtac prem 1); 
    2.67 -by Auto_tac; 
    2.68 -qed "ns_constrainsI";
    2.69 -
    2.70 -
    2.71 -fun ns_constrains_tac i = 
    2.72 -   SELECT_GOAL
    2.73 -      (EVERY [REPEAT (etac Always_ConstrainsI 1),
    2.74 -	      REPEAT (resolve_tac [StableI, stableI,
    2.75 -				   constrains_imp_Constrains] 1),
    2.76 -	      rtac ns_constrainsI 1,
    2.77 -	      Full_simp_tac 1,
    2.78 -	      REPEAT (FIRSTGOAL (etac disjE)),
    2.79 -	      ALLGOALS (clarify_tac (claset() delrules [impI,impCE])),
    2.80 -	      REPEAT (FIRSTGOAL analz_mono_contra_tac),
    2.81 -	      ALLGOALS Asm_simp_tac]) i;
    2.82 -
    2.83 -(*Tactic for proving secrecy theorems*)
    2.84 -val ns_induct_tac = 
    2.85 -  (SELECT_GOAL o EVERY)
    2.86 -     [rtac AlwaysI 1,
    2.87 -      Force_tac 1,
    2.88 -      (*"reachable" gets in here*)
    2.89 -      rtac (Always_reachable RS Always_ConstrainsI RS StableI) 1,
    2.90 -      ns_constrains_tac 1];
    2.91 -
    2.92 -
    2.93 -(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
    2.94 -    sends messages containing X! **)
    2.95 -
    2.96 -(*Spy never sees another agent's private key! (unless it's bad at start)*)
    2.97 -Goal "Nprg : Always {s. (Key (priK A) : parts (spies s)) = (A : bad)}";
    2.98 -by (ns_induct_tac 1);
    2.99 -by (Blast_tac 1);
   2.100 -qed "Spy_see_priK";
   2.101 -Addsimps [impOfAlways Spy_see_priK];
   2.102 -
   2.103 -Goal "Nprg : Always {s. (Key (priK A) : analz (spies s)) = (A : bad)}";
   2.104 -by (rtac (Always_reachable RS Always_weaken) 1);
   2.105 -by Auto_tac;
   2.106 -qed "Spy_analz_priK";
   2.107 -Addsimps [impOfAlways Spy_analz_priK];
   2.108 -
   2.109 -(**
   2.110 -AddSDs [Spy_see_priK RSN (2, rev_iffD1), 
   2.111 -	Spy_analz_priK RSN (2, rev_iffD1)];
   2.112 -**)
   2.113 -
   2.114 -
   2.115 -(**** Authenticity properties obtained from NS2 ****)
   2.116 -
   2.117 -(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
   2.118 -  is secret.  (Honest users generate fresh nonces.)*)
   2.119 -Goal
   2.120 - "Nprg \
   2.121 -\  : Always {s. Nonce NA ~: analz (spies s) -->  \
   2.122 -\               Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies s) --> \
   2.123 -\               Crypt (pubK C) {|NA', Nonce NA|} ~: parts (spies s)}";
   2.124 -by (ns_induct_tac 1);
   2.125 -by (ALLGOALS Blast_tac);
   2.126 -qed "no_nonce_NS1_NS2";
   2.127 -
   2.128 -(*Adding it to the claset slows down proofs...*)
   2.129 -val nonce_NS1_NS2_E = impOfAlways no_nonce_NS1_NS2 RSN (2, rev_notE);
   2.130 -
   2.131 -
   2.132 -(*Unicity for NS1: nonce NA identifies agents A and B*)
   2.133 -Goal "Nprg \
   2.134 -\  : Always {s. Nonce NA ~: analz (spies s) --> \
   2.135 -\               Crypt(pubK B) {|Nonce NA, Agent A|} : parts(spies s) --> \
   2.136 -\               Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies s) --> \
   2.137 -\               A=A' & B=B'}";
   2.138 -by (ns_induct_tac 1);
   2.139 -by Auto_tac;  
   2.140 -(*Fake, NS1 are non-trivial*)
   2.141 -val unique_NA_lemma = result();
   2.142 -
   2.143 -(*Unicity for NS1: nonce NA identifies agents A and B*)
   2.144 -Goal "[| Crypt(pubK B)  {|Nonce NA, Agent A|}  : parts(spies s); \
   2.145 -\        Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies s); \
   2.146 -\        Nonce NA ~: analz (spies s);                            \
   2.147 -\        s : reachable Nprg |]                                   \
   2.148 -\     ==> A=A' & B=B'";
   2.149 -by (blast_tac (claset() addDs [impOfAlways unique_NA_lemma]) 1); 
   2.150 -qed "unique_NA";
   2.151 -
   2.152 -
   2.153 -(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
   2.154 -Goal "[| A ~: bad;  B ~: bad |]                     \
   2.155 -\ ==> Nprg : Always \
   2.156 -\             {s. Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set s \
   2.157 -\                 --> Nonce NA ~: analz (spies s)}";
   2.158 -by (ns_induct_tac 1);
   2.159 -(*NS3*)
   2.160 -by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 4);
   2.161 -(*NS2*)
   2.162 -by (blast_tac (claset() addDs [unique_NA]) 3);
   2.163 -(*NS1*)
   2.164 -by (Blast_tac 2);
   2.165 -(*Fake*)
   2.166 -by (spy_analz_tac 1);
   2.167 -qed "Spy_not_see_NA";
   2.168 -
   2.169 -
   2.170 -(*Authentication for A: if she receives message 2 and has used NA
   2.171 -  to start a run, then B has sent message 2.*)
   2.172 -val prems =
   2.173 -goal thy "[| A ~: bad;  B ~: bad |]                     \
   2.174 -\ ==> Nprg : Always \
   2.175 -\             {s. Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set s &  \
   2.176 -\                 Crypt(pubK A) {|Nonce NA, Nonce NB|} : parts (knows Spy s) \
   2.177 -\        --> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set s}";
   2.178 -  (*insert an invariant for use in some of the subgoals*)
   2.179 -by (cut_facts_tac ([prems MRS Spy_not_see_NA] @ prems) 1);
   2.180 -by (ns_induct_tac 1);
   2.181 -by (ALLGOALS Clarify_tac);
   2.182 -(*NS2*)
   2.183 -by (blast_tac (claset() addDs [unique_NA]) 3);
   2.184 -(*NS1*)
   2.185 -by (Blast_tac 2);
   2.186 -(*Fake*)
   2.187 -by (Blast_tac 1);
   2.188 -qed "A_trusts_NS2";
   2.189 -
   2.190 -
   2.191 -(*If the encrypted message appears then it originated with Alice in NS1*)
   2.192 -Goal "Nprg : Always \
   2.193 -\             {s. Nonce NA ~: analz (spies s) --> \
   2.194 -\                 Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies s) \
   2.195 -\        --> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set s}";
   2.196 -by (ns_induct_tac 1);
   2.197 -by (Blast_tac 1);
   2.198 -qed "B_trusts_NS1";
   2.199 -
   2.200 -
   2.201 -
   2.202 -(**** Authenticity properties obtained from NS2 ****)
   2.203 -
   2.204 -(*Unicity for NS2: nonce NB identifies nonce NA and agent A
   2.205 -  [proof closely follows that for unique_NA] *)
   2.206 -Goal
   2.207 - "Nprg \
   2.208 -\  : Always {s. Nonce NB ~: analz (spies s)  --> \
   2.209 -\               Crypt (pubK A) {|Nonce NA, Nonce NB|} : parts (spies s) -->  \
   2.210 -\               Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(spies s) -->  \
   2.211 -\               A=A' & NA=NA'}";
   2.212 -by (ns_induct_tac 1);
   2.213 -by Auto_tac;  
   2.214 -(*Fake, NS2 are non-trivial*)
   2.215 -val unique_NB_lemma = result();
   2.216 -
   2.217 -Goal "[| Crypt(pubK A) {|Nonce NA, Nonce NB|}  : parts(spies s); \
   2.218 -\        Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(spies s); \
   2.219 -\        Nonce NB ~: analz (spies s);                            \
   2.220 -\        s : reachable Nprg |]                                        \
   2.221 -\     ==> A=A' & NA=NA'";
   2.222 -by (blast_tac (claset() addDs [impOfAlways unique_NB_lemma]) 1); 
   2.223 -qed "unique_NB";
   2.224 -
   2.225 -
   2.226 -(*NB remains secret PROVIDED Alice never responds with round 3*)
   2.227 -Goal "[| A ~: bad;  B ~: bad |]                     \
   2.228 -\ ==> Nprg : Always \
   2.229 -\             {s. Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set s &  \
   2.230 -\                 (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set s) \
   2.231 -\                 --> Nonce NB ~: analz (spies s)}";
   2.232 -by (ns_induct_tac 1);
   2.233 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
   2.234 -by (ALLGOALS Clarify_tac);
   2.235 -(*NS3: because NB determines A*)
   2.236 -by (blast_tac (claset() addDs [unique_NB]) 4);
   2.237 -(*NS2: by freshness and unicity of NB*)
   2.238 -by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 3);
   2.239 -(*NS1: by freshness*)
   2.240 -by (Blast_tac 2);
   2.241 -(*Fake*)
   2.242 -by (spy_analz_tac 1);
   2.243 -qed "Spy_not_see_NB";
   2.244 -
   2.245 -
   2.246 -
   2.247 -(*Authentication for B: if he receives message 3 and has used NB
   2.248 -  in message 2, then A has sent message 3--to somebody....*)
   2.249 -val prems =
   2.250 -goal thy "[| A ~: bad;  B ~: bad |]                     \
   2.251 -\ ==> Nprg : Always \
   2.252 -\             {s. Crypt (pubK B) (Nonce NB) : parts (spies s) &  \
   2.253 -\                 Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set s \
   2.254 -\                 --> (EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set s)}";
   2.255 -  (*insert an invariant for use in some of the subgoals*)
   2.256 -by (cut_facts_tac ([prems MRS Spy_not_see_NB] @ prems) 1);
   2.257 -by (ns_induct_tac 1);
   2.258 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
   2.259 -by (ALLGOALS Clarify_tac);
   2.260 -(*NS3: because NB determines A (this use of unique_NB is more robust) *)
   2.261 -by (blast_tac (claset() addIs [unique_NB RS conjunct1]) 3);
   2.262 -(*NS1: by freshness*)
   2.263 -by (Blast_tac 2);
   2.264 -(*Fake*)
   2.265 -by (Blast_tac 1);
   2.266 -qed "B_trusts_NS3";
   2.267 -
   2.268 -
   2.269 -(*Can we strengthen the secrecy theorem?  NO*)
   2.270 -Goal "[| A ~: bad;  B ~: bad |]                     \
   2.271 -\ ==> Nprg : Always \
   2.272 -\             {s. Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set s  \
   2.273 -\                 --> Nonce NB ~: analz (spies s)}";
   2.274 -by (ns_induct_tac 1);
   2.275 -by (ALLGOALS Clarify_tac);
   2.276 -(*NS2: by freshness and unicity of NB*)
   2.277 -by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 3);
   2.278 -(*NS1: by freshness*)
   2.279 -by (Blast_tac 2);
   2.280 -(*Fake*)
   2.281 -by (spy_analz_tac 1);
   2.282 -(*NS3: unicity of NB identifies A and NA, but not B*)
   2.283 -by (forw_inst_tac [("A'","A")] (Says_imp_spies RS parts.Inj RS unique_NB) 1
   2.284 -    THEN REPEAT (eresolve_tac [asm_rl, Says_imp_spies RS parts.Inj] 1));
   2.285 -by Auto_tac;
   2.286 -by (rename_tac "s B' C" 1);
   2.287 -
   2.288 -(*
   2.289 -THIS IS THE ATTACK!
   2.290 -[| A ~: bad; B ~: bad |]
   2.291 -==> Nprg
   2.292 -    : Always
   2.293 -       {s. Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set s -->
   2.294 -           Nonce NB ~: analz (knows Spy s)}
   2.295 - 1. !!s B' C.
   2.296 -       [| A ~: bad; B ~: bad; s : reachable Nprg;
   2.297 -          Says A C (Crypt (pubK C) {|Nonce NA, Agent A|}) : set s;
   2.298 -          Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set s;
   2.299 -          C : bad; Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set s;
   2.300 -          Nonce NB ~: analz (knows Spy s) |]
   2.301 -       ==> False
   2.302 -*)
     3.1 --- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Tue Sep 23 15:44:25 2003 +0200
     3.2 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Tue Sep 23 15:49:17 2003 +0200
     3.3 @@ -3,57 +3,336 @@
     3.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.5      Copyright   1996  University of Cambridge
     3.6  
     3.7 -add_path "../Auth"; use_thy"NSP_Bad";
     3.8 -
     3.9 -Security protocols in UNITY: Needham-Schroeder, public keys (flawed version).
    3.10 +ML{*add_path "$ISABELLE_HOME/src/HOL/Auth"*}
    3.11  
    3.12  Original file is ../Auth/NS_Public_Bad
    3.13  *)
    3.14  
    3.15 -NSP_Bad = Public + UNITY_Main + 
    3.16 +header{*Analyzing the Needham-Schroeder Public-Key Protocol in UNITY*}
    3.17 +
    3.18 +theory NSP_Bad = Public + UNITY_Main:
    3.19  
    3.20 -types state = event list
    3.21 +text{*This is the flawed version, vulnerable to Lowe's attack.
    3.22 +From page 260 of
    3.23 +  Burrows, Abadi and Needham.  A Logic of Authentication.
    3.24 +  Proc. Royal Soc. 426 (1989).
    3.25 +*}
    3.26 +
    3.27 +types state = "event list"
    3.28  
    3.29  constdefs
    3.30 -  
    3.31 +
    3.32    (*The spy MAY say anything he CAN say.  We do not expect him to
    3.33      invent new nonces here, but he can also use NS1.  Common to
    3.34      all similar protocols.*)
    3.35    Fake :: "(state*state) set"
    3.36      "Fake == {(s,s').
    3.37 -	      EX B X. s' = Says Spy B X # s
    3.38 -		    & X: synth (analz (spies s))}"
    3.39 -  
    3.40 +	      \<exists>B X. s' = Says Spy B X # s
    3.41 +		    & X \<in> synth (analz (spies s))}"
    3.42 +
    3.43    (*The numeric suffixes on A identify the rule*)
    3.44  
    3.45    (*Alice initiates a protocol run, sending a nonce to Bob*)
    3.46    NS1 :: "(state*state) set"
    3.47      "NS1 == {(s1,s').
    3.48 -	     EX A1 B NA.
    3.49 +	     \<exists>A1 B NA.
    3.50  	         s' = Says A1 B (Crypt (pubK B) {|Nonce NA, Agent A1|}) # s1
    3.51 -	       & Nonce NA ~: used s1}"
    3.52 -  
    3.53 +	       & Nonce NA \<notin> used s1}"
    3.54 +
    3.55    (*Bob responds to Alice's message with a further nonce*)
    3.56    NS2 :: "(state*state) set"
    3.57      "NS2 == {(s2,s').
    3.58 -	     EX A' A2 B NA NB.
    3.59 +	     \<exists>A' A2 B NA NB.
    3.60  	         s' = Says B A2 (Crypt (pubK A2) {|Nonce NA, Nonce NB|}) # s2
    3.61 -               & Says A' B (Crypt (pubK B) {|Nonce NA, Agent A2|}) : set s2
    3.62 -	       & Nonce NB ~: used s2}"
    3.63 - 
    3.64 +               & Says A' B (Crypt (pubK B) {|Nonce NA, Agent A2|}) \<in> set s2
    3.65 +	       & Nonce NB \<notin> used s2}"
    3.66 +
    3.67    (*Alice proves her existence by sending NB back to Bob.*)
    3.68    NS3 :: "(state*state) set"
    3.69      "NS3 == {(s3,s').
    3.70 -	     EX A3 B' B NA NB.
    3.71 +	     \<exists>A3 B' B NA NB.
    3.72  	         s' = Says A3 B (Crypt (pubK B) (Nonce NB)) # s3
    3.73 -               & Says A3  B (Crypt (pubK B) {|Nonce NA, Agent A3|}) : set s3
    3.74 -	       & Says B' A3 (Crypt (pubK A3) {|Nonce NA, Nonce NB|}) : set s3}"
    3.75 +               & Says A3  B (Crypt (pubK B) {|Nonce NA, Agent A3|}) \<in> set s3
    3.76 +	       & Says B' A3 (Crypt (pubK A3) {|Nonce NA, Nonce NB|}) \<in> set s3}"
    3.77 +
    3.78 +
    3.79 +constdefs
    3.80 +  Nprg :: "state program"
    3.81 +    (*Initial trace is empty*)
    3.82 +    "Nprg == mk_total_program({[]}, {Fake, NS1, NS2, NS3}, UNIV)"
    3.83 +
    3.84 +declare spies_partsEs [elim]
    3.85 +declare analz_into_parts [dest]
    3.86 +declare Fake_parts_insert_in_Un  [dest]
    3.87 +
    3.88 +text{*For other theories, e.g. Mutex and Lift, using [iff] slows proofs down.
    3.89 +  Here, it facilitates re-use of the Auth proofs.*}
    3.90 +
    3.91 +declare Fake_def [THEN def_act_simp, iff]
    3.92 +declare NS1_def [THEN def_act_simp, iff]
    3.93 +declare NS2_def [THEN def_act_simp, iff]
    3.94 +declare NS3_def [THEN def_act_simp, iff]
    3.95 +
    3.96 +declare Nprg_def [THEN def_prg_Init, simp]
    3.97 +
    3.98 +
    3.99 +text{*A "possibility property": there are traces that reach the end.
   3.100 +  Replace by LEADSTO proof!*}
   3.101 +lemma "A \<noteq> B ==>
   3.102 +       \<exists>NB. \<exists>s \<in> reachable Nprg. Says A B (Crypt (pubK B) (Nonce NB)) \<in> set s"
   3.103 +apply (intro exI bexI)
   3.104 +apply (rule_tac [2] act = "totalize_act NS3" in reachable.Acts)
   3.105 +apply (rule_tac [3] act = "totalize_act NS2" in reachable.Acts)
   3.106 +apply (rule_tac [4] act = "totalize_act NS1" in reachable.Acts)
   3.107 +apply (rule_tac [5] reachable.Init)
   3.108 +apply (simp_all (no_asm_simp) add: Nprg_def totalize_act_def)
   3.109 +apply auto
   3.110 +done
   3.111 +
   3.112 +
   3.113 +subsection{*Inductive Proofs about @{term ns_public}*}
   3.114 +
   3.115 +lemma ns_constrainsI:
   3.116 +     "(!!act s s'. [| act \<in> {Id, Fake, NS1, NS2, NS3};
   3.117 +                      (s,s') \<in> act;  s \<in> A |] ==> s' \<in> A')
   3.118 +      ==> Nprg \<in> A co A'"
   3.119 +apply (simp add: Nprg_def mk_total_program_def)
   3.120 +apply (rule constrainsI, auto)
   3.121 +done
   3.122 +
   3.123 +
   3.124 +text{*This ML code does the inductions directly.*}
   3.125 +ML{*
   3.126 +val ns_constrainsI = thm "ns_constrainsI";
   3.127 +
   3.128 +fun ns_constrains_tac(cs,ss) i =
   3.129 +   SELECT_GOAL
   3.130 +      (EVERY [REPEAT (etac Always_ConstrainsI 1),
   3.131 +	      REPEAT (resolve_tac [StableI, stableI,
   3.132 +				   constrains_imp_Constrains] 1),
   3.133 +	      rtac ns_constrainsI 1,
   3.134 +	      full_simp_tac ss 1,
   3.135 +	      REPEAT (FIRSTGOAL (etac disjE)),
   3.136 +	      ALLGOALS (clarify_tac (cs delrules [impI,impCE])),
   3.137 +	      REPEAT (FIRSTGOAL analz_mono_contra_tac),
   3.138 +	      ALLGOALS (asm_simp_tac ss)]) i;
   3.139 +
   3.140 +(*Tactic for proving secrecy theorems*)
   3.141 +fun ns_induct_tac(cs,ss) =
   3.142 +  (SELECT_GOAL o EVERY)
   3.143 +     [rtac AlwaysI 1,
   3.144 +      force_tac (cs,ss) 1,
   3.145 +      (*"reachable" gets in here*)
   3.146 +      rtac (Always_reachable RS Always_ConstrainsI RS StableI) 1,
   3.147 +      ns_constrains_tac(cs,ss) 1];
   3.148 +*}
   3.149 +
   3.150 +method_setup ns_induct = {*
   3.151 +    Method.ctxt_args (fn ctxt =>
   3.152 +        Method.METHOD (fn facts =>
   3.153 +            ns_induct_tac (Classical.get_local_claset ctxt,
   3.154 +                               Simplifier.get_local_simpset ctxt) 1)) *}
   3.155 +    "for inductive reasoning about the Needham-Schroeder protocol"
   3.156 +
   3.157 +text{*Converts invariants into statements about reachable states*}
   3.158 +lemmas Always_Collect_reachableD =
   3.159 +     Always_includes_reachable [THEN subsetD, THEN CollectD]
   3.160 +
   3.161 +text{*Spy never sees another agent's private key! (unless it's bad at start)*}
   3.162 +lemma Spy_see_priK:
   3.163 +     "Nprg \<in> Always {s. (Key (priK A) \<in> parts (spies s)) = (A \<in> bad)}"
   3.164 +apply ns_induct
   3.165 +apply blast
   3.166 +done
   3.167 +declare Spy_see_priK [THEN Always_Collect_reachableD, simp]
   3.168 +
   3.169 +lemma Spy_analz_priK:
   3.170 +     "Nprg \<in> Always {s. (Key (priK A) \<in> analz (spies s)) = (A \<in> bad)}"
   3.171 +by (rule Always_reachable [THEN Always_weaken], auto)
   3.172 +declare Spy_analz_priK [THEN Always_Collect_reachableD, simp]
   3.173 +
   3.174 +
   3.175 +subsection{*Authenticity properties obtained from NS2*}
   3.176 +
   3.177 +text{*It is impossible to re-use a nonce in both NS1 and NS2 provided the
   3.178 +     nonce is secret.  (Honest users generate fresh nonces.)*}
   3.179 +lemma no_nonce_NS1_NS2:
   3.180 + "Nprg
   3.181 +  \<in> Always {s. Crypt (pubK C) {|NA', Nonce NA|} \<in> parts (spies s) -->
   3.182 +                Crypt (pubK B) {|Nonce NA, Agent A|} \<in> parts (spies s) -->
   3.183 +                Nonce NA \<in> analz (spies s)}"
   3.184 +apply ns_induct
   3.185 +apply (blast intro: analz_insertI)+
   3.186 +done
   3.187 +
   3.188 +text{*Adding it to the claset slows down proofs...*}
   3.189 +lemmas no_nonce_NS1_NS2_reachable =
   3.190 +       no_nonce_NS1_NS2 [THEN Always_Collect_reachableD, rule_format]
   3.191 +
   3.192 +
   3.193 +text{*Unicity for NS1: nonce NA identifies agents A and B*}
   3.194 +lemma unique_NA_lemma:
   3.195 +     "Nprg
   3.196 +  \<in> Always {s. Nonce NA \<notin> analz (spies s) -->
   3.197 +                Crypt(pubK B) {|Nonce NA, Agent A|} \<in> parts(spies s) -->
   3.198 +                Crypt(pubK B') {|Nonce NA, Agent A'|} \<in> parts(spies s) -->
   3.199 +                A=A' & B=B'}"
   3.200 +apply ns_induct
   3.201 +apply auto
   3.202 +txt{*Fake, NS1 are non-trivial*}
   3.203 +done
   3.204 +
   3.205 +text{*Unicity for NS1: nonce NA identifies agents A and B*}
   3.206 +lemma unique_NA:
   3.207 +     "[| Crypt(pubK B)  {|Nonce NA, Agent A|} \<in> parts(spies s);
   3.208 +         Crypt(pubK B') {|Nonce NA, Agent A'|} \<in> parts(spies s);
   3.209 +         Nonce NA \<notin> analz (spies s);
   3.210 +         s \<in> reachable Nprg |]
   3.211 +      ==> A=A' & B=B'"
   3.212 +by (blast dest: unique_NA_lemma [THEN Always_Collect_reachableD])
   3.213 +
   3.214 +
   3.215 +text{*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*}
   3.216 +lemma Spy_not_see_NA:
   3.217 +     "[| A \<notin> bad;  B \<notin> bad |]
   3.218 +  ==> Nprg \<in> Always
   3.219 +              {s. Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) \<in> set s
   3.220 +                  --> Nonce NA \<notin> analz (spies s)}"
   3.221 +apply ns_induct
   3.222 +txt{*NS3*}
   3.223 +prefer 4 apply (blast intro: no_nonce_NS1_NS2_reachable)
   3.224 +txt{*NS2*}
   3.225 +prefer 3 apply (blast dest: unique_NA)
   3.226 +txt{*NS1*}
   3.227 +prefer 2 apply blast
   3.228 +txt{*Fake*}
   3.229 +apply spy_analz
   3.230 +done
   3.231 +
   3.232 +
   3.233 +text{*Authentication for A: if she receives message 2 and has used NA
   3.234 +  to start a run, then B has sent message 2.*}
   3.235 +lemma A_trusts_NS2:
   3.236 + "[| A \<notin> bad;  B \<notin> bad |]
   3.237 +  ==> Nprg \<in> Always
   3.238 +              {s. Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) \<in> set s &
   3.239 +                  Crypt(pubK A) {|Nonce NA, Nonce NB|} \<in> parts (knows Spy s)
   3.240 +         --> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}) \<in> set s}"
   3.241 +  (*insert an invariant for use in some of the subgoals*)
   3.242 +apply (insert Spy_not_see_NA [of A B NA], simp, ns_induct)
   3.243 +apply (auto dest: unique_NA)
   3.244 +done
   3.245 +
   3.246 +
   3.247 +text{*If the encrypted message appears then it originated with Alice in NS1*}
   3.248 +lemma B_trusts_NS1:
   3.249 +     "Nprg \<in> Always
   3.250 +              {s. Nonce NA \<notin> analz (spies s) -->
   3.251 +                  Crypt (pubK B) {|Nonce NA, Agent A|} \<in> parts (spies s)
   3.252 +         --> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) \<in> set s}"
   3.253 +apply ns_induct
   3.254 +apply blast
   3.255 +done
   3.256 +
   3.257 +
   3.258 +subsection{*Authenticity properties obtained from NS2*}
   3.259 +
   3.260 +text{*Unicity for NS2: nonce NB identifies nonce NA and agent A.
   3.261 +   Proof closely follows that of @{text unique_NA}.*}
   3.262 +lemma unique_NB_lemma:
   3.263 + "Nprg
   3.264 +  \<in> Always {s. Nonce NB \<notin> analz (spies s)  -->
   3.265 +                Crypt (pubK A) {|Nonce NA, Nonce NB|} \<in> parts (spies s) -->
   3.266 +                Crypt(pubK A'){|Nonce NA', Nonce NB|} \<in> parts(spies s) -->
   3.267 +                A=A' & NA=NA'}"
   3.268 +apply ns_induct
   3.269 +apply auto
   3.270 +txt{*Fake, NS2 are non-trivial*}
   3.271 +done
   3.272 +
   3.273 +lemma unique_NB:
   3.274 +     "[| Crypt(pubK A) {|Nonce NA, Nonce NB|} \<in> parts(spies s);
   3.275 +         Crypt(pubK A'){|Nonce NA', Nonce NB|} \<in> parts(spies s);
   3.276 +         Nonce NB \<notin> analz (spies s);
   3.277 +         s \<in> reachable Nprg |]
   3.278 +      ==> A=A' & NA=NA'"
   3.279 +apply (blast dest: unique_NB_lemma [THEN Always_Collect_reachableD])
   3.280 +done
   3.281 +
   3.282 +
   3.283 +text{*NB remains secret PROVIDED Alice never responds with round 3*}
   3.284 +lemma Spy_not_see_NB:
   3.285 +     "[| A \<notin> bad;  B \<notin> bad |]
   3.286 +  ==> Nprg \<in> Always
   3.287 +              {s. Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \<in> set s &
   3.288 +                  (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set s)
   3.289 +                  --> Nonce NB \<notin> analz (spies s)}"
   3.290 +apply ns_induct
   3.291 +apply (simp_all (no_asm_simp) add: all_conj_distrib)
   3.292 +txt{*NS3: because NB determines A*}
   3.293 +prefer 4 apply (blast dest: unique_NB)
   3.294 +txt{*NS2: by freshness and unicity of NB*}
   3.295 +prefer 3 apply (blast intro: no_nonce_NS1_NS2_reachable)
   3.296 +txt{*NS1: by freshness*}
   3.297 +prefer 2 apply blast
   3.298 +txt{*Fake*}
   3.299 +apply spy_analz
   3.300 +done
   3.301  
   3.302  
   3.303  
   3.304 -constdefs
   3.305 -  Nprg :: state program
   3.306 -    (*Initial trace is empty*)
   3.307 -    "Nprg == mk_total_program({[]}, {Fake, NS1, NS2, NS3}, UNIV)"
   3.308 +text{*Authentication for B: if he receives message 3 and has used NB
   3.309 +  in message 2, then A has sent message 3--to somebody....*}
   3.310 +lemma B_trusts_NS3:
   3.311 +     "[| A \<notin> bad;  B \<notin> bad |]
   3.312 +  ==> Nprg \<in> Always
   3.313 +              {s. Crypt (pubK B) (Nonce NB) \<in> parts (spies s) &
   3.314 +                  Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \<in> set s
   3.315 +                  --> (\<exists>C. Says A C (Crypt (pubK C) (Nonce NB)) \<in> set s)}"
   3.316 +  (*insert an invariant for use in some of the subgoals*)
   3.317 +apply (insert Spy_not_see_NB [of A B NA NB], simp, ns_induct)
   3.318 +apply (simp_all (no_asm_simp) add: ex_disj_distrib)
   3.319 +apply auto
   3.320 +txt{*NS3: because NB determines A. This use of @{text unique_NB} is robust.*}
   3.321 +apply (blast intro: unique_NB [THEN conjunct1])
   3.322 +done
   3.323 +
   3.324 +
   3.325 +text{*Can we strengthen the secrecy theorem?  NO*}
   3.326 +lemma "[| A \<notin> bad;  B \<notin> bad |]
   3.327 +  ==> Nprg \<in> Always
   3.328 +              {s. Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \<in> set s
   3.329 +                  --> Nonce NB \<notin> analz (spies s)}"
   3.330 +apply ns_induct
   3.331 +apply auto
   3.332 +txt{*Fake*}
   3.333 +apply spy_analz
   3.334 +txt{*NS2: by freshness and unicity of NB*}
   3.335 + apply (blast intro: no_nonce_NS1_NS2_reachable)
   3.336 +txt{*NS3: unicity of NB identifies A and NA, but not B*}
   3.337 +apply (frule_tac A'=A in Says_imp_spies [THEN parts.Inj, THEN unique_NB])
   3.338 +apply (erule Says_imp_spies [THEN parts.Inj], auto)
   3.339 +apply (rename_tac s B' C)
   3.340 +txt{*This is the attack!
   3.341 +@{subgoals[display,indent=0,margin=65]}
   3.342 +*}
   3.343 +oops
   3.344 +
   3.345 +
   3.346 +(*
   3.347 +THIS IS THE ATTACK!
   3.348 +[| A \<notin> bad; B \<notin> bad |]
   3.349 +==> Nprg
   3.350 +   \<in> Always
   3.351 +       {s. Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \<in> set s -->
   3.352 +           Nonce NB \<notin> analz (knows Spy s)}
   3.353 + 1. !!s B' C.
   3.354 +       [| A \<notin> bad; B \<notin> bad; s \<in> reachable Nprg
   3.355 +          Says A C (Crypt (pubK C) {|Nonce NA, Agent A|}) \<in> set s;
   3.356 +          Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \<in> set s;
   3.357 +          C \<in> bad; Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \<in> set s;
   3.358 +          Nonce NB \<notin> analz (knows Spy s) |]
   3.359 +       ==> False
   3.360 +*)
   3.361  
   3.362  end