1.1 --- a/src/HOL/IsaMakefile Tue Jul 31 12:38:01 2012 +0200
1.2 +++ b/src/HOL/IsaMakefile Thu Jul 26 15:55:19 2012 +0200
1.3 @@ -1513,10 +1513,6 @@
1.4 Quickcheck_Examples/ROOT.ML \
1.5 Quickcheck_Examples/Completeness.thy \
1.6 Quickcheck_Examples/Hotel_Example.thy \
1.7 - Quickcheck_Examples/Needham_Schroeder_Base.thy \
1.8 - Quickcheck_Examples/Needham_Schroeder_No_Attacker_Example.thy \
1.9 - Quickcheck_Examples/Needham_Schroeder_Guided_Attacker_Example.thy \
1.10 - Quickcheck_Examples/Needham_Schroeder_Unguided_Attacker_Example.thy \
1.11 Quickcheck_Examples/Quickcheck_Examples.thy \
1.12 Quickcheck_Examples/Quickcheck_Interfaces.thy \
1.13 Quickcheck_Examples/Quickcheck_Lattice_Examples.thy \
1.14 @@ -1823,6 +1819,10 @@
1.15
1.16 $(LOG)/HOL-Quickcheck_Benchmark.gz: $(OUT)/HOL \
1.17 Quickcheck_Benchmark/ROOT.ML \
1.18 + Quickcheck_Benchmark/Needham_Schroeder_Base.thy \
1.19 + Quickcheck_Benchmark/Needham_Schroeder_No_Attacker_Example.thy \
1.20 + Quickcheck_Benchmark/Needham_Schroeder_Guided_Attacker_Example.thy \
1.21 + Quickcheck_Benchmark/Needham_Schroeder_Unguided_Attacker_Example.thy \
1.22 Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy
1.23 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Quickcheck_Benchmark
1.24
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Thu Jul 26 15:55:19 2012 +0200
2.3 @@ -0,0 +1,200 @@
2.4 +theory Needham_Schroeder_Base
2.5 +imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
2.6 +begin
2.7 +
2.8 +datatype agent = Alice | Bob | Spy
2.9 +
2.10 +definition agents :: "agent set"
2.11 +where
2.12 + "agents = {Spy, Alice, Bob}"
2.13 +
2.14 +definition bad :: "agent set"
2.15 +where
2.16 + "bad = {Spy}"
2.17 +
2.18 +datatype key = pubEK agent | priEK agent
2.19 +
2.20 +fun invKey
2.21 +where
2.22 + "invKey (pubEK A) = priEK A"
2.23 +| "invKey (priEK A) = pubEK A"
2.24 +
2.25 +datatype
2.26 + msg = Agent agent
2.27 + | Key key
2.28 + | Nonce nat
2.29 + | MPair msg msg
2.30 + | Crypt key msg
2.31 +
2.32 +syntax
2.33 + "_MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})")
2.34 +
2.35 +syntax (xsymbols)
2.36 + "_MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
2.37 +
2.38 +translations
2.39 + "{|x, y, z|}" == "{|x, {|y, z|}|}"
2.40 + "{|x, y|}" == "CONST MPair x y"
2.41 +
2.42 +inductive_set
2.43 + parts :: "msg set => msg set"
2.44 + for H :: "msg set"
2.45 + where
2.46 + Inj [intro]: "X \<in> H ==> X \<in> parts H"
2.47 + | Fst: "{|X,Y|} \<in> parts H ==> X \<in> parts H"
2.48 + | Snd: "{|X,Y|} \<in> parts H ==> Y \<in> parts H"
2.49 + | Body: "Crypt K X \<in> parts H ==> X \<in> parts H"
2.50 +
2.51 +inductive_set
2.52 + analz :: "msg set => msg set"
2.53 + for H :: "msg set"
2.54 + where
2.55 + Inj [intro,simp] : "X \<in> H ==> X \<in> analz H"
2.56 + | Fst: "{|X,Y|} \<in> analz H ==> X \<in> analz H"
2.57 + | Snd: "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
2.58 + | Decrypt [dest]:
2.59 + "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
2.60 +
2.61 +inductive_set
2.62 + synth :: "msg set => msg set"
2.63 + for H :: "msg set"
2.64 + where
2.65 + Inj [intro]: "X \<in> H ==> X \<in> synth H"
2.66 + | Agent [intro]: "Agent agt \<in> synth H"
2.67 + | MPair [intro]: "[|X \<in> synth H; Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
2.68 + | Crypt [intro]: "[|X \<in> synth H; Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
2.69 +
2.70 +primrec initState
2.71 +where
2.72 + initState_Alice:
2.73 + "initState Alice = {Key (priEK Alice)} \<union> (Key ` pubEK ` agents)"
2.74 +| initState_Bob:
2.75 + "initState Bob = {Key (priEK Bob)} \<union> (Key ` pubEK ` agents)"
2.76 +| initState_Spy:
2.77 + "initState Spy = (Key ` priEK ` bad) \<union> (Key ` pubEK ` agents)"
2.78 +
2.79 +datatype
2.80 + event = Says agent agent msg
2.81 + | Gets agent msg
2.82 + | Notes agent msg
2.83 +
2.84 +
2.85 +primrec knows :: "agent => event list => msg set"
2.86 +where
2.87 + knows_Nil: "knows A [] = initState A"
2.88 +| knows_Cons:
2.89 + "knows A (ev # evs) =
2.90 + (if A = Spy then
2.91 + (case ev of
2.92 + Says A' B X => insert X (knows Spy evs)
2.93 + | Gets A' X => knows Spy evs
2.94 + | Notes A' X =>
2.95 + if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs)
2.96 + else
2.97 + (case ev of
2.98 + Says A' B X =>
2.99 + if A'=A then insert X (knows A evs) else knows A evs
2.100 + | Gets A' X =>
2.101 + if A'=A then insert X (knows A evs) else knows A evs
2.102 + | Notes A' X =>
2.103 + if A'=A then insert X (knows A evs) else knows A evs))"
2.104 +
2.105 +abbreviation (input)
2.106 + spies :: "event list => msg set" where
2.107 + "spies == knows Spy"
2.108 +
2.109 +primrec used :: "event list => msg set"
2.110 +where
2.111 + used_Nil: "used [] = Union (parts ` initState ` agents)"
2.112 +| used_Cons: "used (ev # evs) =
2.113 + (case ev of
2.114 + Says A B X => parts {X} \<union> used evs
2.115 + | Gets A X => used evs
2.116 + | Notes A X => parts {X} \<union> used evs)"
2.117 +
2.118 +subsection {* Preparations for sets *}
2.119 +
2.120 +fun find_first :: "('a => 'b option) => 'a list => 'b option"
2.121 +where
2.122 + "find_first f [] = None"
2.123 +| "find_first f (x # xs) = (case f x of Some y => Some y | None => find_first f xs)"
2.124 +
2.125 +consts cps_of_set :: "'a set => ('a => term list option) => term list option"
2.126 +
2.127 +lemma
2.128 + [code]: "cps_of_set (set xs) f = find_first f xs"
2.129 +sorry
2.130 +
2.131 +consts pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => code_numeral => (bool * term list) option"
2.132 +consts neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => code_numeral => term list Quickcheck_Exhaustive.three_valued"
2.133 +
2.134 +lemma
2.135 + [code]: "pos_cps_of_set (set xs) f i = find_first f xs"
2.136 +sorry
2.137 +
2.138 +consts find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued)
2.139 + => 'b list => 'a Quickcheck_Exhaustive.three_valued"
2.140 +
2.141 +lemma [code]:
2.142 + "find_first' f [] = Quickcheck_Exhaustive.No_value"
2.143 + "find_first' f (x # xs) = (case f (Quickcheck_Exhaustive.Known x) of Quickcheck_Exhaustive.No_value => find_first' f xs | Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x | Quickcheck_Exhaustive.Unknown_value => (case find_first' f xs of Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x | _ => Quickcheck_Exhaustive.Unknown_value))"
2.144 +sorry
2.145 +
2.146 +lemma
2.147 + [code]: "neg_cps_of_set (set xs) f i = find_first' f xs"
2.148 +sorry
2.149 +
2.150 +setup {*
2.151 +let
2.152 + val Fun = Predicate_Compile_Aux.Fun
2.153 + val Input = Predicate_Compile_Aux.Input
2.154 + val Output = Predicate_Compile_Aux.Output
2.155 + val Bool = Predicate_Compile_Aux.Bool
2.156 + val oi = Fun (Output, Fun (Input, Bool))
2.157 + val ii = Fun (Input, Fun (Input, Bool))
2.158 + fun of_set compfuns (Type ("fun", [T, _])) =
2.159 + case body_type (Predicate_Compile_Aux.mk_monadT compfuns T) of
2.160 + Type ("Quickcheck_Exhaustive.three_valued", _) =>
2.161 + Const(@{const_name neg_cps_of_set}, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T))
2.162 + | Type ("Predicate.pred", _) => Const(@{const_name pred_of_set}, HOLogic.mk_setT T --> Predicate_Compile_Aux.mk_monadT compfuns T)
2.163 + | _ => Const(@{const_name pos_cps_of_set}, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T))
2.164 + fun member compfuns (U as Type ("fun", [T, _])) =
2.165 + (absdummy T (absdummy (HOLogic.mk_setT T) (Predicate_Compile_Aux.mk_if compfuns
2.166 + (Const (@{const_name "Set.member"}, T --> HOLogic.mk_setT T --> @{typ bool}) $ Bound 1 $ Bound 0))))
2.167 +
2.168 +in
2.169 + Core_Data.force_modes_and_compilations @{const_name Set.member}
2.170 + [(oi, (of_set, false)), (ii, (member, false))]
2.171 +end
2.172 +*}
2.173 +
2.174 +subsection {* Derived equations for analz, parts and synth *}
2.175 +
2.176 +lemma [code]:
2.177 + "analz H = (let
2.178 + H' = H \<union> (Union ((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => if Key (invKey K) : H then {X} else {} | _ => {}) ` H))
2.179 + in if H' = H then H else analz H')"
2.180 +sorry
2.181 +
2.182 +lemma [code]:
2.183 + "parts H = (let
2.184 + H' = H \<union> (Union ((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => {X} | _ => {}) ` H))
2.185 + in if H' = H then H else parts H')"
2.186 +sorry
2.187 +
2.188 +definition synth' :: "msg set => msg => bool"
2.189 +where
2.190 + "synth' H m = (m : synth H)"
2.191 +
2.192 +lemmas [code_pred_intro] = synth.intros[folded synth'_def]
2.193 +
2.194 +code_pred [generator_cps] synth' unfolding synth'_def by (rule synth.cases) fastforce+
2.195 +
2.196 +setup {* Predicate_Compile_Data.ignore_consts [@{const_name analz}, @{const_name knows}] *}
2.197 +declare ListMem_iff[symmetric, code_pred_inline]
2.198 +declare [[quickcheck_timing]]
2.199 +
2.200 +setup {* Exhaustive_Generators.setup_exhaustive_datatype_interpretation *}
2.201 +declare [[quickcheck_full_support = false]]
2.202 +
2.203 +end
2.204 \ No newline at end of file
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Guided_Attacker_Example.thy Thu Jul 26 15:55:19 2012 +0200
3.3 @@ -0,0 +1,100 @@
3.4 +theory Needham_Schroeder_Guided_Attacker_Example
3.5 +imports Needham_Schroeder_Base
3.6 +begin
3.7 +
3.8 +inductive_set ns_public :: "event list set"
3.9 + where
3.10 + (*Initial trace is empty*)
3.11 + Nil: "[] \<in> ns_public"
3.12 +
3.13 + | Fake_NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<in> analz (spies evs1) \<rbrakk>
3.14 + \<Longrightarrow> Says Spy B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
3.15 + # evs1 \<in> ns_public"
3.16 + | Fake_NS2: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<in> analz (spies evs1); Nonce NB \<in> analz (spies evs1) \<rbrakk>
3.17 + \<Longrightarrow> Says Spy A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
3.18 + # evs1 \<in> ns_public"
3.19 +
3.20 + (*Alice initiates a protocol run, sending a nonce to Bob*)
3.21 + | NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk>
3.22 + \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
3.23 + # evs1 \<in> ns_public"
3.24 + (*Bob responds to Alice's message with a further nonce*)
3.25 + | NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2;
3.26 + Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
3.27 + \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
3.28 + # evs2 \<in> ns_public"
3.29 +
3.30 + (*Alice proves her existence by sending NB back to Bob.*)
3.31 + | NS3: "\<lbrakk>evs3 \<in> ns_public;
3.32 + Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
3.33 + Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
3.34 + \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
3.35 +
3.36 +declare ListMem_iff[symmetric, code_pred_inline]
3.37 +
3.38 +lemmas [code_pred_intro] = ns_publicp.intros[folded synth'_def]
3.39 +
3.40 +code_pred [skip_proof] ns_publicp unfolding synth'_def by (rule ns_publicp.cases) fastforce+
3.41 +thm ns_publicp.equation
3.42 +
3.43 +code_pred [generator_cps] ns_publicp .
3.44 +thm ns_publicp.generator_cps_equation
3.45 +
3.46 +
3.47 +lemma "ns_publicp evs ==> \<not> (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs"
3.48 +quickcheck[smart_exhaustive, depth = 5, timeout = 100, expect = counterexample]
3.49 +(*quickcheck[narrowing, size = 6, timeout = 200, verbose, expect = no_counterexample]*)
3.50 +oops
3.51 +
3.52 +lemma
3.53 + "\<lbrakk>ns_publicp evs\<rbrakk>
3.54 + \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs
3.55 + \<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B
3.56 + \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
3.57 +(*quickcheck[smart_exhaustive, depth = 6, timeout = 100, expect = counterexample]
3.58 +quickcheck[narrowing, size = 7, timeout = 200, expect = no_counterexample]*)
3.59 +oops
3.60 +
3.61 +section {* Proving the counterexample trace for validation *}
3.62 +
3.63 +lemma
3.64 + assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1"
3.65 + assumes "evs =
3.66 + [Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)),
3.67 + Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}),
3.68 + Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}),
3.69 + Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|})]" (is "_ = [?e3, ?e2, ?e1, ?e0]")
3.70 + shows "A \<noteq> Spy" "B \<noteq> Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)"
3.71 +proof -
3.72 + from assms show "A \<noteq> Spy" by auto
3.73 + from assms show "B \<noteq> Spy" by auto
3.74 + have "[] : ns_public" by (rule Nil)
3.75 + then have first_step: "[?e0] : ns_public"
3.76 + proof (rule NS1)
3.77 + show "Nonce 0 ~: used []" by eval
3.78 + qed
3.79 + then have "[?e1, ?e0] : ns_public"
3.80 + proof (rule Fake_NS1)
3.81 + show "Nonce 0 : analz (knows Spy [?e0])" by eval
3.82 + qed
3.83 + then have "[?e2, ?e1, ?e0] : ns_public"
3.84 + proof (rule NS2)
3.85 + show "Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}) \<in> set [?e1, ?e0]" by simp
3.86 + show " Nonce 1 ~: used [?e1, ?e0]" by eval
3.87 + qed
3.88 + then show "evs : ns_public"
3.89 + unfolding assms
3.90 + proof (rule NS3)
3.91 + show " Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|}) \<in> set [?e2, ?e1, ?e0]" by simp
3.92 + show "Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|})
3.93 + : set [?e2, ?e1, ?e0]" by simp
3.94 + qed
3.95 + from assms show "Nonce NB : analz (knows Spy evs)"
3.96 + apply simp
3.97 + apply (rule analz.intros(4))
3.98 + apply (rule analz.intros(1))
3.99 + apply (auto simp add: bad_def)
3.100 + done
3.101 +qed
3.102 +
3.103 +end
3.104 \ No newline at end of file
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_No_Attacker_Example.thy Thu Jul 26 15:55:19 2012 +0200
4.3 @@ -0,0 +1,47 @@
4.4 +theory Needham_Schroeder_No_Attacker_Example
4.5 +imports Needham_Schroeder_Base
4.6 +begin
4.7 +
4.8 +inductive_set ns_public :: "event list set"
4.9 + where
4.10 + (*Initial trace is empty*)
4.11 + Nil: "[] \<in> ns_public"
4.12 + (*Alice initiates a protocol run, sending a nonce to Bob*)
4.13 + | NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk>
4.14 + \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
4.15 + # evs1 \<in> ns_public"
4.16 + (*Bob responds to Alice's message with a further nonce*)
4.17 + | NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2;
4.18 + Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
4.19 + \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
4.20 + # evs2 \<in> ns_public"
4.21 +
4.22 + (*Alice proves her existence by sending NB back to Bob.*)
4.23 + | NS3: "\<lbrakk>evs3 \<in> ns_public;
4.24 + Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
4.25 + Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
4.26 + \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
4.27 +
4.28 +code_pred [skip_proof] ns_publicp .
4.29 +thm ns_publicp.equation
4.30 +
4.31 +code_pred [generator_cps] ns_publicp .
4.32 +thm ns_publicp.generator_cps_equation
4.33 +
4.34 +lemma "ns_publicp evs ==> \<not> (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs"
4.35 +(*quickcheck[random, iterations = 1000000, size = 20, timeout = 3600, verbose]
4.36 +quickcheck[exhaustive, size = 8, timeout = 3600, verbose]
4.37 +quickcheck[narrowing, size = 7, timeout = 3600, verbose]*)
4.38 +quickcheck[smart_exhaustive, depth = 5, timeout = 30, expect = counterexample]
4.39 +oops
4.40 +
4.41 +lemma
4.42 + "\<lbrakk>ns_publicp evs\<rbrakk>
4.43 + \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs
4.44 + \<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B
4.45 + \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
4.46 +quickcheck[smart_exhaustive, depth = 6, timeout = 30]
4.47 +quickcheck[narrowing, size = 6, timeout = 30, verbose]
4.48 +oops
4.49 +
4.50 +end
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Unguided_Attacker_Example.thy Thu Jul 26 15:55:19 2012 +0200
5.3 @@ -0,0 +1,96 @@
5.4 +theory Needham_Schroeder_Unguided_Attacker_Example
5.5 +imports Needham_Schroeder_Base
5.6 +begin
5.7 +
5.8 +inductive_set ns_public :: "event list set"
5.9 + where
5.10 + (*Initial trace is empty*)
5.11 + Nil: "[] \<in> ns_public"
5.12 +
5.13 + | Fake: "\<lbrakk>evs1 \<in> ns_public; X \<in> synth (analz (spies evs1)) \<rbrakk>
5.14 + \<Longrightarrow> Says Spy A X # evs1 \<in> ns_public"
5.15 +
5.16 + (*Alice initiates a protocol run, sending a nonce to Bob*)
5.17 + | NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk>
5.18 + \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
5.19 + # evs1 \<in> ns_public"
5.20 + (*Bob responds to Alice's message with a further nonce*)
5.21 + | NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2;
5.22 + Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
5.23 + \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
5.24 + # evs2 \<in> ns_public"
5.25 +
5.26 + (*Alice proves her existence by sending NB back to Bob.*)
5.27 + | NS3: "\<lbrakk>evs3 \<in> ns_public;
5.28 + Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
5.29 + Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
5.30 + \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
5.31 +
5.32 +declare ListMem_iff[symmetric, code_pred_inline]
5.33 +
5.34 +lemmas [code_pred_intro] = ns_publicp.intros[folded synth'_def]
5.35 +
5.36 +code_pred [skip_proof] ns_publicp unfolding synth'_def by (rule ns_publicp.cases) fastforce+
5.37 +thm ns_publicp.equation
5.38 +
5.39 +code_pred [generator_cps] ns_publicp .
5.40 +thm ns_publicp.generator_cps_equation
5.41 +
5.42 +
5.43 +lemma "ns_publicp evs ==> \<not> (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs"
5.44 +quickcheck[smart_exhaustive, depth = 5, timeout = 200, expect = counterexample]
5.45 +(*quickcheck[narrowing, size = 6, timeout = 200, verbose, expect = no_counterexample]*)
5.46 +oops
5.47 +
5.48 +lemma
5.49 + "\<lbrakk>ns_publicp evs\<rbrakk>
5.50 + \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs
5.51 + \<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B
5.52 + \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
5.53 +quickcheck[smart_exhaustive, depth = 6, timeout = 100, expect = no_counterexample]
5.54 +(*quickcheck[narrowing, size = 7, timeout = 200, expect = no_counterexample]*)
5.55 +oops
5.56 +
5.57 +section {* Proving the counterexample trace for validation *}
5.58 +
5.59 +lemma
5.60 + assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1"
5.61 + assumes "evs =
5.62 + [Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)),
5.63 + Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}),
5.64 + Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}),
5.65 + Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|})]" (is "_ = [?e3, ?e2, ?e1, ?e0]")
5.66 + shows "A \<noteq> Spy" "B \<noteq> Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)"
5.67 +proof -
5.68 + from assms show "A \<noteq> Spy" by auto
5.69 + from assms show "B \<noteq> Spy" by auto
5.70 + have "[] : ns_public" by (rule Nil)
5.71 + then have first_step: "[?e0] : ns_public"
5.72 + proof (rule NS1)
5.73 + show "Nonce 0 ~: used []" by eval
5.74 + qed
5.75 + then have "[?e1, ?e0] : ns_public"
5.76 + proof (rule Fake)
5.77 + show "Crypt (pubEK Bob) {|Nonce 0, Agent Alice|} : synth (analz (knows Spy [?e0]))"
5.78 + by (intro synth.intros(2,3,4,1)) eval+
5.79 + qed
5.80 + then have "[?e2, ?e1, ?e0] : ns_public"
5.81 + proof (rule NS2)
5.82 + show "Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}) \<in> set [?e1, ?e0]" by simp
5.83 + show " Nonce 1 ~: used [?e1, ?e0]" by eval
5.84 + qed
5.85 + then show "evs : ns_public"
5.86 + unfolding assms
5.87 + proof (rule NS3)
5.88 + show " Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|}) \<in> set [?e2, ?e1, ?e0]" by simp
5.89 + show "Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}) : set [?e2, ?e1, ?e0]" by simp
5.90 + qed
5.91 + from assms show "Nonce NB : analz (knows Spy evs)"
5.92 + apply simp
5.93 + apply (rule analz.intros(4))
5.94 + apply (rule analz.intros(1))
5.95 + apply (auto simp add: bad_def)
5.96 + done
5.97 +qed
5.98 +
5.99 +end
5.100 \ No newline at end of file
6.1 --- a/src/HOL/Quickcheck_Benchmark/ROOT.ML Tue Jul 31 12:38:01 2012 +0200
6.2 +++ b/src/HOL/Quickcheck_Benchmark/ROOT.ML Thu Jul 26 15:55:19 2012 +0200
6.3 @@ -1,1 +1,6 @@
6.4 -use_thys ["Find_Unused_Assms_Examples"]
6.5 +Unsynchronized.setmp quick_and_dirty true use_thys [
6.6 + "Find_Unused_Assms_Examples",
6.7 + "Needham_Schroeder_No_Attacker_Example",
6.8 + "Needham_Schroeder_Guided_Attacker_Example",
6.9 + "Needham_Schroeder_Unguided_Attacker_Example"
6.10 +]
7.1 --- a/src/HOL/Quickcheck_Examples/Needham_Schroeder_Base.thy Tue Jul 31 12:38:01 2012 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,200 +0,0 @@
7.4 -theory Needham_Schroeder_Base
7.5 -imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
7.6 -begin
7.7 -
7.8 -datatype agent = Alice | Bob | Spy
7.9 -
7.10 -definition agents :: "agent set"
7.11 -where
7.12 - "agents = {Spy, Alice, Bob}"
7.13 -
7.14 -definition bad :: "agent set"
7.15 -where
7.16 - "bad = {Spy}"
7.17 -
7.18 -datatype key = pubEK agent | priEK agent
7.19 -
7.20 -fun invKey
7.21 -where
7.22 - "invKey (pubEK A) = priEK A"
7.23 -| "invKey (priEK A) = pubEK A"
7.24 -
7.25 -datatype
7.26 - msg = Agent agent
7.27 - | Key key
7.28 - | Nonce nat
7.29 - | MPair msg msg
7.30 - | Crypt key msg
7.31 -
7.32 -syntax
7.33 - "_MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})")
7.34 -
7.35 -syntax (xsymbols)
7.36 - "_MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
7.37 -
7.38 -translations
7.39 - "{|x, y, z|}" == "{|x, {|y, z|}|}"
7.40 - "{|x, y|}" == "CONST MPair x y"
7.41 -
7.42 -inductive_set
7.43 - parts :: "msg set => msg set"
7.44 - for H :: "msg set"
7.45 - where
7.46 - Inj [intro]: "X \<in> H ==> X \<in> parts H"
7.47 - | Fst: "{|X,Y|} \<in> parts H ==> X \<in> parts H"
7.48 - | Snd: "{|X,Y|} \<in> parts H ==> Y \<in> parts H"
7.49 - | Body: "Crypt K X \<in> parts H ==> X \<in> parts H"
7.50 -
7.51 -inductive_set
7.52 - analz :: "msg set => msg set"
7.53 - for H :: "msg set"
7.54 - where
7.55 - Inj [intro,simp] : "X \<in> H ==> X \<in> analz H"
7.56 - | Fst: "{|X,Y|} \<in> analz H ==> X \<in> analz H"
7.57 - | Snd: "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
7.58 - | Decrypt [dest]:
7.59 - "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
7.60 -
7.61 -inductive_set
7.62 - synth :: "msg set => msg set"
7.63 - for H :: "msg set"
7.64 - where
7.65 - Inj [intro]: "X \<in> H ==> X \<in> synth H"
7.66 - | Agent [intro]: "Agent agt \<in> synth H"
7.67 - | MPair [intro]: "[|X \<in> synth H; Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
7.68 - | Crypt [intro]: "[|X \<in> synth H; Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
7.69 -
7.70 -primrec initState
7.71 -where
7.72 - initState_Alice:
7.73 - "initState Alice = {Key (priEK Alice)} \<union> (Key ` pubEK ` agents)"
7.74 -| initState_Bob:
7.75 - "initState Bob = {Key (priEK Bob)} \<union> (Key ` pubEK ` agents)"
7.76 -| initState_Spy:
7.77 - "initState Spy = (Key ` priEK ` bad) \<union> (Key ` pubEK ` agents)"
7.78 -
7.79 -datatype
7.80 - event = Says agent agent msg
7.81 - | Gets agent msg
7.82 - | Notes agent msg
7.83 -
7.84 -
7.85 -primrec knows :: "agent => event list => msg set"
7.86 -where
7.87 - knows_Nil: "knows A [] = initState A"
7.88 -| knows_Cons:
7.89 - "knows A (ev # evs) =
7.90 - (if A = Spy then
7.91 - (case ev of
7.92 - Says A' B X => insert X (knows Spy evs)
7.93 - | Gets A' X => knows Spy evs
7.94 - | Notes A' X =>
7.95 - if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs)
7.96 - else
7.97 - (case ev of
7.98 - Says A' B X =>
7.99 - if A'=A then insert X (knows A evs) else knows A evs
7.100 - | Gets A' X =>
7.101 - if A'=A then insert X (knows A evs) else knows A evs
7.102 - | Notes A' X =>
7.103 - if A'=A then insert X (knows A evs) else knows A evs))"
7.104 -
7.105 -abbreviation (input)
7.106 - spies :: "event list => msg set" where
7.107 - "spies == knows Spy"
7.108 -
7.109 -primrec used :: "event list => msg set"
7.110 -where
7.111 - used_Nil: "used [] = Union (parts ` initState ` agents)"
7.112 -| used_Cons: "used (ev # evs) =
7.113 - (case ev of
7.114 - Says A B X => parts {X} \<union> used evs
7.115 - | Gets A X => used evs
7.116 - | Notes A X => parts {X} \<union> used evs)"
7.117 -
7.118 -subsection {* Preparations for sets *}
7.119 -
7.120 -fun find_first :: "('a => 'b option) => 'a list => 'b option"
7.121 -where
7.122 - "find_first f [] = None"
7.123 -| "find_first f (x # xs) = (case f x of Some y => Some y | None => find_first f xs)"
7.124 -
7.125 -consts cps_of_set :: "'a set => ('a => term list option) => term list option"
7.126 -
7.127 -lemma
7.128 - [code]: "cps_of_set (set xs) f = find_first f xs"
7.129 -sorry
7.130 -
7.131 -consts pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => code_numeral => (bool * term list) option"
7.132 -consts neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => code_numeral => term list Quickcheck_Exhaustive.three_valued"
7.133 -
7.134 -lemma
7.135 - [code]: "pos_cps_of_set (set xs) f i = find_first f xs"
7.136 -sorry
7.137 -
7.138 -consts find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued)
7.139 - => 'b list => 'a Quickcheck_Exhaustive.three_valued"
7.140 -
7.141 -lemma [code]:
7.142 - "find_first' f [] = Quickcheck_Exhaustive.No_value"
7.143 - "find_first' f (x # xs) = (case f (Quickcheck_Exhaustive.Known x) of Quickcheck_Exhaustive.No_value => find_first' f xs | Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x | Quickcheck_Exhaustive.Unknown_value => (case find_first' f xs of Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x | _ => Quickcheck_Exhaustive.Unknown_value))"
7.144 -sorry
7.145 -
7.146 -lemma
7.147 - [code]: "neg_cps_of_set (set xs) f i = find_first' f xs"
7.148 -sorry
7.149 -
7.150 -setup {*
7.151 -let
7.152 - val Fun = Predicate_Compile_Aux.Fun
7.153 - val Input = Predicate_Compile_Aux.Input
7.154 - val Output = Predicate_Compile_Aux.Output
7.155 - val Bool = Predicate_Compile_Aux.Bool
7.156 - val oi = Fun (Output, Fun (Input, Bool))
7.157 - val ii = Fun (Input, Fun (Input, Bool))
7.158 - fun of_set compfuns (Type ("fun", [T, _])) =
7.159 - case body_type (Predicate_Compile_Aux.mk_monadT compfuns T) of
7.160 - Type ("Quickcheck_Exhaustive.three_valued", _) =>
7.161 - Const(@{const_name neg_cps_of_set}, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T))
7.162 - | Type ("Predicate.pred", _) => Const(@{const_name pred_of_set}, HOLogic.mk_setT T --> Predicate_Compile_Aux.mk_monadT compfuns T)
7.163 - | _ => Const(@{const_name pos_cps_of_set}, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T))
7.164 - fun member compfuns (U as Type ("fun", [T, _])) =
7.165 - (absdummy T (absdummy (HOLogic.mk_setT T) (Predicate_Compile_Aux.mk_if compfuns
7.166 - (Const (@{const_name "Set.member"}, T --> HOLogic.mk_setT T --> @{typ bool}) $ Bound 1 $ Bound 0))))
7.167 -
7.168 -in
7.169 - Core_Data.force_modes_and_compilations @{const_name Set.member}
7.170 - [(oi, (of_set, false)), (ii, (member, false))]
7.171 -end
7.172 -*}
7.173 -
7.174 -subsection {* Derived equations for analz, parts and synth *}
7.175 -
7.176 -lemma [code]:
7.177 - "analz H = (let
7.178 - H' = H \<union> (Union ((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => if Key (invKey K) : H then {X} else {} | _ => {}) ` H))
7.179 - in if H' = H then H else analz H')"
7.180 -sorry
7.181 -
7.182 -lemma [code]:
7.183 - "parts H = (let
7.184 - H' = H \<union> (Union ((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => {X} | _ => {}) ` H))
7.185 - in if H' = H then H else parts H')"
7.186 -sorry
7.187 -
7.188 -definition synth' :: "msg set => msg => bool"
7.189 -where
7.190 - "synth' H m = (m : synth H)"
7.191 -
7.192 -lemmas [code_pred_intro] = synth.intros[folded synth'_def]
7.193 -
7.194 -code_pred [generator_cps] synth' unfolding synth'_def by (rule synth.cases) fastforce+
7.195 -
7.196 -setup {* Predicate_Compile_Data.ignore_consts [@{const_name analz}, @{const_name knows}] *}
7.197 -declare ListMem_iff[symmetric, code_pred_inline]
7.198 -declare [[quickcheck_timing]]
7.199 -
7.200 -setup {* Exhaustive_Generators.setup_exhaustive_datatype_interpretation *}
7.201 -declare [[quickcheck_full_support = false]]
7.202 -
7.203 -end
7.204 \ No newline at end of file
8.1 --- a/src/HOL/Quickcheck_Examples/Needham_Schroeder_Guided_Attacker_Example.thy Tue Jul 31 12:38:01 2012 +0200
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,100 +0,0 @@
8.4 -theory Needham_Schroeder_Guided_Attacker_Example
8.5 -imports Needham_Schroeder_Base
8.6 -begin
8.7 -
8.8 -inductive_set ns_public :: "event list set"
8.9 - where
8.10 - (*Initial trace is empty*)
8.11 - Nil: "[] \<in> ns_public"
8.12 -
8.13 - | Fake_NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<in> analz (spies evs1) \<rbrakk>
8.14 - \<Longrightarrow> Says Spy B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
8.15 - # evs1 \<in> ns_public"
8.16 - | Fake_NS2: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<in> analz (spies evs1); Nonce NB \<in> analz (spies evs1) \<rbrakk>
8.17 - \<Longrightarrow> Says Spy A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
8.18 - # evs1 \<in> ns_public"
8.19 -
8.20 - (*Alice initiates a protocol run, sending a nonce to Bob*)
8.21 - | NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk>
8.22 - \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
8.23 - # evs1 \<in> ns_public"
8.24 - (*Bob responds to Alice's message with a further nonce*)
8.25 - | NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2;
8.26 - Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
8.27 - \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
8.28 - # evs2 \<in> ns_public"
8.29 -
8.30 - (*Alice proves her existence by sending NB back to Bob.*)
8.31 - | NS3: "\<lbrakk>evs3 \<in> ns_public;
8.32 - Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
8.33 - Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
8.34 - \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
8.35 -
8.36 -declare ListMem_iff[symmetric, code_pred_inline]
8.37 -
8.38 -lemmas [code_pred_intro] = ns_publicp.intros[folded synth'_def]
8.39 -
8.40 -code_pred [skip_proof] ns_publicp unfolding synth'_def by (rule ns_publicp.cases) fastforce+
8.41 -thm ns_publicp.equation
8.42 -
8.43 -code_pred [generator_cps] ns_publicp .
8.44 -thm ns_publicp.generator_cps_equation
8.45 -
8.46 -
8.47 -lemma "ns_publicp evs ==> \<not> (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs"
8.48 -quickcheck[smart_exhaustive, depth = 5, timeout = 100, expect = counterexample]
8.49 -(*quickcheck[narrowing, size = 6, timeout = 200, verbose, expect = no_counterexample]*)
8.50 -oops
8.51 -
8.52 -lemma
8.53 - "\<lbrakk>ns_publicp evs\<rbrakk>
8.54 - \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs
8.55 - \<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B
8.56 - \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
8.57 -(*quickcheck[smart_exhaustive, depth = 6, timeout = 100, expect = counterexample]
8.58 -quickcheck[narrowing, size = 7, timeout = 200, expect = no_counterexample]*)
8.59 -oops
8.60 -
8.61 -section {* Proving the counterexample trace for validation *}
8.62 -
8.63 -lemma
8.64 - assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1"
8.65 - assumes "evs =
8.66 - [Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)),
8.67 - Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}),
8.68 - Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}),
8.69 - Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|})]" (is "_ = [?e3, ?e2, ?e1, ?e0]")
8.70 - shows "A \<noteq> Spy" "B \<noteq> Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)"
8.71 -proof -
8.72 - from assms show "A \<noteq> Spy" by auto
8.73 - from assms show "B \<noteq> Spy" by auto
8.74 - have "[] : ns_public" by (rule Nil)
8.75 - then have first_step: "[?e0] : ns_public"
8.76 - proof (rule NS1)
8.77 - show "Nonce 0 ~: used []" by eval
8.78 - qed
8.79 - then have "[?e1, ?e0] : ns_public"
8.80 - proof (rule Fake_NS1)
8.81 - show "Nonce 0 : analz (knows Spy [?e0])" by eval
8.82 - qed
8.83 - then have "[?e2, ?e1, ?e0] : ns_public"
8.84 - proof (rule NS2)
8.85 - show "Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}) \<in> set [?e1, ?e0]" by simp
8.86 - show " Nonce 1 ~: used [?e1, ?e0]" by eval
8.87 - qed
8.88 - then show "evs : ns_public"
8.89 - unfolding assms
8.90 - proof (rule NS3)
8.91 - show " Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|}) \<in> set [?e2, ?e1, ?e0]" by simp
8.92 - show "Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|})
8.93 - : set [?e2, ?e1, ?e0]" by simp
8.94 - qed
8.95 - from assms show "Nonce NB : analz (knows Spy evs)"
8.96 - apply simp
8.97 - apply (rule analz.intros(4))
8.98 - apply (rule analz.intros(1))
8.99 - apply (auto simp add: bad_def)
8.100 - done
8.101 -qed
8.102 -
8.103 -end
8.104 \ No newline at end of file
9.1 --- a/src/HOL/Quickcheck_Examples/Needham_Schroeder_No_Attacker_Example.thy Tue Jul 31 12:38:01 2012 +0200
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,47 +0,0 @@
9.4 -theory Needham_Schroeder_No_Attacker_Example
9.5 -imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
9.6 -begin
9.7 -
9.8 -inductive_set ns_public :: "event list set"
9.9 - where
9.10 - (*Initial trace is empty*)
9.11 - Nil: "[] \<in> ns_public"
9.12 - (*Alice initiates a protocol run, sending a nonce to Bob*)
9.13 - | NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk>
9.14 - \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
9.15 - # evs1 \<in> ns_public"
9.16 - (*Bob responds to Alice's message with a further nonce*)
9.17 - | NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2;
9.18 - Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
9.19 - \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
9.20 - # evs2 \<in> ns_public"
9.21 -
9.22 - (*Alice proves her existence by sending NB back to Bob.*)
9.23 - | NS3: "\<lbrakk>evs3 \<in> ns_public;
9.24 - Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
9.25 - Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
9.26 - \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
9.27 -
9.28 -code_pred [skip_proof] ns_publicp .
9.29 -thm ns_publicp.equation
9.30 -
9.31 -code_pred [generator_cps] ns_publicp .
9.32 -thm ns_publicp.generator_cps_equation
9.33 -
9.34 -lemma "ns_publicp evs ==> \<not> (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs"
9.35 -(*quickcheck[random, iterations = 1000000, size = 20, timeout = 3600, verbose]
9.36 -quickcheck[exhaustive, size = 8, timeout = 3600, verbose]
9.37 -quickcheck[narrowing, size = 7, timeout = 3600, verbose]*)
9.38 -quickcheck[smart_exhaustive, depth = 5, timeout = 30, expect = counterexample]
9.39 -oops
9.40 -
9.41 -lemma
9.42 - "\<lbrakk>ns_publicp evs\<rbrakk>
9.43 - \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs
9.44 - \<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B
9.45 - \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
9.46 -quickcheck[smart_exhaustive, depth = 6, timeout = 30]
9.47 -quickcheck[narrowing, size = 6, timeout = 30, verbose]
9.48 -oops
9.49 -
9.50 -end
9.51 \ No newline at end of file
10.1 --- a/src/HOL/Quickcheck_Examples/Needham_Schroeder_Unguided_Attacker_Example.thy Tue Jul 31 12:38:01 2012 +0200
10.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
10.3 @@ -1,96 +0,0 @@
10.4 -theory Needham_Schroeder_Unguided_Attacker_Example
10.5 -imports Needham_Schroeder_Base
10.6 -begin
10.7 -
10.8 -inductive_set ns_public :: "event list set"
10.9 - where
10.10 - (*Initial trace is empty*)
10.11 - Nil: "[] \<in> ns_public"
10.12 -
10.13 - | Fake: "\<lbrakk>evs1 \<in> ns_public; X \<in> synth (analz (spies evs1)) \<rbrakk>
10.14 - \<Longrightarrow> Says Spy A X # evs1 \<in> ns_public"
10.15 -
10.16 - (*Alice initiates a protocol run, sending a nonce to Bob*)
10.17 - | NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk>
10.18 - \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
10.19 - # evs1 \<in> ns_public"
10.20 - (*Bob responds to Alice's message with a further nonce*)
10.21 - | NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2;
10.22 - Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
10.23 - \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
10.24 - # evs2 \<in> ns_public"
10.25 -
10.26 - (*Alice proves her existence by sending NB back to Bob.*)
10.27 - | NS3: "\<lbrakk>evs3 \<in> ns_public;
10.28 - Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
10.29 - Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
10.30 - \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
10.31 -
10.32 -declare ListMem_iff[symmetric, code_pred_inline]
10.33 -
10.34 -lemmas [code_pred_intro] = ns_publicp.intros[folded synth'_def]
10.35 -
10.36 -code_pred [skip_proof] ns_publicp unfolding synth'_def by (rule ns_publicp.cases) fastforce+
10.37 -thm ns_publicp.equation
10.38 -
10.39 -code_pred [generator_cps] ns_publicp .
10.40 -thm ns_publicp.generator_cps_equation
10.41 -
10.42 -
10.43 -lemma "ns_publicp evs ==> \<not> (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs"
10.44 -quickcheck[smart_exhaustive, depth = 5, timeout = 200, expect = counterexample]
10.45 -(*quickcheck[narrowing, size = 6, timeout = 200, verbose, expect = no_counterexample]*)
10.46 -oops
10.47 -
10.48 -lemma
10.49 - "\<lbrakk>ns_publicp evs\<rbrakk>
10.50 - \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs
10.51 - \<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B
10.52 - \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
10.53 -quickcheck[smart_exhaustive, depth = 6, timeout = 100, expect = no_counterexample]
10.54 -(*quickcheck[narrowing, size = 7, timeout = 200, expect = no_counterexample]*)
10.55 -oops
10.56 -
10.57 -section {* Proving the counterexample trace for validation *}
10.58 -
10.59 -lemma
10.60 - assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1"
10.61 - assumes "evs =
10.62 - [Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)),
10.63 - Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}),
10.64 - Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}),
10.65 - Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|})]" (is "_ = [?e3, ?e2, ?e1, ?e0]")
10.66 - shows "A \<noteq> Spy" "B \<noteq> Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)"
10.67 -proof -
10.68 - from assms show "A \<noteq> Spy" by auto
10.69 - from assms show "B \<noteq> Spy" by auto
10.70 - have "[] : ns_public" by (rule Nil)
10.71 - then have first_step: "[?e0] : ns_public"
10.72 - proof (rule NS1)
10.73 - show "Nonce 0 ~: used []" by eval
10.74 - qed
10.75 - then have "[?e1, ?e0] : ns_public"
10.76 - proof (rule Fake)
10.77 - show "Crypt (pubEK Bob) {|Nonce 0, Agent Alice|} : synth (analz (knows Spy [?e0]))"
10.78 - by (intro synth.intros(2,3,4,1)) eval+
10.79 - qed
10.80 - then have "[?e2, ?e1, ?e0] : ns_public"
10.81 - proof (rule NS2)
10.82 - show "Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}) \<in> set [?e1, ?e0]" by simp
10.83 - show " Nonce 1 ~: used [?e1, ?e0]" by eval
10.84 - qed
10.85 - then show "evs : ns_public"
10.86 - unfolding assms
10.87 - proof (rule NS3)
10.88 - show " Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|}) \<in> set [?e2, ?e1, ?e0]" by simp
10.89 - show "Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}) : set [?e2, ?e1, ?e0]" by simp
10.90 - qed
10.91 - from assms show "Nonce NB : analz (knows Spy evs)"
10.92 - apply simp
10.93 - apply (rule analz.intros(4))
10.94 - apply (rule analz.intros(1))
10.95 - apply (auto simp add: bad_def)
10.96 - done
10.97 -qed
10.98 -
10.99 -end
10.100 \ No newline at end of file
11.1 --- a/src/HOL/Quickcheck_Examples/ROOT.ML Tue Jul 31 12:38:01 2012 +0200
11.2 +++ b/src/HOL/Quickcheck_Examples/ROOT.ML Thu Jul 26 15:55:19 2012 +0200
11.3 @@ -1,14 +1,10 @@
11.4 use_thys [
11.5 -(* "Find_Unused_Assms_Examples", *)
11.6 "Quickcheck_Examples"
11.7 (*,
11.8 "Quickcheck_Lattice_Examples",
11.9 "Completeness",
11.10 "Quickcheck_Interfaces",
11.11 - "Hotel_Example",
11.12 - "Needham_Schroeder_No_Attacker_Example",
11.13 - "Needham_Schroeder_Guided_Attacker_Example",
11.14 - "Needham_Schroeder_Unguided_Attacker_Example"*)
11.15 + "Hotel_Example",*)
11.16 ];
11.17
11.18 if getenv "ISABELLE_GHC" = "" then ()
12.1 --- a/src/HOL/ROOT Tue Jul 31 12:38:01 2012 +0200
12.2 +++ b/src/HOL/ROOT Thu Jul 26 15:55:19 2012 +0200
12.3 @@ -740,8 +740,11 @@
12.4 Quickcheck_Narrowing_Examples
12.5
12.6 session Quickcheck_Benchmark = HOL +
12.7 - theories [condition = ISABELLE_BENCHMARK]
12.8 - Find_Unused_Assms_Examples (* FIXME more *)
12.9 + theories [condition = ISABELLE_BENCHMARK, quick_and_dirty]
12.10 + Find_Unused_Assms_Examples
12.11 + Needham_Schroeder_No_Attacker_Example
12.12 + Needham_Schroeder_Guided_Attacker_Example
12.13 + Needham_Schroeder_Unguided_Attacker_Example (* FIXME more *)
12.14
12.15 session Quotient_Examples = HOL +
12.16 description {*