# HG changeset patch # User bulwahn # Date 1341938494 -7200 # Node ID f2dd90cc724b6edc06120ee8e86b1968a4fbb126 # Parent b16d22bfad07666819c69ae944eddb9cf8ab814b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck) diff -r b16d22bfad07 -r f2dd90cc724b src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Jul 10 13:45:08 2012 +0200 +++ b/src/HOL/IsaMakefile Tue Jul 10 18:41:34 2012 +0200 @@ -1503,6 +1503,7 @@ Quickcheck_Examples/Completeness.thy \ Quickcheck_Examples/Find_Unused_Assms_Examples.thy \ Quickcheck_Examples/Hotel_Example.thy \ + Quickcheck_Examples/Needham_Schroeder_No_Attacker_Example.thy \ Quickcheck_Examples/Quickcheck_Examples.thy \ Quickcheck_Examples/Quickcheck_Interfaces.thy \ Quickcheck_Examples/Quickcheck_Lattice_Examples.thy \ diff -r b16d22bfad07 -r f2dd90cc724b src/HOL/Quickcheck_Examples/Needham_Schroeder_No_Attacker_Example.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Quickcheck_Examples/Needham_Schroeder_No_Attacker_Example.thy Tue Jul 10 18:41:34 2012 +0200 @@ -0,0 +1,240 @@ +theory Needham_Schroeder_No_Attacker_Example +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 --{*Agent names*} + | Key key + | Nonce nat --{*Unguessable nonces*} + | MPair msg msg --{*Compound messages*} + | Crypt key msg --{*Encryption, public- or shared-key*} + +text{*Concrete syntax: messages appear as {|A,B,NA|}, etc...*} +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)" + (* --{*The case for @{term Gets} seems anomalous, but @{term Gets} always + follows @{term Says} in real protocols. Seems difficult to change. + See @{text Gets_correct} in theory @{text "Guard/Extensions.thy"}. *}*) + +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" + + +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 + +code_pred [skip_proof] ns_publicp . +thm ns_publicp.equation + +code_pred [generator_cps] ns_publicp . +thm ns_publicp.generator_cps_equation + +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]] + +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 b16d22bfad07 -r f2dd90cc724b src/HOL/Quickcheck_Examples/ROOT.ML --- a/src/HOL/Quickcheck_Examples/ROOT.ML Tue Jul 10 13:45:08 2012 +0200 +++ b/src/HOL/Quickcheck_Examples/ROOT.ML Tue Jul 10 18:41:34 2012 +0200 @@ -4,7 +4,8 @@ "Quickcheck_Lattice_Examples", "Completeness", "Quickcheck_Interfaces", - "Hotel_Example" + "Hotel_Example", + "Needham_Schroeder_No_Attacker_Example" ]; if getenv "ISABELLE_GHC" = "" then ()