Theory System_Construction

section ‹Examples›

theory System_Construction imports
  "../../Constructive_Cryptography"
begin

subsection ‹Random oracle resource›

locale rorc =
  fixes range :: "'r set"
begin

fun rnd_oracle :: "('m ⇒ 'r option, 'm, 'r) oracle'" where
  "rnd_oracle f m = (case f m of
    (Some  r) ⇒ return_spmf (r, f)
  | None      ⇒ do { 
      r ← spmf_of_set (range); 
      return_spmf (r, f(m := Some r))})"

definition "res = RES (rnd_oracle ⊕⇩O rnd_oracle) Map.empty"

end

subsection ‹Key resource›

locale key =
  fixes key_gen :: "'k spmf"
begin

fun key_oracle :: "('k option, unit, 'k) oracle'" where
  "key_oracle None     () =  do { k ← key_gen; return_spmf (k, Some k)}"
| "key_oracle (Some x) () =  return_spmf (x, Some x)"

definition "res = RES (key_oracle ⊕⇩O key_oracle) None"

end


subsection ‹Channel resource›

datatype 'a cstate = Void | Fail | Store 'a | Collect 'a

datatype 'a aquery = Look | ForwardOrEdit (forward_or_edit: 'a) | Drop
type_synonym 'a insec_query = "'a option aquery"
type_synonym auth_query = "unit aquery"

consts Forward :: "'a aquery"
abbreviation Forward_auth :: auth_query where "Forward_auth ≡ ForwardOrEdit ()"
abbreviation Forward_insec :: "'a insec_query" where "Forward_insec ≡ ForwardOrEdit None"
abbreviation Edit :: "'a ⇒ 'a insec_query" where "Edit m ≡ ForwardOrEdit (Some m)"
adhoc_overloading Forward ⇌ Forward_auth
adhoc_overloading Forward ⇌ Forward_insec

translations
  (logic) "CONST Forward" <= (logic) "CONST ForwardOrEdit (CONST None)"
  (logic) "CONST Forward" <= (logic) "CONST ForwardOrEdit (CONST Product_Type.Unity)"
  (type) "auth_query" <= (type) "unit aquery"
  (type) "'a insec_query" <= (type) "'a option aquery"

subsubsection ‹Generic channel›

locale channel =
  fixes side_oracle :: "('m cstate, 'a, 'b option) oracle'"
begin

fun send_oracle :: "('m cstate, 'm, unit) oracle'" where
  "send_oracle Void m = return_spmf ((), Store m)"
| "send_oracle s    m = return_spmf ((), s)"

fun recv_oracle :: "('m cstate, unit, 'm option) oracle'" where
  "recv_oracle (Collect m) () = return_spmf (Some m, Fail)"
| "recv_oracle s           () = return_spmf (None, s)"

definition res :: "('a + 'm + unit, 'b option + unit + 'm option) resource" where
  "res ≡ RES (side_oracle ⊕⇩O send_oracle ⊕⇩O recv_oracle) Void"

end

subsubsection ‹Insecure channel›

locale insec_channel
begin

fun insec_oracle :: "('m cstate, 'm insec_query, 'm option) oracle'" where
  "insec_oracle Void      (Edit m') = return_spmf (None, Collect m')"
| "insec_oracle (Store m) (Edit m') = return_spmf (None, Collect m')"
| "insec_oracle (Store m) Forward   = return_spmf (None, Collect m)"
| "insec_oracle (Store m) Drop      = return_spmf (None, Fail)"
| "insec_oracle (Store m) Look      = return_spmf (Some m, Store m)"
| "insec_oracle s         _         = return_spmf (None, s)"

sublocale channel insec_oracle .

end

subsubsection ‹Authenticated channel›

locale auth_channel
begin

fun auth_oracle :: "('m cstate, auth_query, 'm option) oracle'" where
  "auth_oracle (Store m) Forward = return_spmf (None, Collect m)"
