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