--- a/src/HOL/UNITY/ROOT.ML Tue Sep 23 15:44:25 2003 +0200
+++ b/src/HOL/UNITY/ROOT.ML Tue Sep 23 15:49:17 2003 +0200
@@ -20,8 +20,9 @@
time_use_thy "Simple/Reach";
time_use_thy "Simple/Reachability";
-with_path "../Auth" (*to find Public.thy*)
- time_use_thy"Simple/NSP_Bad";
+(*Verifying security protocols using UNITY*)
+with_path "../Auth" (no_document use_thy) "Public";
+with_path "../Auth" time_use_thy "Simple/NSP_Bad";
(*Example of composition*)
time_use_thy "Comp/Handshake";
--- a/src/HOL/UNITY/Simple/NSP_Bad.ML Tue Sep 23 15:44:25 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,299 +0,0 @@
-(* Title: HOL/Auth/NSP_Bad
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-
-Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol.
-Flawed version, vulnerable to Lowe's attack.
-
-From page 260 of
- Burrows, Abadi and Needham. A Logic of Authentication.
- Proc. Royal Soc. 426 (1989)
-*)
-
-fun impOfAlways th =
- ObjectLogic.rulify (th RS Always_includes_reachable RS subsetD RS CollectD);
-
-AddEs spies_partsEs;
-AddDs [impOfSubs analz_subset_parts];
-AddDs [impOfSubs Fake_parts_insert];
-
-(*For other theories, e.g. Mutex and Lift, using AddIffs slows proofs down.
- Here, it facilitates re-use of the Auth proofs.*)
-
-AddIffs (map simp_of_act [Fake_def, NS1_def, NS2_def, NS3_def]);
-Addsimps [Nprg_def RS def_prg_Init];
-
-
-(*A "possibility property": there are traces that reach the end.
- Replace by LEADSTO proof!*)
-Goal "A ~= B ==> EX NB. EX s: reachable Nprg. \
-\ Says A B (Crypt (pubK B) (Nonce NB)) : set s";
-by (REPEAT (resolve_tac [exI,bexI] 1));
-by (res_inst_tac [("act", "totalize_act NS3")] reachable_Acts 2);
-by (res_inst_tac [("act", "totalize_act NS2")] reachable_Acts 3);
-by (res_inst_tac [("act", "totalize_act NS1")] reachable_Acts 4);
-by (rtac reachable_Init 5);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [Nprg_def, totalize_act_def])));
- (*Now ignore the possibility of identity transitions*)
-by (REPEAT_FIRST (resolve_tac [disjI1, exI]));
-by possibility_tac;
-result();
-
-
-(**** Inductive proofs about ns_public ****)
-
-(*can be used to simulate analz_mono_contra_tac
-val analz_impI = read_instantiate_sg (sign_of thy)
- [("P", "?Y ~: analz (spies ?evs)")] impI;
-
-val spies_Says_analz_contraD =
- spies_subset_spies_Says RS analz_mono RS contra_subsetD;
-
-by (rtac analz_impI 2);
-by (auto_tac (claset() addSDs [spies_Says_analz_contraD], simpset()));
-*)
-
-val [prem] =
-Goal "(!!act s s'. [| act: {Id, Fake, NS1, NS2, NS3}; \
-\ (s,s') \\<in> act; s \\<in> A |] ==> s': A') \
-\ ==> Nprg \\<in> A co A'";
-by (asm_full_simp_tac (simpset() addsimps [Nprg_def, mk_total_program_def]) 1);
-by (rtac constrainsI 1);
-by (rtac prem 1);
-by Auto_tac;
-qed "ns_constrainsI";
-
-
-fun ns_constrains_tac i =
- SELECT_GOAL
- (EVERY [REPEAT (etac Always_ConstrainsI 1),
- REPEAT (resolve_tac [StableI, stableI,
- constrains_imp_Constrains] 1),
- rtac ns_constrainsI 1,
- Full_simp_tac 1,
- REPEAT (FIRSTGOAL (etac disjE)),
- ALLGOALS (clarify_tac (claset() delrules [impI,impCE])),
- REPEAT (FIRSTGOAL analz_mono_contra_tac),
- ALLGOALS Asm_simp_tac]) i;
-
-(*Tactic for proving secrecy theorems*)
-val ns_induct_tac =
- (SELECT_GOAL o EVERY)
- [rtac AlwaysI 1,
- Force_tac 1,
- (*"reachable" gets in here*)
- rtac (Always_reachable RS Always_ConstrainsI RS StableI) 1,
- ns_constrains_tac 1];
-
-
-(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
- sends messages containing X! **)
-
-(*Spy never sees another agent's private key! (unless it's bad at start)*)
-Goal "Nprg : Always {s. (Key (priK A) : parts (spies s)) = (A : bad)}";
-by (ns_induct_tac 1);
-by (Blast_tac 1);
-qed "Spy_see_priK";
-Addsimps [impOfAlways Spy_see_priK];
-
-Goal "Nprg : Always {s. (Key (priK A) : analz (spies s)) = (A : bad)}";
-by (rtac (Always_reachable RS Always_weaken) 1);
-by Auto_tac;
-qed "Spy_analz_priK";
-Addsimps [impOfAlways Spy_analz_priK];
-
-(**
-AddSDs [Spy_see_priK RSN (2, rev_iffD1),
- Spy_analz_priK RSN (2, rev_iffD1)];
-**)
-
-
-(**** Authenticity properties obtained from NS2 ****)
-
-(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
- is secret. (Honest users generate fresh nonces.)*)
-Goal
- "Nprg \
-\ : Always {s. Nonce NA ~: analz (spies s) --> \
-\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies s) --> \
-\ Crypt (pubK C) {|NA', Nonce NA|} ~: parts (spies s)}";
-by (ns_induct_tac 1);
-by (ALLGOALS Blast_tac);
-qed "no_nonce_NS1_NS2";
-
-(*Adding it to the claset slows down proofs...*)
-val nonce_NS1_NS2_E = impOfAlways no_nonce_NS1_NS2 RSN (2, rev_notE);
-
-
-(*Unicity for NS1: nonce NA identifies agents A and B*)
-Goal "Nprg \
-\ : Always {s. Nonce NA ~: analz (spies s) --> \
-\ Crypt(pubK B) {|Nonce NA, Agent A|} : parts(spies s) --> \
-\ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies s) --> \
-\ A=A' & B=B'}";
-by (ns_induct_tac 1);
-by Auto_tac;
-(*Fake, NS1 are non-trivial*)
-val unique_NA_lemma = result();
-
-(*Unicity for NS1: nonce NA identifies agents A and B*)
-Goal "[| Crypt(pubK B) {|Nonce NA, Agent A|} : parts(spies s); \
-\ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies s); \
-\ Nonce NA ~: analz (spies s); \
-\ s : reachable Nprg |] \
-\ ==> A=A' & B=B'";
-by (blast_tac (claset() addDs [impOfAlways unique_NA_lemma]) 1);
-qed "unique_NA";
-
-
-(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
-Goal "[| A ~: bad; B ~: bad |] \
-\ ==> Nprg : Always \
-\ {s. Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set s \
-\ --> Nonce NA ~: analz (spies s)}";
-by (ns_induct_tac 1);
-(*NS3*)
-by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 4);
-(*NS2*)
-by (blast_tac (claset() addDs [unique_NA]) 3);
-(*NS1*)
-by (Blast_tac 2);
-(*Fake*)
-by (spy_analz_tac 1);
-qed "Spy_not_see_NA";
-
-
-(*Authentication for A: if she receives message 2 and has used NA
- to start a run, then B has sent message 2.*)
-val prems =
-goal thy "[| A ~: bad; B ~: bad |] \
-\ ==> Nprg : Always \
-\ {s. Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set s & \
-\ Crypt(pubK A) {|Nonce NA, Nonce NB|} : parts (knows Spy s) \
-\ --> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set s}";
- (*insert an invariant for use in some of the subgoals*)
-by (cut_facts_tac ([prems MRS Spy_not_see_NA] @ prems) 1);
-by (ns_induct_tac 1);
-by (ALLGOALS Clarify_tac);
-(*NS2*)
-by (blast_tac (claset() addDs [unique_NA]) 3);
-(*NS1*)
-by (Blast_tac 2);
-(*Fake*)
-by (Blast_tac 1);
-qed "A_trusts_NS2";
-
-
-(*If the encrypted message appears then it originated with Alice in NS1*)
-Goal "Nprg : Always \
-\ {s. Nonce NA ~: analz (spies s) --> \
-\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies s) \
-\ --> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set s}";
-by (ns_induct_tac 1);
-by (Blast_tac 1);
-qed "B_trusts_NS1";
-
-
-
-(**** Authenticity properties obtained from NS2 ****)
-
-(*Unicity for NS2: nonce NB identifies nonce NA and agent A
- [proof closely follows that for unique_NA] *)
-Goal
- "Nprg \
-\ : Always {s. Nonce NB ~: analz (spies s) --> \
-\ Crypt (pubK A) {|Nonce NA, Nonce NB|} : parts (spies s) --> \
-\ Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(spies s) --> \
-\ A=A' & NA=NA'}";
-by (ns_induct_tac 1);
-by Auto_tac;
-(*Fake, NS2 are non-trivial*)
-val unique_NB_lemma = result();
-
-Goal "[| Crypt(pubK A) {|Nonce NA, Nonce NB|} : parts(spies s); \
-\ Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(spies s); \
-\ Nonce NB ~: analz (spies s); \
-\ s : reachable Nprg |] \
-\ ==> A=A' & NA=NA'";
-by (blast_tac (claset() addDs [impOfAlways unique_NB_lemma]) 1);
-qed "unique_NB";
-
-
-(*NB remains secret PROVIDED Alice never responds with round 3*)
-Goal "[| A ~: bad; B ~: bad |] \
-\ ==> Nprg : Always \
-\ {s. Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set s & \
-\ (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set s) \
-\ --> Nonce NB ~: analz (spies s)}";
-by (ns_induct_tac 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
-by (ALLGOALS Clarify_tac);
-(*NS3: because NB determines A*)
-by (blast_tac (claset() addDs [unique_NB]) 4);
-(*NS2: by freshness and unicity of NB*)
-by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 3);
-(*NS1: by freshness*)
-by (Blast_tac 2);
-(*Fake*)
-by (spy_analz_tac 1);
-qed "Spy_not_see_NB";
-
-
-
-(*Authentication for B: if he receives message 3 and has used NB
- in message 2, then A has sent message 3--to somebody....*)
-val prems =
-goal thy "[| A ~: bad; B ~: bad |] \
-\ ==> Nprg : Always \
-\ {s. Crypt (pubK B) (Nonce NB) : parts (spies s) & \
-\ Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set s \
-\ --> (EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set s)}";
- (*insert an invariant for use in some of the subgoals*)
-by (cut_facts_tac ([prems MRS Spy_not_see_NB] @ prems) 1);
-by (ns_induct_tac 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
-by (ALLGOALS Clarify_tac);
-(*NS3: because NB determines A (this use of unique_NB is more robust) *)
-by (blast_tac (claset() addIs [unique_NB RS conjunct1]) 3);
-(*NS1: by freshness*)
-by (Blast_tac 2);
-(*Fake*)
-by (Blast_tac 1);
-qed "B_trusts_NS3";
-
-
-(*Can we strengthen the secrecy theorem? NO*)
-Goal "[| A ~: bad; B ~: bad |] \
-\ ==> Nprg : Always \
-\ {s. Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set s \
-\ --> Nonce NB ~: analz (spies s)}";
-by (ns_induct_tac 1);
-by (ALLGOALS Clarify_tac);
-(*NS2: by freshness and unicity of NB*)
-by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 3);
-(*NS1: by freshness*)
-by (Blast_tac 2);
-(*Fake*)
-by (spy_analz_tac 1);
-(*NS3: unicity of NB identifies A and NA, but not B*)
-by (forw_inst_tac [("A'","A")] (Says_imp_spies RS parts.Inj RS unique_NB) 1
- THEN REPEAT (eresolve_tac [asm_rl, Says_imp_spies RS parts.Inj] 1));
-by Auto_tac;
-by (rename_tac "s B' C" 1);
-
-(*
-THIS IS THE ATTACK!
-[| A ~: bad; B ~: bad |]
-==> Nprg
- : Always
- {s. Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set s -->
- Nonce NB ~: analz (knows Spy s)}
- 1. !!s B' C.
- [| A ~: bad; B ~: bad; s : reachable Nprg;
- Says A C (Crypt (pubK C) {|Nonce NA, Agent A|}) : set s;
- Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set s;
- C : bad; Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set s;
- Nonce NB ~: analz (knows Spy s) |]
- ==> False
-*)
--- a/src/HOL/UNITY/Simple/NSP_Bad.thy Tue Sep 23 15:44:25 2003 +0200
+++ b/src/HOL/UNITY/Simple/NSP_Bad.thy Tue Sep 23 15:49:17 2003 +0200
@@ -3,57 +3,336 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
-add_path "../Auth"; use_thy"NSP_Bad";
-
-Security protocols in UNITY: Needham-Schroeder, public keys (flawed version).
+ML{*add_path "$ISABELLE_HOME/src/HOL/Auth"*}
Original file is ../Auth/NS_Public_Bad
*)
-NSP_Bad = Public + UNITY_Main +
+header{*Analyzing the Needham-Schroeder Public-Key Protocol in UNITY*}
+
+theory NSP_Bad = Public + UNITY_Main:
-types state = event list
+text{*This is the flawed version, vulnerable to Lowe's attack.
+From page 260 of
+ Burrows, Abadi and Needham. A Logic of Authentication.
+ Proc. Royal Soc. 426 (1989).
+*}
+
+types state = "event list"
constdefs
-
+
(*The spy MAY say anything he CAN say. We do not expect him to
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
Fake :: "(state*state) set"
"Fake == {(s,s').
- EX B X. s' = Says Spy B X # s
- & X: synth (analz (spies s))}"
-
+ \<exists>B X. s' = Says Spy B X # s
+ & X \<in> synth (analz (spies s))}"
+
(*The numeric suffixes on A identify the rule*)
(*Alice initiates a protocol run, sending a nonce to Bob*)
NS1 :: "(state*state) set"
"NS1 == {(s1,s').
- EX A1 B NA.
+ \<exists>A1 B NA.
s' = Says A1 B (Crypt (pubK B) {|Nonce NA, Agent A1|}) # s1
- & Nonce NA ~: used s1}"
-
+ & Nonce NA \<notin> used s1}"
+
(*Bob responds to Alice's message with a further nonce*)
NS2 :: "(state*state) set"
"NS2 == {(s2,s').
- EX A' A2 B NA NB.
+ \<exists>A' A2 B NA NB.
s' = Says B A2 (Crypt (pubK A2) {|Nonce NA, Nonce NB|}) # s2
- & Says A' B (Crypt (pubK B) {|Nonce NA, Agent A2|}) : set s2
- & Nonce NB ~: used s2}"
-
+ & Says A' B (Crypt (pubK B) {|Nonce NA, Agent A2|}) \<in> set s2
+ & Nonce NB \<notin> used s2}"
+
(*Alice proves her existence by sending NB back to Bob.*)
NS3 :: "(state*state) set"
"NS3 == {(s3,s').
- EX A3 B' B NA NB.
+ \<exists>A3 B' B NA NB.
s' = Says A3 B (Crypt (pubK B) (Nonce NB)) # s3
- & Says A3 B (Crypt (pubK B) {|Nonce NA, Agent A3|}) : set s3
- & Says B' A3 (Crypt (pubK A3) {|Nonce NA, Nonce NB|}) : set s3}"
+ & Says A3 B (Crypt (pubK B) {|Nonce NA, Agent A3|}) \<in> set s3
+ & Says B' A3 (Crypt (pubK A3) {|Nonce NA, Nonce NB|}) \<in> set s3}"
+
+
+constdefs
+ Nprg :: "state program"
+ (*Initial trace is empty*)
+ "Nprg == mk_total_program({[]}, {Fake, NS1, NS2, NS3}, UNIV)"
+
+declare spies_partsEs [elim]
+declare analz_into_parts [dest]
+declare Fake_parts_insert_in_Un [dest]
+
+text{*For other theories, e.g. Mutex and Lift, using [iff] slows proofs down.
+ Here, it facilitates re-use of the Auth proofs.*}
+
+declare Fake_def [THEN def_act_simp, iff]
+declare NS1_def [THEN def_act_simp, iff]
+declare NS2_def [THEN def_act_simp, iff]
+declare NS3_def [THEN def_act_simp, iff]
+
+declare Nprg_def [THEN def_prg_Init, simp]
+
+
+text{*A "possibility property": there are traces that reach the end.
+ Replace by LEADSTO proof!*}
+lemma "A \<noteq> B ==>
+ \<exists>NB. \<exists>s \<in> reachable Nprg. Says A B (Crypt (pubK B) (Nonce NB)) \<in> set s"
+apply (intro exI bexI)
+apply (rule_tac [2] act = "totalize_act NS3" in reachable.Acts)
+apply (rule_tac [3] act = "totalize_act NS2" in reachable.Acts)
+apply (rule_tac [4] act = "totalize_act NS1" in reachable.Acts)
+apply (rule_tac [5] reachable.Init)
+apply (simp_all (no_asm_simp) add: Nprg_def totalize_act_def)
+apply auto
+done
+
+
+subsection{*Inductive Proofs about @{term ns_public}*}
+
+lemma ns_constrainsI:
+ "(!!act s s'. [| act \<in> {Id, Fake, NS1, NS2, NS3};
+ (s,s') \<in> act; s \<in> A |] ==> s' \<in> A')
+ ==> Nprg \<in> A co A'"
+apply (simp add: Nprg_def mk_total_program_def)
+apply (rule constrainsI, auto)
+done
+
+
+text{*This ML code does the inductions directly.*}
+ML{*
+val ns_constrainsI = thm "ns_constrainsI";
+
+fun ns_constrains_tac(cs,ss) i =
+ SELECT_GOAL
+ (EVERY [REPEAT (etac Always_ConstrainsI 1),
+ REPEAT (resolve_tac [StableI, stableI,
+ constrains_imp_Constrains] 1),
+ rtac ns_constrainsI 1,
+ full_simp_tac ss 1,
+ REPEAT (FIRSTGOAL (etac disjE)),
+ ALLGOALS (clarify_tac (cs delrules [impI,impCE])),
+ REPEAT (FIRSTGOAL analz_mono_contra_tac),
+ ALLGOALS (asm_simp_tac ss)]) i;
+
+(*Tactic for proving secrecy theorems*)
+fun ns_induct_tac(cs,ss) =
+ (SELECT_GOAL o EVERY)
+ [rtac AlwaysI 1,
+ force_tac (cs,ss) 1,
+ (*"reachable" gets in here*)
+ rtac (Always_reachable RS Always_ConstrainsI RS StableI) 1,
+ ns_constrains_tac(cs,ss) 1];
+*}
+
+method_setup ns_induct = {*
+ Method.ctxt_args (fn ctxt =>
+ Method.METHOD (fn facts =>
+ ns_induct_tac (Classical.get_local_claset ctxt,
+ Simplifier.get_local_simpset ctxt) 1)) *}
+ "for inductive reasoning about the Needham-Schroeder protocol"
+
+text{*Converts invariants into statements about reachable states*}
+lemmas Always_Collect_reachableD =
+ Always_includes_reachable [THEN subsetD, THEN CollectD]
+
+text{*Spy never sees another agent's private key! (unless it's bad at start)*}
+lemma Spy_see_priK:
+ "Nprg \<in> Always {s. (Key (priK A) \<in> parts (spies s)) = (A \<in> bad)}"
+apply ns_induct
+apply blast
+done
+declare Spy_see_priK [THEN Always_Collect_reachableD, simp]
+
+lemma Spy_analz_priK:
+ "Nprg \<in> Always {s. (Key (priK A) \<in> analz (spies s)) = (A \<in> bad)}"
+by (rule Always_reachable [THEN Always_weaken], auto)
+declare Spy_analz_priK [THEN Always_Collect_reachableD, simp]
+
+
+subsection{*Authenticity properties obtained from NS2*}
+
+text{*It is impossible to re-use a nonce in both NS1 and NS2 provided the
+ nonce is secret. (Honest users generate fresh nonces.)*}
+lemma no_nonce_NS1_NS2:
+ "Nprg
+ \<in> Always {s. Crypt (pubK C) {|NA', Nonce NA|} \<in> parts (spies s) -->
+ Crypt (pubK B) {|Nonce NA, Agent A|} \<in> parts (spies s) -->
+ Nonce NA \<in> analz (spies s)}"
+apply ns_induct
+apply (blast intro: analz_insertI)+
+done
+
+text{*Adding it to the claset slows down proofs...*}
+lemmas no_nonce_NS1_NS2_reachable =
+ no_nonce_NS1_NS2 [THEN Always_Collect_reachableD, rule_format]
+
+
+text{*Unicity for NS1: nonce NA identifies agents A and B*}
+lemma unique_NA_lemma:
+ "Nprg
+ \<in> Always {s. Nonce NA \<notin> analz (spies s) -->
+ Crypt(pubK B) {|Nonce NA, Agent A|} \<in> parts(spies s) -->
+ Crypt(pubK B') {|Nonce NA, Agent A'|} \<in> parts(spies s) -->
+ A=A' & B=B'}"
+apply ns_induct
+apply auto
+txt{*Fake, NS1 are non-trivial*}
+done
+
+text{*Unicity for NS1: nonce NA identifies agents A and B*}
+lemma unique_NA:
+ "[| Crypt(pubK B) {|Nonce NA, Agent A|} \<in> parts(spies s);
+ Crypt(pubK B') {|Nonce NA, Agent A'|} \<in> parts(spies s);
+ Nonce NA \<notin> analz (spies s);
+ s \<in> reachable Nprg |]
+ ==> A=A' & B=B'"
+by (blast dest: unique_NA_lemma [THEN Always_Collect_reachableD])
+
+
+text{*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*}
+lemma Spy_not_see_NA:
+ "[| A \<notin> bad; B \<notin> bad |]
+ ==> Nprg \<in> Always
+ {s. Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) \<in> set s
+ --> Nonce NA \<notin> analz (spies s)}"
+apply ns_induct
+txt{*NS3*}
+prefer 4 apply (blast intro: no_nonce_NS1_NS2_reachable)
+txt{*NS2*}
+prefer 3 apply (blast dest: unique_NA)
+txt{*NS1*}
+prefer 2 apply blast
+txt{*Fake*}
+apply spy_analz
+done
+
+
+text{*Authentication for A: if she receives message 2 and has used NA
+ to start a run, then B has sent message 2.*}
+lemma A_trusts_NS2:
+ "[| A \<notin> bad; B \<notin> bad |]
+ ==> Nprg \<in> Always
+ {s. Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) \<in> set s &
+ Crypt(pubK A) {|Nonce NA, Nonce NB|} \<in> parts (knows Spy s)
+ --> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}) \<in> set s}"
+ (*insert an invariant for use in some of the subgoals*)
+apply (insert Spy_not_see_NA [of A B NA], simp, ns_induct)
+apply (auto dest: unique_NA)
+done
+
+
+text{*If the encrypted message appears then it originated with Alice in NS1*}
+lemma B_trusts_NS1:
+ "Nprg \<in> Always
+ {s. Nonce NA \<notin> analz (spies s) -->
+ Crypt (pubK B) {|Nonce NA, Agent A|} \<in> parts (spies s)
+ --> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) \<in> set s}"
+apply ns_induct
+apply blast
+done
+
+
+subsection{*Authenticity properties obtained from NS2*}
+
+text{*Unicity for NS2: nonce NB identifies nonce NA and agent A.
+ Proof closely follows that of @{text unique_NA}.*}
+lemma unique_NB_lemma:
+ "Nprg
+ \<in> Always {s. Nonce NB \<notin> analz (spies s) -->
+ Crypt (pubK A) {|Nonce NA, Nonce NB|} \<in> parts (spies s) -->
+ Crypt(pubK A'){|Nonce NA', Nonce NB|} \<in> parts(spies s) -->
+ A=A' & NA=NA'}"
+apply ns_induct
+apply auto
+txt{*Fake, NS2 are non-trivial*}
+done
+
+lemma unique_NB:
+ "[| Crypt(pubK A) {|Nonce NA, Nonce NB|} \<in> parts(spies s);
+ Crypt(pubK A'){|Nonce NA', Nonce NB|} \<in> parts(spies s);
+ Nonce NB \<notin> analz (spies s);
+ s \<in> reachable Nprg |]
+ ==> A=A' & NA=NA'"
+apply (blast dest: unique_NB_lemma [THEN Always_Collect_reachableD])
+done
+
+
+text{*NB remains secret PROVIDED Alice never responds with round 3*}
+lemma Spy_not_see_NB:
+ "[| A \<notin> bad; B \<notin> bad |]
+ ==> Nprg \<in> Always
+ {s. Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \<in> set s &
+ (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set s)
+ --> Nonce NB \<notin> analz (spies s)}"
+apply ns_induct
+apply (simp_all (no_asm_simp) add: all_conj_distrib)
+txt{*NS3: because NB determines A*}
+prefer 4 apply (blast dest: unique_NB)
+txt{*NS2: by freshness and unicity of NB*}
+prefer 3 apply (blast intro: no_nonce_NS1_NS2_reachable)
+txt{*NS1: by freshness*}
+prefer 2 apply blast
+txt{*Fake*}
+apply spy_analz
+done
-constdefs
- Nprg :: state program
- (*Initial trace is empty*)
- "Nprg == mk_total_program({[]}, {Fake, NS1, NS2, NS3}, UNIV)"
+text{*Authentication for B: if he receives message 3 and has used NB
+ in message 2, then A has sent message 3--to somebody....*}
+lemma B_trusts_NS3:
+ "[| A \<notin> bad; B \<notin> bad |]
+ ==> Nprg \<in> Always
+ {s. Crypt (pubK B) (Nonce NB) \<in> parts (spies s) &
+ Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \<in> set s
+ --> (\<exists>C. Says A C (Crypt (pubK C) (Nonce NB)) \<in> set s)}"
+ (*insert an invariant for use in some of the subgoals*)
+apply (insert Spy_not_see_NB [of A B NA NB], simp, ns_induct)
+apply (simp_all (no_asm_simp) add: ex_disj_distrib)
+apply auto
+txt{*NS3: because NB determines A. This use of @{text unique_NB} is robust.*}
+apply (blast intro: unique_NB [THEN conjunct1])
+done
+
+
+text{*Can we strengthen the secrecy theorem? NO*}
+lemma "[| A \<notin> bad; B \<notin> bad |]
+ ==> Nprg \<in> Always
+ {s. Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \<in> set s
+ --> Nonce NB \<notin> analz (spies s)}"
+apply ns_induct
+apply auto
+txt{*Fake*}
+apply spy_analz
+txt{*NS2: by freshness and unicity of NB*}
+ apply (blast intro: no_nonce_NS1_NS2_reachable)
+txt{*NS3: unicity of NB identifies A and NA, but not B*}
+apply (frule_tac A'=A in Says_imp_spies [THEN parts.Inj, THEN unique_NB])
+apply (erule Says_imp_spies [THEN parts.Inj], auto)
+apply (rename_tac s B' C)
+txt{*This is the attack!
+@{subgoals[display,indent=0,margin=65]}
+*}
+oops
+
+
+(*
+THIS IS THE ATTACK!
+[| A \<notin> bad; B \<notin> bad |]
+==> Nprg
+ \<in> Always
+ {s. Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \<in> set s -->
+ Nonce NB \<notin> analz (knows Spy s)}
+ 1. !!s B' C.
+ [| A \<notin> bad; B \<notin> bad; s \<in> reachable Nprg
+ Says A C (Crypt (pubK C) {|Nonce NA, Agent A|}) \<in> set s;
+ Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \<in> set s;
+ C \<in> bad; Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \<in> set s;
+ Nonce NB \<notin> analz (knows Spy s) |]
+ ==> False
+*)
end