| "auth_oracle (Store m) Drop    = return_spmf (None, Fail)"
| "auth_oracle (Store m) Look    = return_spmf (Some m, Store m)"
| "auth_oracle s         _       = return_spmf (None, s)"

sublocale channel auth_oracle .

end

fun insec_query_of :: "auth_query ⇒ 'm insec_query" where
  "insec_query_of Forward = Forward"
| "insec_query_of Drop = Drop"
| "insec_query_of Look = Look"

abbreviation (input) auth_response_of :: "('mac × 'm) option ⇒ 'm option" 
  where "auth_response_of ≡ map_option snd"

abbreviation insec_auth_wiring :: "(auth_query, 'm option, ('mac × 'm) insec_query, ('mac × 'm) option) wiring"
  where "insec_auth_wiring ≡ (insec_query_of, auth_response_of)"


subsubsection ‹Secure channel›

locale sec_channel
begin

fun sec_oracle :: "('a list cstate, auth_query, nat option) oracle'" where
  "sec_oracle (Store m) Forward = return_spmf (None, Collect m)"
| "sec_oracle (Store m) Drop    = return_spmf (None, Fail)"
| "sec_oracle (Store m) Look    = return_spmf (Some (length m), Store m)"
| "sec_oracle s         _       = return_spmf (None, s)"

sublocale channel sec_oracle .

end

abbreviation (input) auth_query_of :: "auth_query ⇒ auth_query"
  where "auth_query_of ≡ id"

abbreviation (input) sec_response_of :: "'a list option ⇒ nat option"
  where "sec_response_of ≡ map_option length"

abbreviation auth_sec_wiring :: "(auth_query, nat option, auth_query, 'a list option) wiring"
  where "auth_sec_wiring ≡ (auth_query_of, sec_response_of)"

subsection ‹Cipher converter›

locale cipher =
  AUTH: auth_channel + KEY: key key_alg 
  for key_alg :: "'k spmf" +
  fixes enc_alg :: "'k ⇒ 'm ⇒ 'c spmf"
    and dec_alg :: "'k ⇒ 'c ⇒ 'm option"
begin

definition enc :: "('m, unit, unit + 'c, 'k + unit) converter" where
  "enc ≡ CNV (stateless_callee (λm. do {
    k ← Pause (Inl ()) Done;
    c ← lift_spmf (enc_alg (projl k) m);
    (_ :: 'k + unit) ← Pause (Inr c) Done;
    Done (()) 
  })) ()"

definition dec :: "(unit, 'm option, unit + unit, 'k + 'c option) converter" where
  "dec ≡ CNV (stateless_callee (λ_. Pause (Inr ()) (λc'. 
    case c' of Inr (Some c) ⇒ (do {
      k ← Pause (Inl ()) Done;
      Done (dec_alg (projl k) c) })
    | _ ⇒ Done None)
  )) ()"

definition πE :: "(auth_query, 'c option, auth_query, 'c option) converter" (‹π⇧E›) where
  "π⇧E ≡ 1⇩C"

definition "routing ≡ (1⇩C |⇩= lassocr⇩C) ⊙ swap_lassocr ⊙ (1⇩C |⇩= (1⇩C |⇩= swap_lassocr) ⊙ swap_lassocr) ⊙ rassocl⇩C"

definition "res = (1⇩C |⇩= enc |⇩= dec) ⊳ (1⇩C |⇩= parallel_wiring) ⊳ parallel_resource1_wiring ⊳ (KEY.res ∥ AUTH.res)"

lemma res_alt_def: "res = ((1⇩C |⇩= enc |⇩= dec) ⊙ (1⇩C |⇩= parallel_wiring)) ⊳ parallel_resource1_wiring ⊳ (KEY.res ∥ AUTH.res)"
  by(simp add: res_def attach_compose)

end

subsection ‹Message authentication converter›

locale macode = 
  INSEC: insec_channel + RO: rorc range 
  for   range :: "'r set" +
  fixes mac_alg :: "'r ⇒ 'm ⇒ 'a spmf"
begin

