# HG changeset patch
# User bulwahn
# Date 1342007677 -7200
# Node ID b149de01d669532ec7826f24d285b227aa1bf037
# Parent  f2dd90cc724b6edc06120ee8e86b1968a4fbb126
adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck

diff -r f2dd90cc724b -r b149de01d669 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Jul 10 18:41:34 2012 +0200
+++ b/src/HOL/IsaMakefile	Wed Jul 11 13:54:37 2012 +0200
@@ -1503,7 +1503,10 @@
   Quickcheck_Examples/Completeness.thy					\
   Quickcheck_Examples/Find_Unused_Assms_Examples.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			\
diff -r f2dd90cc724b -r b149de01d669 src/HOL/Quickcheck_Examples/Needham_Schroeder_Base.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quickcheck_Examples/Needham_Schroeder_Base.thy	Wed Jul 11 13:54:37 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\<lbrace>_,/ _\<rbrace>)")
+
+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 \<in> H ==> X \<in> parts H"
+  | Fst:         "{|X,Y|}   \<in> parts H ==> X \<in> parts H"
+  | Snd:         "{|X,Y|}   \<in> parts H ==> Y \<in> parts H"
+  | Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
+
+inductive_set
+  analz :: "msg set => msg set"
+  for H :: "msg set"
+  where
+    Inj [intro,simp] :    "X \<in> H ==> X \<in> analz H"
+  | Fst:     "{|X,Y|} \<in> analz H ==> X \<in> analz H"
+  | Snd:     "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
+  | Decrypt [dest]: 
+             "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
+
+inductive_set
+  synth :: "msg set => msg set"
+  for H :: "msg set"
+  where
+    Inj    [intro]:   "X \<in> H ==> X \<in> synth H"
+  | Agent  [intro]:   "Agent agt \<in> synth H"
+  | MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
+  | Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
+
+primrec initState
+where
+  initState_Alice:
+    "initState Alice = {Key (priEK Alice)} \<union> (Key ` pubEK ` agents)"
+| initState_Bob:
+    "initState Bob = {Key (priEK Bob)} \<union> (Key ` pubEK ` agents)"
+| initState_Spy:
+    "initState Spy        =  (Key ` priEK ` bad) \<union> (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' \<in> 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} \<union> used evs
+                      | Gets A X   => used evs
+                      | Notes A X  => parts {X} \<union> 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> (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> (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 f2dd90cc724b -r b149de01d669 src/HOL/Quickcheck_Examples/Needham_Schroeder_Guided_Attacker_Example.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quickcheck_Examples/Needham_Schroeder_Guided_Attacker_Example.thy	Wed Jul 11 13:54:37 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:  "[] \<in> ns_public"
+
+ | Fake_NS1:  "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<in> analz (spies evs1) \<rbrakk>
+          \<Longrightarrow> Says Spy B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
+                # evs1  \<in> ns_public"
+ | Fake_NS2:  "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<in> analz (spies evs1); Nonce NB \<in> analz (spies evs1) \<rbrakk>
+          \<Longrightarrow> Says Spy A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
+                # evs1  \<in> ns_public"
+
+         (*Alice initiates a protocol run, sending a nonce to Bob*)
+ | NS1:  "\<lbrakk>evs1 \<in> ns_public;  Nonce NA \<notin> used evs1\<rbrakk>
+          \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
+                # evs1  \<in>  ns_public"
+         (*Bob responds to Alice's message with a further nonce*)
+ | NS2:  "\<lbrakk>evs2 \<in> ns_public;  Nonce NB \<notin> used evs2;
+           Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
+          \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
+                # evs2  \<in>  ns_public"
+
+         (*Alice proves her existence by sending NB back to Bob.*)
+ | NS3:  "\<lbrakk>evs3 \<in> ns_public;
+           Says A  B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
+           Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
+          \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> 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 ==> \<not> (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
+  "\<lbrakk>ns_publicp evs\<rbrakk>            
+       \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs
+       \<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B 
+           \<Longrightarrow> Nonce NB \<notin> 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 \<noteq> Spy" "B \<noteq> Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)"
+proof -
+  from assms show "A \<noteq> Spy" by auto
+  from assms show "B \<noteq> 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|}) \<in> 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|}) \<in> 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 f2dd90cc724b -r b149de01d669 src/HOL/Quickcheck_Examples/Needham_Schroeder_No_Attacker_Example.thy
--- a/src/HOL/Quickcheck_Examples/Needham_Schroeder_No_Attacker_Example.thy	Tue Jul 10 18:41:34 2012 +0200
+++ b/src/HOL/Quickcheck_Examples/Needham_Schroeder_No_Attacker_Example.thy	Wed Jul 11 13:54:37 2012 +0200
@@ -2,121 +2,6 @@
 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\<lbrace>_,/ _\<rbrace>)")
-
-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 \<in> H ==> X \<in> parts H"
-  | Fst:         "{|X,Y|}   \<in> parts H ==> X \<in> parts H"
-  | Snd:         "{|X,Y|}   \<in> parts H ==> Y \<in> parts H"
-  | Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
-
-inductive_set
-  analz :: "msg set => msg set"
-  for H :: "msg set"
-  where
-    Inj [intro,simp] :    "X \<in> H ==> X \<in> analz H"
-  | Fst:     "{|X,Y|} \<in> analz H ==> X \<in> analz H"
-  | Snd:     "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
-  | Decrypt [dest]: 
-             "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
-
-inductive_set
-  synth :: "msg set => msg set"
-  for H :: "msg set"
-  where
-    Inj    [intro]:   "X \<in> H ==> X \<in> synth H"
-  | Agent  [intro]:   "Agent agt \<in> synth H"
-  | MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
-  | Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
-
-primrec initState
-where
-  initState_Alice:
-    "initState Alice = {Key (priEK Alice)} \<union> (Key ` pubEK ` agents)"
-| initState_Bob:
-    "initState Bob = {Key (priEK Bob)} \<union> (Key ` pubEK ` agents)"
-
-| initState_Spy:
-    "initState Spy        =  (Key ` priEK ` bad) \<union> (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' \<in> 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} \<union> used evs
-                      | Gets A X   => used evs
-                      | Notes A X  => parts {X} \<union> 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*)
@@ -137,90 +22,12 @@
            Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
           \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> 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> (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> (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 ==> \<not> (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]
diff -r f2dd90cc724b -r b149de01d669 src/HOL/Quickcheck_Examples/Needham_Schroeder_Unguided_Attacker.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quickcheck_Examples/Needham_Schroeder_Unguided_Attacker.thy	Wed Jul 11 13:54:37 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:  "[] \<in> ns_public"
+
+ | Fake:  "\<lbrakk>evs1 \<in> ns_public; X \<in> synth (analz (spies evs1)) \<rbrakk>
+          \<Longrightarrow> Says Spy A X # evs1  \<in> ns_public"
+
+         (*Alice initiates a protocol run, sending a nonce to Bob*)
+ | NS1:  "\<lbrakk>evs1 \<in> ns_public;  Nonce NA \<notin> used evs1\<rbrakk>
+          \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
+                # evs1  \<in>  ns_public"
+         (*Bob responds to Alice's message with a further nonce*)
+ | NS2:  "\<lbrakk>evs2 \<in> ns_public;  Nonce NB \<notin> used evs2;
+           Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
+          \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
+                # evs2  \<in>  ns_public"
+
+         (*Alice proves her existence by sending NB back to Bob.*)
+ | NS3:  "\<lbrakk>evs3 \<in> ns_public;
+           Says A  B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
+           Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
+          \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> 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 ==> \<not> (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
+  "\<lbrakk>ns_publicp evs\<rbrakk>            
+       \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs
+       \<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B 
+           \<Longrightarrow> Nonce NB \<notin> 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 \<noteq> Spy" "B \<noteq> Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)"
+proof -
+  from assms show "A \<noteq> Spy" by auto
+  from assms show "B \<noteq> 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|}) \<in> 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|}) \<in> 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 f2dd90cc724b -r b149de01d669 src/HOL/Quickcheck_Examples/ROOT.ML
--- a/src/HOL/Quickcheck_Examples/ROOT.ML	Tue Jul 10 18:41:34 2012 +0200
+++ b/src/HOL/Quickcheck_Examples/ROOT.ML	Wed Jul 11 13:54:37 2012 +0200
@@ -5,7 +5,9 @@
   "Completeness",
   "Quickcheck_Interfaces",
   "Hotel_Example",
-  "Needham_Schroeder_No_Attacker_Example"
+  "Needham_Schroeder_No_Attacker_Example",
+  "Needham_Schroeder_Guided_Attacker_Example",
+  "Needham_Schroeder_Unguided_Attacker_Example"
 ];
 
 if getenv "ISABELLE_GHC" = "" then ()