src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy
author wenzelm
Wed Apr 10 21:20:35 2013 +0200 (2013-04-10)
changeset 51692 ecd34f863242
parent 51143 0a2371e7ced3
child 58249 180f1b3508ed
permissions -rw-r--r--
tuned pretty layout: avoid nested Pretty.string_of, which merely happens to work with Isabelle/jEdit since formatting is delegated to Scala side;
declare command "print_case_translations" where it is actually defined;
     1 theory Needham_Schroeder_Base
     2 imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
     3 begin
     4 
     5 datatype agent = Alice | Bob | Spy
     6 
     7 definition agents :: "agent set"
     8 where
     9   "agents = {Spy, Alice, Bob}"
    10 
    11 definition bad :: "agent set"
    12 where
    13   "bad = {Spy}"
    14 
    15 datatype key = pubEK agent | priEK agent
    16 
    17 fun invKey
    18 where
    19   "invKey (pubEK A) = priEK A"
    20 | "invKey (priEK A) = pubEK A"
    21 
    22 datatype
    23      msg = Agent  agent
    24          | Key    key
    25          | Nonce  nat
    26          | MPair  msg msg
    27          | Crypt  key msg
    28 
    29 syntax
    30   "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
    31 
    32 syntax (xsymbols)
    33   "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
    34 
    35 translations
    36   "{|x, y, z|}"   == "{|x, {|y, z|}|}"
    37   "{|x, y|}"      == "CONST MPair x y"
    38 
    39 inductive_set
    40   parts :: "msg set => msg set"
    41   for H :: "msg set"
    42   where
    43     Inj [intro]:               "X \<in> H ==> X \<in> parts H"
    44   | Fst:         "{|X,Y|}   \<in> parts H ==> X \<in> parts H"
    45   | Snd:         "{|X,Y|}   \<in> parts H ==> Y \<in> parts H"
    46   | Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
    47 
    48 inductive_set
    49   analz :: "msg set => msg set"
    50   for H :: "msg set"
    51   where
    52     Inj [intro,simp] :    "X \<in> H ==> X \<in> analz H"
    53   | Fst:     "{|X,Y|} \<in> analz H ==> X \<in> analz H"
    54   | Snd:     "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
    55   | Decrypt [dest]: 
    56              "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
    57 
    58 inductive_set
    59   synth :: "msg set => msg set"
    60   for H :: "msg set"
    61   where
    62     Inj    [intro]:   "X \<in> H ==> X \<in> synth H"
    63   | Agent  [intro]:   "Agent agt \<in> synth H"
    64   | MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
    65   | Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
    66 
    67 primrec initState
    68 where
    69   initState_Alice:
    70     "initState Alice = {Key (priEK Alice)} \<union> (Key ` pubEK ` agents)"
    71 | initState_Bob:
    72     "initState Bob = {Key (priEK Bob)} \<union> (Key ` pubEK ` agents)"
    73 | initState_Spy:
    74     "initState Spy        =  (Key ` priEK ` bad) \<union> (Key ` pubEK ` agents)"
    75 
    76 datatype
    77   event = Says  agent agent msg
    78         | Gets  agent       msg
    79         | Notes agent       msg
    80 
    81 
    82 primrec knows :: "agent => event list => msg set"
    83 where
    84   knows_Nil:   "knows A [] = initState A"
    85 | knows_Cons:
    86     "knows A (ev # evs) =
    87        (if A = Spy then 
    88         (case ev of
    89            Says A' B X => insert X (knows Spy evs)
    90          | Gets A' X => knows Spy evs
    91          | Notes A' X  => 
    92              if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs)
    93         else
    94         (case ev of
    95            Says A' B X => 
    96              if A'=A then insert X (knows A evs) else knows A evs
    97          | Gets A' X    => 
    98              if A'=A then insert X (knows A evs) else knows A evs
    99          | Notes A' X    => 
   100              if A'=A then insert X (knows A evs) else knows A evs))"
   101 
   102 abbreviation (input)
   103   spies  :: "event list => msg set" where
   104   "spies == knows Spy"
   105 
   106 primrec used :: "event list => msg set"
   107 where
   108   used_Nil:   "used []         = Union (parts ` initState ` agents)"
   109 | used_Cons:  "used (ev # evs) =
   110                      (case ev of
   111                         Says A B X => parts {X} \<union> used evs
   112                       | Gets A X   => used evs
   113                       | Notes A X  => parts {X} \<union> used evs)"
   114 
   115 subsection {* Preparations for sets *}
   116 
   117 fun find_first :: "('a => 'b option) => 'a list => 'b option"
   118 where
   119   "find_first f [] = None"
   120 | "find_first f (x # xs) = (case f x of Some y => Some y | None => find_first f xs)"
   121 
   122 consts cps_of_set :: "'a set => ('a => term list option) => term list option"
   123 
   124 lemma
   125   [code]: "cps_of_set (set xs) f = find_first f xs"
   126 sorry
   127 
   128 consts pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => natural => (bool * term list) option"
   129 consts neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => natural => term list Quickcheck_Exhaustive.three_valued"
   130 
   131 lemma
   132   [code]: "pos_cps_of_set (set xs) f i = find_first f xs"
   133 sorry
   134 
   135 consts find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued)
   136     => 'b list => 'a Quickcheck_Exhaustive.three_valued"
   137 
   138 lemma [code]:
   139   "find_first' f [] = Quickcheck_Exhaustive.No_value"
   140   "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))"
   141 sorry
   142 
   143 lemma
   144   [code]: "neg_cps_of_set (set xs) f i = find_first' f xs"
   145 sorry
   146 
   147 setup {*
   148 let
   149   val Fun = Predicate_Compile_Aux.Fun
   150   val Input = Predicate_Compile_Aux.Input
   151   val Output = Predicate_Compile_Aux.Output
   152   val Bool = Predicate_Compile_Aux.Bool
   153   val oi = Fun (Output, Fun (Input, Bool))
   154   val ii = Fun (Input, Fun (Input, Bool))
   155   fun of_set compfuns (Type ("fun", [T, _])) =
   156     case body_type (Predicate_Compile_Aux.mk_monadT compfuns T) of
   157       Type ("Quickcheck_Exhaustive.three_valued", _) => 
   158         Const(@{const_name neg_cps_of_set}, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T))
   159     | Type ("Predicate.pred", _) => Const(@{const_name pred_of_set}, HOLogic.mk_setT T --> Predicate_Compile_Aux.mk_monadT compfuns T)
   160     | _ => Const(@{const_name pos_cps_of_set}, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T))
   161   fun member compfuns (U as Type ("fun", [T, _])) =
   162     (absdummy T (absdummy (HOLogic.mk_setT T) (Predicate_Compile_Aux.mk_if compfuns
   163       (Const (@{const_name "Set.member"}, T --> HOLogic.mk_setT T --> @{typ bool}) $ Bound 1 $ Bound 0))))
   164  
   165 in
   166   Core_Data.force_modes_and_compilations @{const_name Set.member}
   167     [(oi, (of_set, false)), (ii, (member, false))]
   168 end
   169 *}
   170 
   171 subsection {* Derived equations for analz, parts and synth *}
   172 
   173 lemma [code]:
   174   "analz H = (let
   175      H' = H \<union> (Union ((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => if Key (invKey K) : H then {X} else {} | _ => {}) ` H))
   176    in if H' = H then H else analz H')"
   177 sorry
   178 
   179 lemma [code]:
   180   "parts H = (let
   181      H' = H \<union> (Union ((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => {X} | _ => {}) ` H))
   182    in if H' = H then H else parts H')"
   183 sorry
   184 
   185 definition synth' :: "msg set => msg => bool"
   186 where
   187   "synth' H m = (m : synth H)"
   188 
   189 lemmas [code_pred_intro] = synth.intros[folded synth'_def]
   190 
   191 code_pred [generator_cps] synth' unfolding synth'_def by (rule synth.cases) fastforce+
   192 
   193 setup {* Predicate_Compile_Data.ignore_consts [@{const_name analz}, @{const_name knows}] *}
   194 declare ListMem_iff[symmetric, code_pred_inline]
   195 declare [[quickcheck_timing]]
   196 
   197 setup {* Exhaustive_Generators.setup_exhaustive_datatype_interpretation *}
   198 declare [[quickcheck_full_support = false]]
   199 
   200 end