definition enm :: "('m, unit, 'm + ('a × 'm), 'r + unit) converter" where
  "enm ≡ CNV (λbs m. if bs 
    then Done ((), True)
    else do {
      r ← Pause (Inl m) Done;
      a ← lift_spmf (mac_alg (projl r) m);
      (_ :: 'r + unit) ← Pause (Inr (a, m)) Done;
      Done ((), True)
    }) False"

definition dem :: "(unit, 'm option, 'm + unit, 'r + ('a × 'm) option) converter" where
  "dem ≡ CNV (stateless_callee (λ_. Pause (Inr ()) (λam'. 
    case am' of Inr (Some (a, m)) ⇒ (do {
      r ← Pause (Inl m) Done;
      a' ← lift_spmf (mac_alg (projl r) m);    
      Done (if a' = a then Some m else None) })
    | _ ⇒ Done None)
  )) ()"

definition πE :: "(('a × 'm) insec_query, ('a × 'm) option, ('a × 'm) insec_query, ('a × 'm) option) converter" (‹π⇧E›) where
  "π⇧E ≡ 1⇩C"

definition "routing ≡ (1⇩C |⇩= lassocr⇩C) ⊙ swap_lassocr ⊙ (1⇩C |⇩= (1⇩C |⇩= swap_lassocr) ⊙ swap_lassocr) ⊙ rassocl⇩C"

definition "res = (1⇩C |⇩= enm |⇩= dem) ⊳ (1⇩C |⇩= parallel_wiring) ⊳ parallel_resource1_wiring ⊳ (RO.res ∥ INSEC.res)"

end


lemma interface_wiring:
  "(cnv_advr |⇩= cnv_send |⇩= cnv_recv) ⊳ (1⇩C |⇩= parallel_wiring) ⊳ parallel_resource1_wiring ⊳ 
  (RES (res2_send ⊕⇩O res2_recv) res2_s ∥ RES (res1_advr ⊕⇩O res1_send ⊕⇩O res1_recv) res1_s)
  =
  cnv_advr |⇩= cnv_send |⇩= cnv_recv ⊳
  RES (†res1_advr ⊕⇩O (res2_send† ⊕⇩O †res1_send) ⊕⇩O res2_recv† ⊕⇩O †res1_recv) (res2_s, res1_s)"
  (is "_ ⊳ ?L1 ⊳ ?L2 ⊳ ?L3 = _ ⊳ ?R")
proof -
  let ?wiring = "(id, id) |⇩w  (lassocr⇩w ∘⇩w ((id, id) |⇩w (rassocl⇩w ∘⇩w (swap⇩w |⇩w (id, id) ∘⇩w lassocr⇩w)) 
    ∘⇩w rassocl⇩w)) ∘⇩w (rassocl⇩w ∘⇩w (swap⇩w |⇩w (id, id) ∘⇩w lassocr⇩w))"

  have "?L1 ⊳ ?L2 ⊳ ?L3 = ?L1 ⊙ ?L2 ⊳
    RES ((res2_send† ⊕⇩O res2_recv†) ⊕⇩O †res1_advr ⊕⇩O †res1_send ⊕⇩O †res1_recv) (res2_s, res1_s)" (is "_ = _ ⊳ RES(?O) ?S") 
    unfolding attach_compose[symmetric] resource_of_parallel_oracle[symmetric]
    by (simp only: parallel_oracle_conv_plus_oracle extend_state_oracle_plus_oracle extend_state_oracle2_plus_oracle)
  also have "… = RES(apply_wiring ?wiring ?O) ?S"
    by (rule attach_wiring_resource_of_oracle, simp only: parallel_wiring_def parallel_resource1_wiring_def swap_lassocr_def)
      ((rule wiring_intro WT_resource_of_oracle WT_plus_oracleI WT_callee_full)+, simp_all)
  also have "… = ?R" by simp
  finally show ?thesis by (rule arg_cong2[where f="attach", OF refl]) 
qed


(* prevent the simplifier from rewriting id and restructuring the equations *)
definition id' where "id' = id"

end