src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
author bulwahn
Tue Aug 31 08:00:55 2010 +0200 (2010-08-31)
changeset 38953 0c38eb5fc4ca
parent 38950 62578950e748
child 38954 80ce658600b0
permissions -rw-r--r--
added further hotel key card attack in example file
     1 theory Hotel_Example
     2 imports Predicate_Compile_Alternative_Defs Code_Prolog
     3 begin
     4 
     5 datatype guest = Guest0 | Guest1
     6 datatype key = Key0 | Key1 | Key2 | Key3
     7 datatype room = Room0
     8 
     9 types card = "key * key"
    10 
    11 datatype event =
    12    Check_in guest room card | Enter guest room card | Exit guest room
    13 
    14 definition initk :: "room \<Rightarrow> key"
    15   where "initk = (%r. Key0)"
    16 
    17 declare initk_def[code_pred_def, code]
    18 
    19 primrec owns :: "event list \<Rightarrow> room \<Rightarrow> guest option"
    20 where
    21   "owns [] r = None"
    22 | "owns (e#s) r = (case e of
    23     Check_in g r' c \<Rightarrow> if r' = r then Some g else owns s r |
    24     Enter g r' c \<Rightarrow> owns s r |
    25     Exit g r' \<Rightarrow> owns s r)"
    26 
    27 primrec currk :: "event list \<Rightarrow> room \<Rightarrow> key"
    28 where
    29   "currk [] r = initk r"
    30 | "currk (e#s) r = (let k = currk s r in
    31     case e of Check_in g r' (k1, k2) \<Rightarrow> if r' = r then k2 else k
    32             | Enter g r' c \<Rightarrow> k
    33             | Exit g r \<Rightarrow> k)"
    34 
    35 primrec issued :: "event list \<Rightarrow> key set"
    36 where
    37   "issued [] = range initk"
    38 | "issued (e#s) = issued s \<union>
    39   (case e of Check_in g r (k1, k2) \<Rightarrow> {k2} | Enter g r c \<Rightarrow> {} | Exit g r \<Rightarrow> {})"
    40 
    41 primrec cards :: "event list \<Rightarrow> guest \<Rightarrow> card set"
    42 where
    43   "cards [] g = {}"
    44 | "cards (e#s) g = (let C = cards s g in
    45                     case e of Check_in g' r c \<Rightarrow> if g' = g then insert c C
    46                                                 else C
    47                             | Enter g r c \<Rightarrow> C
    48                             | Exit g r \<Rightarrow> C)"
    49 
    50 primrec roomk :: "event list \<Rightarrow> room \<Rightarrow> key"
    51 where
    52   "roomk [] r = initk r"
    53 | "roomk (e#s) r = (let k = roomk s r in
    54     case e of Check_in g r' c \<Rightarrow> k
    55             | Enter g r' (x,y) \<Rightarrow> if r' = r (*& x = k*) then y else k
    56             | Exit g r \<Rightarrow> k)"
    57 
    58 primrec isin :: "event list \<Rightarrow> room \<Rightarrow> guest set"
    59 where
    60   "isin [] r = {}"
    61 | "isin (e#s) r = (let G = isin s r in
    62                  case e of Check_in g r c \<Rightarrow> G
    63                  | Enter g r' c \<Rightarrow> if r' = r then {g} \<union> G else G
    64                  | Exit g r' \<Rightarrow> if r'=r then G - {g} else G)"
    65 
    66 primrec hotel :: "event list \<Rightarrow> bool"
    67 where
    68   "hotel []  = True"
    69 | "hotel (e # s) = (hotel s & (case e of
    70   Check_in g r (k,k') \<Rightarrow> k = currk s r \<and> k' \<notin> issued s |
    71   Enter g r (k,k') \<Rightarrow> (k,k') : cards s g & (roomk s r : {k, k'}) |
    72   Exit g r \<Rightarrow> g : isin s r))"
    73 
    74 lemma issued_nil: "issued [] = {Key0}"
    75 by (auto simp add: initk_def)
    76 
    77 lemmas issued_simps[code, code_pred_def] = issued_nil issued.simps(2)
    78 
    79 declare Let_def[code_pred_inline]
    80 
    81 lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)"
    82 by (auto simp add: insert_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection)
    83 
    84 lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
    85 by (auto simp add: Diff_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection)
    86 
    87 setup {* Code_Prolog.map_code_options (K
    88   {ensure_groundness = true,
    89   limited_types = [],
    90   limited_predicates = [],
    91   replacing = [],
    92   prolog_system = Code_Prolog.SWI_PROLOG}) *}
    93 
    94 values 40 "{s. hotel s}"
    95 
    96 
    97 setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
    98 
    99 lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
   100 quickcheck[generator = code, iterations = 100000, report]
   101 quickcheck[generator = prolog, iterations = 1, expect = counterexample]
   102 oops
   103 
   104 
   105 definition no_Check_in :: "event list \<Rightarrow> room \<Rightarrow> bool" where(*>*)
   106 [code del]: "no_Check_in s r \<equiv> \<not>(\<exists>g c. Check_in g r c \<in> set s)"
   107 
   108 
   109 definition feels_safe :: "event list \<Rightarrow> room \<Rightarrow> bool"
   110 where
   111   "feels_safe s r = (\<exists>s\<^isub>1 s\<^isub>2 s\<^isub>3 g c c'.
   112    s = s\<^isub>3 @ [Enter g r c] @ s\<^isub>2 @ [Check_in g r c'] @ s\<^isub>1 \<and>
   113    no_Check_in (s\<^isub>3 @ s\<^isub>2) r \<and> isin (s\<^isub>2 @ [Check_in g r c] @ s\<^isub>1) r = {})"
   114 
   115 ML {* set Code_Prolog.trace *}
   116 
   117 setup {* Code_Prolog.map_code_options (K 
   118   {ensure_groundness = true,
   119    limited_types = [],
   120    limited_predicates = [("hotel", 2)],
   121    replacing = [(("hotel", "limited_hotel"), "quickcheck")],
   122    prolog_system = Code_Prolog.SWI_PROLOG}) *}
   123 
   124 lemma
   125   "hotel s ==> feels_safe s (Room0) ==> g \<in> isin s (Room0) ==> owns s Room0 = Some g"
   126 quickcheck[generator = prolog, iterations = 1]
   127 oops
   128 
   129 end