# HG changeset patch # User bulwahn # Date 1343310919 -7200 # Node ID 1f7e068b46130de488cfde9b0a22c135c83d96aa # Parent 6004f45756456952f73567fc77bfa4575052b4e9 moved another larger quickcheck example to Quickcheck_Benchmark diff -r 6004f4575645 -r 1f7e068b4613 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Jul 31 12:38:01 2012 +0200 +++ b/src/HOL/IsaMakefile Thu Jul 26 15:55:19 2012 +0200 @@ -1513,10 +1513,6 @@ Quickcheck_Examples/ROOT.ML \ Quickcheck_Examples/Completeness.thy \ Quickcheck_Examples/Hotel_Example.thy \ - Quickcheck_Examples/Needham_Schroeder_Base.thy \ - Quickcheck_Examples/Needham_Schroeder_No_Attacker_Example.thy \ - Quickcheck_Examples/Needham_Schroeder_Guided_Attacker_Example.thy \ - Quickcheck_Examples/Needham_Schroeder_Unguided_Attacker_Example.thy \ Quickcheck_Examples/Quickcheck_Examples.thy \ Quickcheck_Examples/Quickcheck_Interfaces.thy \ Quickcheck_Examples/Quickcheck_Lattice_Examples.thy \ @@ -1823,6 +1819,10 @@ $(LOG)/HOL-Quickcheck_Benchmark.gz: $(OUT)/HOL \ Quickcheck_Benchmark/ROOT.ML \ + Quickcheck_Benchmark/Needham_Schroeder_Base.thy \ + Quickcheck_Benchmark/Needham_Schroeder_No_Attacker_Example.thy \ + Quickcheck_Benchmark/Needham_Schroeder_Guided_Attacker_Example.thy \ + Quickcheck_Benchmark/Needham_Schroeder_Unguided_Attacker_Example.thy \ Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy @$(ISABELLE_TOOL) usedir $(OUT)/HOL Quickcheck_Benchmark diff -r 6004f4575645 -r 1f7e068b4613 src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Thu Jul 26 15:55:19 2012 +0200 @@ -0,0 +1,200 @@ +theory Needham_Schroeder_Base +imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck" +begin + +datatype agent = Alice | Bob | Spy + +definition agents :: "agent set" +where + "agents = {Spy, Alice, Bob}" + +definition bad :: "agent set" +where + "bad = {Spy}" + +datatype key = pubEK agent | priEK agent + +fun invKey +where + "invKey (pubEK A) = priEK A" +| "invKey (priEK A) = pubEK A" + +datatype + msg = Agent agent + | Key key + | Nonce nat + | MPair msg msg + | Crypt key msg + +syntax + "_MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})") + +syntax (xsymbols) + "_MTuple" :: "['a, args] => 'a * 'b" ("(2\_,/ _\)") + +translations + "{|x, y, z|}" == "{|x, {|y, z|}|}" + "{|x, y|}" == "CONST MPair x y" + +inductive_set + parts :: "msg set => msg set" + for H :: "msg set" + where + Inj [intro]: "X \ H ==> X \ parts H" + | Fst: "{|X,Y|} \ parts H ==> X \ parts H" + | Snd: "{|X,Y|} \ parts H ==> Y \ parts H" + | Body: "Crypt K X \ parts H ==> X \ parts H" + +inductive_set + analz :: "msg set => msg set" + for H :: "msg set" + where + Inj [intro,simp] : "X \ H ==> X \ analz H" + | Fst: "{|X,Y|} \ analz H ==> X \ analz H" + | Snd: "{|X,Y|} \ analz H ==> Y \ analz H" + | Decrypt [dest]: + "[|Crypt K X \ analz H; Key(invKey K): analz H|] ==> X \ analz H" + +inductive_set + synth :: "msg set => msg set" + for H :: "msg set" + where + Inj [intro]: "X \ H ==> X \ synth H" + | Agent [intro]: "Agent agt \ synth H" + | MPair [intro]: "[|X \ synth H; Y \ synth H|] ==> {|X,Y|} \ synth H" + | Crypt [intro]: "[|X \ synth H; Key(K) \ H|] ==> Crypt K X \ synth H" + +primrec initState +where + initState_Alice: + "initState Alice = {Key (priEK Alice)} \ (Key ` pubEK ` agents)" +| initState_Bob: + "initState Bob = {Key (priEK Bob)} \ (Key ` pubEK ` agents)" +| initState_Spy: + "initState Spy = (Key ` priEK ` bad) \ (Key ` pubEK ` agents)" + +datatype + event = Says agent agent msg + | Gets agent msg + | Notes agent msg + + +primrec knows :: "agent => event list => msg set" +where + knows_Nil: "knows A [] = initState A" +| knows_Cons: + "knows A (ev # evs) = + (if A = Spy then + (case ev of + Says A' B X => insert X (knows Spy evs) + | Gets A' X => knows Spy evs + | Notes A' X => + if A' \ bad then insert X (knows Spy evs) else knows Spy evs) + else + (case ev of + Says A' B X => + if A'=A then insert X (knows A evs) else knows A evs + | Gets A' X => + if A'=A then insert X (knows A evs) else knows A evs + | Notes A' X => + if A'=A then insert X (knows A evs) else knows A evs))" + +abbreviation (input) + spies :: "event list => msg set" where + "spies == knows Spy" + +primrec used :: "event list => msg set" +where + used_Nil: "used [] = Union (parts ` initState ` agents)" +| used_Cons: "used (ev # evs) = + (case ev of + Says A B X => parts {X} \ used evs + | Gets A X => used evs + | Notes A X => parts {X} \ used evs)" + +subsection {* Preparations for sets *} + +fun find_first :: "('a => 'b option) => 'a list => 'b option" +where + "find_first f [] = None" +| "find_first f (x # xs) = (case f x of Some y => Some y | None => find_first f xs)" + +consts cps_of_set :: "'a set => ('a => term list option) => term list option" + +lemma + [code]: "cps_of_set (set xs) f = find_first f xs" +sorry + +consts pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => code_numeral => (bool * term list) option" +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" + +lemma + [code]: "pos_cps_of_set (set xs) f i = find_first f xs" +sorry + +consts find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued) + => 'b list => 'a Quickcheck_Exhaustive.three_valued" + +lemma [code]: + "find_first' f [] = Quickcheck_Exhaustive.No_value" + "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))" +sorry + +lemma + [code]: "neg_cps_of_set (set xs) f i = find_first' f xs" +sorry + +setup {* +let + val Fun = Predicate_Compile_Aux.Fun + val Input = Predicate_Compile_Aux.Input + val Output = Predicate_Compile_Aux.Output + val Bool = Predicate_Compile_Aux.Bool + val oi = Fun (Output, Fun (Input, Bool)) + val ii = Fun (Input, Fun (Input, Bool)) + fun of_set compfuns (Type ("fun", [T, _])) = + case body_type (Predicate_Compile_Aux.mk_monadT compfuns T) of + Type ("Quickcheck_Exhaustive.three_valued", _) => + Const(@{const_name neg_cps_of_set}, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T)) + | Type ("Predicate.pred", _) => Const(@{const_name pred_of_set}, HOLogic.mk_setT T --> Predicate_Compile_Aux.mk_monadT compfuns T) + | _ => Const(@{const_name pos_cps_of_set}, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T)) + fun member compfuns (U as Type ("fun", [T, _])) = + (absdummy T (absdummy (HOLogic.mk_setT T) (Predicate_Compile_Aux.mk_if compfuns + (Const (@{const_name "Set.member"}, T --> HOLogic.mk_setT T --> @{typ bool}) $ Bound 1 $ Bound 0)))) + +in + Core_Data.force_modes_and_compilations @{const_name Set.member} + [(oi, (of_set, false)), (ii, (member, false))] +end +*} + +subsection {* Derived equations for analz, parts and synth *} + +lemma [code]: + "analz H = (let + H' = H \ (Union ((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => if Key (invKey K) : H then {X} else {} | _ => {}) ` H)) + in if H' = H then H else analz H')" +sorry + +lemma [code]: + "parts H = (let + H' = H \ (Union ((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => {X} | _ => {}) ` H)) + in if H' = H then H else parts H')" +sorry + +definition synth' :: "msg set => msg => bool" +where + "synth' H m = (m : synth H)" + +lemmas [code_pred_intro] = synth.intros[folded synth'_def] + +code_pred [generator_cps] synth' unfolding synth'_def by (rule synth.cases) fastforce+ + +setup {* Predicate_Compile_Data.ignore_consts [@{const_name analz}, @{const_name knows}] *} +declare ListMem_iff[symmetric, code_pred_inline] +declare [[quickcheck_timing]] + +setup {* Exhaustive_Generators.setup_exhaustive_datatype_interpretation *} +declare [[quickcheck_full_support = false]] + +end \ No newline at end of file diff -r 6004f4575645 -r 1f7e068b4613 src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Guided_Attacker_Example.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Guided_Attacker_Example.thy Thu Jul 26 15:55:19 2012 +0200 @@ -0,0 +1,100 @@ +theory Needham_Schroeder_Guided_Attacker_Example +imports Needham_Schroeder_Base +begin + +inductive_set ns_public :: "event list set" + where + (*Initial trace is empty*) + Nil: "[] \ ns_public" + + | Fake_NS1: "\evs1 \ ns_public; Nonce NA \ analz (spies evs1) \ + \ Says Spy B (Crypt (pubEK B) \Nonce NA, Agent A\) + # evs1 \ ns_public" + | Fake_NS2: "\evs1 \ ns_public; Nonce NA \ analz (spies evs1); Nonce NB \ analz (spies evs1) \ + \ Says Spy A (Crypt (pubEK A) \Nonce NA, Nonce NB\) + # evs1 \ ns_public" + + (*Alice initiates a protocol run, sending a nonce to Bob*) + | NS1: "\evs1 \ ns_public; Nonce NA \ used evs1\ + \ Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) + # evs1 \ ns_public" + (*Bob responds to Alice's message with a further nonce*) + | NS2: "\evs2 \ ns_public; Nonce NB \ used evs2; + Says A' B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs2\ + \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) + # evs2 \ ns_public" + + (*Alice proves her existence by sending NB back to Bob.*) + | NS3: "\evs3 \ ns_public; + Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs3; + Says B' A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs3\ + \ Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \ ns_public" + +declare ListMem_iff[symmetric, code_pred_inline] + +lemmas [code_pred_intro] = ns_publicp.intros[folded synth'_def] + +code_pred [skip_proof] ns_publicp unfolding synth'_def by (rule ns_publicp.cases) fastforce+ +thm ns_publicp.equation + +code_pred [generator_cps] ns_publicp . +thm ns_publicp.generator_cps_equation + + +lemma "ns_publicp evs ==> \ (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs" +quickcheck[smart_exhaustive, depth = 5, timeout = 100, expect = counterexample] +(*quickcheck[narrowing, size = 6, timeout = 200, verbose, expect = no_counterexample]*) +oops + +lemma + "\ns_publicp evs\ + \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) : set evs + \ A \ Spy \ B \ Spy \ A \ B + \ Nonce NB \ analz (spies evs)" +(*quickcheck[smart_exhaustive, depth = 6, timeout = 100, expect = counterexample] +quickcheck[narrowing, size = 7, timeout = 200, expect = no_counterexample]*) +oops + +section {* Proving the counterexample trace for validation *} + +lemma + assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1" + assumes "evs = + [Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)), + Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}), + Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}), + Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|})]" (is "_ = [?e3, ?e2, ?e1, ?e0]") + shows "A \ Spy" "B \ Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)" +proof - + from assms show "A \ Spy" by auto + from assms show "B \ Spy" by auto + have "[] : ns_public" by (rule Nil) + then have first_step: "[?e0] : ns_public" + proof (rule NS1) + show "Nonce 0 ~: used []" by eval + qed + then have "[?e1, ?e0] : ns_public" + proof (rule Fake_NS1) + show "Nonce 0 : analz (knows Spy [?e0])" by eval + qed + then have "[?e2, ?e1, ?e0] : ns_public" + proof (rule NS2) + show "Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}) \ set [?e1, ?e0]" by simp + show " Nonce 1 ~: used [?e1, ?e0]" by eval + qed + then show "evs : ns_public" + unfolding assms + proof (rule NS3) + show " Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|}) \ set [?e2, ?e1, ?e0]" by simp + show "Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}) + : set [?e2, ?e1, ?e0]" by simp + qed + from assms show "Nonce NB : analz (knows Spy evs)" + apply simp + apply (rule analz.intros(4)) + apply (rule analz.intros(1)) + apply (auto simp add: bad_def) + done +qed + +end \ No newline at end of file diff -r 6004f4575645 -r 1f7e068b4613 src/HOL/Quickcheck_Benchmark/Needham_Schroeder_No_Attacker_Example.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_No_Attacker_Example.thy Thu Jul 26 15:55:19 2012 +0200 @@ -0,0 +1,47 @@ +theory Needham_Schroeder_No_Attacker_Example +imports Needham_Schroeder_Base +begin + +inductive_set ns_public :: "event list set" + where + (*Initial trace is empty*) + Nil: "[] \ ns_public" + (*Alice initiates a protocol run, sending a nonce to Bob*) + | NS1: "\evs1 \ ns_public; Nonce NA \ used evs1\ + \ Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) + # evs1 \ ns_public" + (*Bob responds to Alice's message with a further nonce*) + | NS2: "\evs2 \ ns_public; Nonce NB \ used evs2; + Says A' B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs2\ + \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) + # evs2 \ ns_public" + + (*Alice proves her existence by sending NB back to Bob.*) + | NS3: "\evs3 \ ns_public; + Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs3; + Says B' A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs3\ + \ Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \ ns_public" + +code_pred [skip_proof] ns_publicp . +thm ns_publicp.equation + +code_pred [generator_cps] ns_publicp . +thm ns_publicp.generator_cps_equation + +lemma "ns_publicp evs ==> \ (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs" +(*quickcheck[random, iterations = 1000000, size = 20, timeout = 3600, verbose] +quickcheck[exhaustive, size = 8, timeout = 3600, verbose] +quickcheck[narrowing, size = 7, timeout = 3600, verbose]*) +quickcheck[smart_exhaustive, depth = 5, timeout = 30, expect = counterexample] +oops + +lemma + "\ns_publicp evs\ + \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) : set evs + \ A \ Spy \ B \ Spy \ A \ B + \ Nonce NB \ analz (spies evs)" +quickcheck[smart_exhaustive, depth = 6, timeout = 30] +quickcheck[narrowing, size = 6, timeout = 30, verbose] +oops + +end diff -r 6004f4575645 -r 1f7e068b4613 src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Unguided_Attacker_Example.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Unguided_Attacker_Example.thy Thu Jul 26 15:55:19 2012 +0200 @@ -0,0 +1,96 @@ +theory Needham_Schroeder_Unguided_Attacker_Example +imports Needham_Schroeder_Base +begin + +inductive_set ns_public :: "event list set" + where + (*Initial trace is empty*) + Nil: "[] \ ns_public" + + | Fake: "\evs1 \ ns_public; X \ synth (analz (spies evs1)) \ + \ Says Spy A X # evs1 \ ns_public" + + (*Alice initiates a protocol run, sending a nonce to Bob*) + | NS1: "\evs1 \ ns_public; Nonce NA \ used evs1\ + \ Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) + # evs1 \ ns_public" + (*Bob responds to Alice's message with a further nonce*) + | NS2: "\evs2 \ ns_public; Nonce NB \ used evs2; + Says A' B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs2\ + \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) + # evs2 \ ns_public" + + (*Alice proves her existence by sending NB back to Bob.*) + | NS3: "\evs3 \ ns_public; + Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs3; + Says B' A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs3\ + \ Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \ ns_public" + +declare ListMem_iff[symmetric, code_pred_inline] + +lemmas [code_pred_intro] = ns_publicp.intros[folded synth'_def] + +code_pred [skip_proof] ns_publicp unfolding synth'_def by (rule ns_publicp.cases) fastforce+ +thm ns_publicp.equation + +code_pred [generator_cps] ns_publicp . +thm ns_publicp.generator_cps_equation + + +lemma "ns_publicp evs ==> \ (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs" +quickcheck[smart_exhaustive, depth = 5, timeout = 200, expect = counterexample] +(*quickcheck[narrowing, size = 6, timeout = 200, verbose, expect = no_counterexample]*) +oops + +lemma + "\ns_publicp evs\ + \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) : set evs + \ A \ Spy \ B \ Spy \ A \ B + \ Nonce NB \ analz (spies evs)" +quickcheck[smart_exhaustive, depth = 6, timeout = 100, expect = no_counterexample] +(*quickcheck[narrowing, size = 7, timeout = 200, expect = no_counterexample]*) +oops + +section {* Proving the counterexample trace for validation *} + +lemma + assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1" + assumes "evs = + [Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)), + Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}), + Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}), + Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|})]" (is "_ = [?e3, ?e2, ?e1, ?e0]") + shows "A \ Spy" "B \ Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)" +proof - + from assms show "A \ Spy" by auto + from assms show "B \ Spy" by auto + have "[] : ns_public" by (rule Nil) + then have first_step: "[?e0] : ns_public" + proof (rule NS1) + show "Nonce 0 ~: used []" by eval + qed + then have "[?e1, ?e0] : ns_public" + proof (rule Fake) + show "Crypt (pubEK Bob) {|Nonce 0, Agent Alice|} : synth (analz (knows Spy [?e0]))" + by (intro synth.intros(2,3,4,1)) eval+ + qed + then have "[?e2, ?e1, ?e0] : ns_public" + proof (rule NS2) + show "Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}) \ set [?e1, ?e0]" by simp + show " Nonce 1 ~: used [?e1, ?e0]" by eval + qed + then show "evs : ns_public" + unfolding assms + proof (rule NS3) + show " Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|}) \ set [?e2, ?e1, ?e0]" by simp + show "Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}) : set [?e2, ?e1, ?e0]" by simp + qed + from assms show "Nonce NB : analz (knows Spy evs)" + apply simp + apply (rule analz.intros(4)) + apply (rule analz.intros(1)) + apply (auto simp add: bad_def) + done +qed + +end \ No newline at end of file diff -r 6004f4575645 -r 1f7e068b4613 src/HOL/Quickcheck_Benchmark/ROOT.ML --- a/src/HOL/Quickcheck_Benchmark/ROOT.ML Tue Jul 31 12:38:01 2012 +0200 +++ b/src/HOL/Quickcheck_Benchmark/ROOT.ML Thu Jul 26 15:55:19 2012 +0200 @@ -1,1 +1,6 @@ -use_thys ["Find_Unused_Assms_Examples"] +Unsynchronized.setmp quick_and_dirty true use_thys [ + "Find_Unused_Assms_Examples", + "Needham_Schroeder_No_Attacker_Example", + "Needham_Schroeder_Guided_Attacker_Example", + "Needham_Schroeder_Unguided_Attacker_Example" +] diff -r 6004f4575645 -r 1f7e068b4613 src/HOL/Quickcheck_Examples/Needham_Schroeder_Base.thy --- a/src/HOL/Quickcheck_Examples/Needham_Schroeder_Base.thy Tue Jul 31 12:38:01 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,200 +0,0 @@ -theory Needham_Schroeder_Base -imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck" -begin - -datatype agent = Alice | Bob | Spy - -definition agents :: "agent set" -where - "agents = {Spy, Alice, Bob}" - -definition bad :: "agent set" -where - "bad = {Spy}" - -datatype key = pubEK agent | priEK agent - -fun invKey -where - "invKey (pubEK A) = priEK A" -| "invKey (priEK A) = pubEK A" - -datatype - msg = Agent agent - | Key key - | Nonce nat - | MPair msg msg - | Crypt key msg - -syntax - "_MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})") - -syntax (xsymbols) - "_MTuple" :: "['a, args] => 'a * 'b" ("(2\_,/ _\)") - -translations - "{|x, y, z|}" == "{|x, {|y, z|}|}" - "{|x, y|}" == "CONST MPair x y" - -inductive_set - parts :: "msg set => msg set" - for H :: "msg set" - where - Inj [intro]: "X \ H ==> X \ parts H" - | Fst: "{|X,Y|} \ parts H ==> X \ parts H" - | Snd: "{|X,Y|} \ parts H ==> Y \ parts H" - | Body: "Crypt K X \ parts H ==> X \ parts H" - -inductive_set - analz :: "msg set => msg set" - for H :: "msg set" - where - Inj [intro,simp] : "X \ H ==> X \ analz H" - | Fst: "{|X,Y|} \ analz H ==> X \ analz H" - | Snd: "{|X,Y|} \ analz H ==> Y \ analz H" - | Decrypt [dest]: - "[|Crypt K X \ analz H; Key(invKey K): analz H|] ==> X \ analz H" - -inductive_set - synth :: "msg set => msg set" - for H :: "msg set" - where - Inj [intro]: "X \ H ==> X \ synth H" - | Agent [intro]: "Agent agt \ synth H" - | MPair [intro]: "[|X \ synth H; Y \ synth H|] ==> {|X,Y|} \ synth H" - | Crypt [intro]: "[|X \ synth H; Key(K) \ H|] ==> Crypt K X \ synth H" - -primrec initState -where - initState_Alice: - "initState Alice = {Key (priEK Alice)} \ (Key ` pubEK ` agents)" -| initState_Bob: - "initState Bob = {Key (priEK Bob)} \ (Key ` pubEK ` agents)" -| initState_Spy: - "initState Spy = (Key ` priEK ` bad) \ (Key ` pubEK ` agents)" - -datatype - event = Says agent agent msg - | Gets agent msg - | Notes agent msg - - -primrec knows :: "agent => event list => msg set" -where - knows_Nil: "knows A [] = initState A" -| knows_Cons: - "knows A (ev # evs) = - (if A = Spy then - (case ev of - Says A' B X => insert X (knows Spy evs) - | Gets A' X => knows Spy evs - | Notes A' X => - if A' \ bad then insert X (knows Spy evs) else knows Spy evs) - else - (case ev of - Says A' B X => - if A'=A then insert X (knows A evs) else knows A evs - | Gets A' X => - if A'=A then insert X (knows A evs) else knows A evs - | Notes A' X => - if A'=A then insert X (knows A evs) else knows A evs))" - -abbreviation (input) - spies :: "event list => msg set" where - "spies == knows Spy" - -primrec used :: "event list => msg set" -where - used_Nil: "used [] = Union (parts ` initState ` agents)" -| used_Cons: "used (ev # evs) = - (case ev of - Says A B X => parts {X} \ used evs - | Gets A X => used evs - | Notes A X => parts {X} \ used evs)" - -subsection {* Preparations for sets *} - -fun find_first :: "('a => 'b option) => 'a list => 'b option" -where - "find_first f [] = None" -| "find_first f (x # xs) = (case f x of Some y => Some y | None => find_first f xs)" - -consts cps_of_set :: "'a set => ('a => term list option) => term list option" - -lemma - [code]: "cps_of_set (set xs) f = find_first f xs" -sorry - -consts pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => code_numeral => (bool * term list) option" -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" - -lemma - [code]: "pos_cps_of_set (set xs) f i = find_first f xs" -sorry - -consts find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued) - => 'b list => 'a Quickcheck_Exhaustive.three_valued" - -lemma [code]: - "find_first' f [] = Quickcheck_Exhaustive.No_value" - "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))" -sorry - -lemma - [code]: "neg_cps_of_set (set xs) f i = find_first' f xs" -sorry - -setup {* -let - val Fun = Predicate_Compile_Aux.Fun - val Input = Predicate_Compile_Aux.Input - val Output = Predicate_Compile_Aux.Output - val Bool = Predicate_Compile_Aux.Bool - val oi = Fun (Output, Fun (Input, Bool)) - val ii = Fun (Input, Fun (Input, Bool)) - fun of_set compfuns (Type ("fun", [T, _])) = - case body_type (Predicate_Compile_Aux.mk_monadT compfuns T) of - Type ("Quickcheck_Exhaustive.three_valued", _) => - Const(@{const_name neg_cps_of_set}, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T)) - | Type ("Predicate.pred", _) => Const(@{const_name pred_of_set}, HOLogic.mk_setT T --> Predicate_Compile_Aux.mk_monadT compfuns T) - | _ => Const(@{const_name pos_cps_of_set}, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T)) - fun member compfuns (U as Type ("fun", [T, _])) = - (absdummy T (absdummy (HOLogic.mk_setT T) (Predicate_Compile_Aux.mk_if compfuns - (Const (@{const_name "Set.member"}, T --> HOLogic.mk_setT T --> @{typ bool}) $ Bound 1 $ Bound 0)))) - -in - Core_Data.force_modes_and_compilations @{const_name Set.member} - [(oi, (of_set, false)), (ii, (member, false))] -end -*} - -subsection {* Derived equations for analz, parts and synth *} - -lemma [code]: - "analz H = (let - H' = H \ (Union ((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => if Key (invKey K) : H then {X} else {} | _ => {}) ` H)) - in if H' = H then H else analz H')" -sorry - -lemma [code]: - "parts H = (let - H' = H \ (Union ((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => {X} | _ => {}) ` H)) - in if H' = H then H else parts H')" -sorry - -definition synth' :: "msg set => msg => bool" -where - "synth' H m = (m : synth H)" - -lemmas [code_pred_intro] = synth.intros[folded synth'_def] - -code_pred [generator_cps] synth' unfolding synth'_def by (rule synth.cases) fastforce+ - -setup {* Predicate_Compile_Data.ignore_consts [@{const_name analz}, @{const_name knows}] *} -declare ListMem_iff[symmetric, code_pred_inline] -declare [[quickcheck_timing]] - -setup {* Exhaustive_Generators.setup_exhaustive_datatype_interpretation *} -declare [[quickcheck_full_support = false]] - -end \ No newline at end of file diff -r 6004f4575645 -r 1f7e068b4613 src/HOL/Quickcheck_Examples/Needham_Schroeder_Guided_Attacker_Example.thy --- a/src/HOL/Quickcheck_Examples/Needham_Schroeder_Guided_Attacker_Example.thy Tue Jul 31 12:38:01 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,100 +0,0 @@ -theory Needham_Schroeder_Guided_Attacker_Example -imports Needham_Schroeder_Base -begin - -inductive_set ns_public :: "event list set" - where - (*Initial trace is empty*) - Nil: "[] \ ns_public" - - | Fake_NS1: "\evs1 \ ns_public; Nonce NA \ analz (spies evs1) \ - \ Says Spy B (Crypt (pubEK B) \Nonce NA, Agent A\) - # evs1 \ ns_public" - | Fake_NS2: "\evs1 \ ns_public; Nonce NA \ analz (spies evs1); Nonce NB \ analz (spies evs1) \ - \ Says Spy A (Crypt (pubEK A) \Nonce NA, Nonce NB\) - # evs1 \ ns_public" - - (*Alice initiates a protocol run, sending a nonce to Bob*) - | NS1: "\evs1 \ ns_public; Nonce NA \ used evs1\ - \ Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) - # evs1 \ ns_public" - (*Bob responds to Alice's message with a further nonce*) - | NS2: "\evs2 \ ns_public; Nonce NB \ used evs2; - Says A' B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs2\ - \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) - # evs2 \ ns_public" - - (*Alice proves her existence by sending NB back to Bob.*) - | NS3: "\evs3 \ ns_public; - Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs3; - Says B' A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs3\ - \ Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \ ns_public" - -declare ListMem_iff[symmetric, code_pred_inline] - -lemmas [code_pred_intro] = ns_publicp.intros[folded synth'_def] - -code_pred [skip_proof] ns_publicp unfolding synth'_def by (rule ns_publicp.cases) fastforce+ -thm ns_publicp.equation - -code_pred [generator_cps] ns_publicp . -thm ns_publicp.generator_cps_equation - - -lemma "ns_publicp evs ==> \ (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs" -quickcheck[smart_exhaustive, depth = 5, timeout = 100, expect = counterexample] -(*quickcheck[narrowing, size = 6, timeout = 200, verbose, expect = no_counterexample]*) -oops - -lemma - "\ns_publicp evs\ - \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) : set evs - \ A \ Spy \ B \ Spy \ A \ B - \ Nonce NB \ analz (spies evs)" -(*quickcheck[smart_exhaustive, depth = 6, timeout = 100, expect = counterexample] -quickcheck[narrowing, size = 7, timeout = 200, expect = no_counterexample]*) -oops - -section {* Proving the counterexample trace for validation *} - -lemma - assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1" - assumes "evs = - [Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)), - Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}), - Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}), - Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|})]" (is "_ = [?e3, ?e2, ?e1, ?e0]") - shows "A \ Spy" "B \ Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)" -proof - - from assms show "A \ Spy" by auto - from assms show "B \ Spy" by auto - have "[] : ns_public" by (rule Nil) - then have first_step: "[?e0] : ns_public" - proof (rule NS1) - show "Nonce 0 ~: used []" by eval - qed - then have "[?e1, ?e0] : ns_public" - proof (rule Fake_NS1) - show "Nonce 0 : analz (knows Spy [?e0])" by eval - qed - then have "[?e2, ?e1, ?e0] : ns_public" - proof (rule NS2) - show "Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}) \ set [?e1, ?e0]" by simp - show " Nonce 1 ~: used [?e1, ?e0]" by eval - qed - then show "evs : ns_public" - unfolding assms - proof (rule NS3) - show " Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|}) \ set [?e2, ?e1, ?e0]" by simp - show "Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}) - : set [?e2, ?e1, ?e0]" by simp - qed - from assms show "Nonce NB : analz (knows Spy evs)" - apply simp - apply (rule analz.intros(4)) - apply (rule analz.intros(1)) - apply (auto simp add: bad_def) - done -qed - -end \ No newline at end of file diff -r 6004f4575645 -r 1f7e068b4613 src/HOL/Quickcheck_Examples/Needham_Schroeder_No_Attacker_Example.thy --- a/src/HOL/Quickcheck_Examples/Needham_Schroeder_No_Attacker_Example.thy Tue Jul 31 12:38:01 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,47 +0,0 @@ -theory Needham_Schroeder_No_Attacker_Example -imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck" -begin - -inductive_set ns_public :: "event list set" - where - (*Initial trace is empty*) - Nil: "[] \ ns_public" - (*Alice initiates a protocol run, sending a nonce to Bob*) - | NS1: "\evs1 \ ns_public; Nonce NA \ used evs1\ - \ Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) - # evs1 \ ns_public" - (*Bob responds to Alice's message with a further nonce*) - | NS2: "\evs2 \ ns_public; Nonce NB \ used evs2; - Says A' B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs2\ - \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) - # evs2 \ ns_public" - - (*Alice proves her existence by sending NB back to Bob.*) - | NS3: "\evs3 \ ns_public; - Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs3; - Says B' A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs3\ - \ Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \ ns_public" - -code_pred [skip_proof] ns_publicp . -thm ns_publicp.equation - -code_pred [generator_cps] ns_publicp . -thm ns_publicp.generator_cps_equation - -lemma "ns_publicp evs ==> \ (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs" -(*quickcheck[random, iterations = 1000000, size = 20, timeout = 3600, verbose] -quickcheck[exhaustive, size = 8, timeout = 3600, verbose] -quickcheck[narrowing, size = 7, timeout = 3600, verbose]*) -quickcheck[smart_exhaustive, depth = 5, timeout = 30, expect = counterexample] -oops - -lemma - "\ns_publicp evs\ - \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) : set evs - \ A \ Spy \ B \ Spy \ A \ B - \ Nonce NB \ analz (spies evs)" -quickcheck[smart_exhaustive, depth = 6, timeout = 30] -quickcheck[narrowing, size = 6, timeout = 30, verbose] -oops - -end \ No newline at end of file diff -r 6004f4575645 -r 1f7e068b4613 src/HOL/Quickcheck_Examples/Needham_Schroeder_Unguided_Attacker_Example.thy --- a/src/HOL/Quickcheck_Examples/Needham_Schroeder_Unguided_Attacker_Example.thy Tue Jul 31 12:38:01 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,96 +0,0 @@ -theory Needham_Schroeder_Unguided_Attacker_Example -imports Needham_Schroeder_Base -begin - -inductive_set ns_public :: "event list set" - where - (*Initial trace is empty*) - Nil: "[] \ ns_public" - - | Fake: "\evs1 \ ns_public; X \ synth (analz (spies evs1)) \ - \ Says Spy A X # evs1 \ ns_public" - - (*Alice initiates a protocol run, sending a nonce to Bob*) - | NS1: "\evs1 \ ns_public; Nonce NA \ used evs1\ - \ Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) - # evs1 \ ns_public" - (*Bob responds to Alice's message with a further nonce*) - | NS2: "\evs2 \ ns_public; Nonce NB \ used evs2; - Says A' B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs2\ - \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) - # evs2 \ ns_public" - - (*Alice proves her existence by sending NB back to Bob.*) - | NS3: "\evs3 \ ns_public; - Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs3; - Says B' A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs3\ - \ Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \ ns_public" - -declare ListMem_iff[symmetric, code_pred_inline] - -lemmas [code_pred_intro] = ns_publicp.intros[folded synth'_def] - -code_pred [skip_proof] ns_publicp unfolding synth'_def by (rule ns_publicp.cases) fastforce+ -thm ns_publicp.equation - -code_pred [generator_cps] ns_publicp . -thm ns_publicp.generator_cps_equation - - -lemma "ns_publicp evs ==> \ (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs" -quickcheck[smart_exhaustive, depth = 5, timeout = 200, expect = counterexample] -(*quickcheck[narrowing, size = 6, timeout = 200, verbose, expect = no_counterexample]*) -oops - -lemma - "\ns_publicp evs\ - \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) : set evs - \ A \ Spy \ B \ Spy \ A \ B - \ Nonce NB \ analz (spies evs)" -quickcheck[smart_exhaustive, depth = 6, timeout = 100, expect = no_counterexample] -(*quickcheck[narrowing, size = 7, timeout = 200, expect = no_counterexample]*) -oops - -section {* Proving the counterexample trace for validation *} - -lemma - assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1" - assumes "evs = - [Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)), - Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}), - Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}), - Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|})]" (is "_ = [?e3, ?e2, ?e1, ?e0]") - shows "A \ Spy" "B \ Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)" -proof - - from assms show "A \ Spy" by auto - from assms show "B \ Spy" by auto - have "[] : ns_public" by (rule Nil) - then have first_step: "[?e0] : ns_public" - proof (rule NS1) - show "Nonce 0 ~: used []" by eval - qed - then have "[?e1, ?e0] : ns_public" - proof (rule Fake) - show "Crypt (pubEK Bob) {|Nonce 0, Agent Alice|} : synth (analz (knows Spy [?e0]))" - by (intro synth.intros(2,3,4,1)) eval+ - qed - then have "[?e2, ?e1, ?e0] : ns_public" - proof (rule NS2) - show "Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}) \ set [?e1, ?e0]" by simp - show " Nonce 1 ~: used [?e1, ?e0]" by eval - qed - then show "evs : ns_public" - unfolding assms - proof (rule NS3) - show " Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|}) \ set [?e2, ?e1, ?e0]" by simp - show "Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}) : set [?e2, ?e1, ?e0]" by simp - qed - from assms show "Nonce NB : analz (knows Spy evs)" - apply simp - apply (rule analz.intros(4)) - apply (rule analz.intros(1)) - apply (auto simp add: bad_def) - done -qed - -end \ No newline at end of file diff -r 6004f4575645 -r 1f7e068b4613 src/HOL/Quickcheck_Examples/ROOT.ML --- a/src/HOL/Quickcheck_Examples/ROOT.ML Tue Jul 31 12:38:01 2012 +0200 +++ b/src/HOL/Quickcheck_Examples/ROOT.ML Thu Jul 26 15:55:19 2012 +0200 @@ -1,14 +1,10 @@ use_thys [ -(* "Find_Unused_Assms_Examples", *) "Quickcheck_Examples" (*, "Quickcheck_Lattice_Examples", "Completeness", "Quickcheck_Interfaces", - "Hotel_Example", - "Needham_Schroeder_No_Attacker_Example", - "Needham_Schroeder_Guided_Attacker_Example", - "Needham_Schroeder_Unguided_Attacker_Example"*) + "Hotel_Example",*) ]; if getenv "ISABELLE_GHC" = "" then () diff -r 6004f4575645 -r 1f7e068b4613 src/HOL/ROOT --- a/src/HOL/ROOT Tue Jul 31 12:38:01 2012 +0200 +++ b/src/HOL/ROOT Thu Jul 26 15:55:19 2012 +0200 @@ -740,8 +740,11 @@ Quickcheck_Narrowing_Examples session Quickcheck_Benchmark = HOL + - theories [condition = ISABELLE_BENCHMARK] - Find_Unused_Assms_Examples (* FIXME more *) + theories [condition = ISABELLE_BENCHMARK, quick_and_dirty] + Find_Unused_Assms_Examples + Needham_Schroeder_No_Attacker_Example + Needham_Schroeder_Guided_Attacker_Example + Needham_Schroeder_Unguided_Attacker_Example (* FIXME more *) session Quotient_Examples = HOL + description {*