Theory SUF_CMA

(* Title: SUF_CMA.thy
  Author: Andreas Lochbihler, ETH Zurich *)

theory SUF_CMA imports
  CryptHOL.Computational_Model
  CryptHOL.Negligible
  CryptHOL.Environment_Functor
begin

subsection ‹Strongly existentially unforgeable signature scheme›

locale sig_scheme =
  fixes key_gen :: "security ⇒ ('vkey × 'sigkey) spmf"
  and sign :: "security ⇒ 'sigkey ⇒ 'message ⇒ 'signature spmf"
  and verify :: "security ⇒ 'vkey ⇒ 'message ⇒ 'signature ⇒ bool" ― ‹verification is deterministic›
  and valid_message :: "security ⇒ 'message ⇒ bool"

locale suf_cma = sig_scheme +
  constrains key_gen :: "security ⇒ ('vkey × 'sigkey) spmf"
  and sign :: "security ⇒ 'sigkey ⇒ 'message ⇒ 'signature spmf"
  and verify :: "security ⇒ 'vkey ⇒ 'message ⇒ 'signature ⇒ bool"
  and valid_message :: "security ⇒ 'message ⇒ bool"
begin

type_synonym ('vkey', 'sigkey', 'message', 'signature') state_oracle 
  = "('vkey' × 'sigkey' × ('message' × 'signature') list) option"

fun vkey_oracle :: "security ⇒ (('vkey, 'sigkey, 'message, 'signature) state_oracle, unit, 'vkey) oracle'"
where
  "vkey_oracle η None _ = do {
     (vkey, sigkey) ← key_gen η;
     return_spmf (vkey, Some (vkey, sigkey, []))
   }"
| "⋀log. vkey_oracle η (Some (vkey, sigkey, log)) _ = return_spmf (vkey, Some (vkey, sigkey, log))"

context notes bind_spmf_cong[fundef_cong] begin
function sign_oracle
  :: "security ⇒ (('vkey, 'sigkey, 'message, 'signature) state_oracle, 'message, 'signature) oracle'"
where
  "sign_oracle η None m = do { (_, σ) ← vkey_oracle η None (); sign_oracle η σ m }"
| "⋀log. sign_oracle η (Some (vkey, skey, log)) m =
  (if valid_message η m then do {
    sig ← sign η skey m;
    return_spmf (sig, Some (vkey, skey, (m, sig) # log)) 
  } else return_pmf None)"
by pat_completeness auto
termination by(relation "Wellfounded.measure (λ(η, σ, m). case σ of None ⇒ 1 | _ ⇒ 0)") auto
end

lemma lossless_vkey_oracle [simp]:
  "lossless_spmf (vkey_oracle η σ x) ⟷ (σ = None ⟶ lossless_spmf (key_gen η))"
by(cases "(η, σ, x)" rule: vkey_oracle.cases) auto

lemma lossless_sign_oracle [simp]:
  "⟦ σ = None ⟹ lossless_spmf (key_gen η);
    ⋀skey m. valid_message η m ⟹ lossless_spmf (sign η skey m) ⟧
  ⟹ lossless_spmf (sign_oracle η σ m) ⟷ valid_message η m"
apply(cases "(η, σ, m)" rule: sign_oracle.cases)
apply(auto simp add: split_beta dest: lossless_spmfD_set_spmf_nonempty)
done

lemma lossless_sign_oracle_Some: fixes log shows
  "lossless_spmf (sign_oracle η (Some (vkey, skey, log)) m) ⟷ lossless_spmf (sign η skey m) ∧ valid_message η m"
by(simp)

subsubsection ‹Single-user setting›

type_synonym 'message' call⇩1 = "unit + 'message'"
type_synonym ('vkey', 'signature') ret⇩1 = "'vkey' + 'signature'"

definition oracle⇩1 :: "security
  ⇒ (('vkey, 'sigkey, 'message, 'signature) state_oracle, 'message call⇩1, ('vkey, 'signature) ret⇩1) oracle'"
where "oracle⇩1 η = vkey_oracle η ⊕⇩O sign_oracle η"

lemma oracle⇩1_simps [simp]:
  "oracle⇩1 η s (Inl x) = map_spmf (apfst Inl) (vkey_oracle η s x)"
  "oracle⇩1 η s (Inr y) = map_spmf (apfst Inr) (sign_oracle η s y)"
by(simp_all add: oracle⇩1_def)

type_synonym ('vkey', 'message', 'signature') adversary⇩1' = 
  "(('message' × 'signature'), 'message' call⇩1, ('vkey', 'signature') ret⇩1) gpv"
type_synonym ('vkey', 'message', 'signature') adversary⇩1 =
  "security ⇒ ('vkey', 'message', 'signature') adversary⇩1'"

definition suf_cma⇩1 :: "('vkey, 'message, 'signature) adversary⇩1 ⇒ security ⇒ bool spmf"
where
  "⋀log. suf_cma⇩1 𝒜 η = do {
    ((m, sig), σ) ← exec_gpv (oracle⇩1 η) (𝒜 η) None;
    return_spmf (
      case σ of None ⇒ False
      | Some (vkey, skey, log) ⇒ verify η vkey m sig ∧ (m, sig) ∉ set log)
  }"

definition advantage⇩1 :: "('vkey, 'message, 'signature) adversary⇩1 ⇒ advantage"
where "advantage⇩1 𝒜 η = spmf (suf_cma⇩1 𝒜 η) True"

lemma advantage⇩1_nonneg: "advantage⇩1 𝒜 η ≥ 0" by(simp add: advantage⇩1_def pmf_nonneg)

abbreviation secure_for⇩1 :: "('vkey, 'message, 'signature) adversary⇩1 ⇒ bool"
where "secure_for⇩1 𝒜 ≡ negligible (advantage⇩1 𝒜)"

definition ibounded_by⇩1' :: "('vkey, 'message, 'signature) adversary⇩1' ⇒ nat ⇒ bool"
where "ibounded_by⇩1' 𝒜 q = (interaction_any_bounded_by 𝒜 q)"

abbreviation ibounded_by⇩1 :: "('vkey, 'message, 'signature) adversary⇩1 ⇒ (security ⇒ nat) ⇒ bool"
where "ibounded_by⇩1 ≡ rel_envir ibounded_by⇩1'"

definition lossless⇩1' :: "('vkey, 'message, 'signature) adversary⇩1' ⇒ bool"
where "lossless⇩1' 𝒜 = (lossless_gpv ℐ_full 𝒜)"

abbreviation lossless⇩1 :: "('vkey, 'message, 'signature) adversary⇩1 ⇒ bool"
where "lossless⇩1 ≡ pred_envir lossless⇩1'"

subsubsection ‹Multi-user setting›

definition oracle⇩n :: "security
  ⇒ ('i ⇒ ('vkey, 'sigkey, 'message, 'signature) state_oracle, 'i × 'message call⇩1, ('vkey, 'signature) ret⇩1) oracle'"
where "oracle⇩n η = family_oracle (λ_. oracle⇩1 η)"

lemma oracle⇩n_apply [simp]:
  "oracle⇩n η s (i, x) = map_spmf (apsnd (fun_upd s i)) (oracle⇩1 η (s i) x)"
by(simp add: oracle⇩n_def)

type_synonym ('i, 'vkey', 'message', 'signature') adversary⇩n' = 
  "(('i × 'message' × 'signature'), 'i × 'message' call⇩1, ('vkey', 'signature') ret⇩1) gpv"
type_synonym ('i, 'vkey', 'message', 'signature') adversary⇩n =
  "security ⇒ ('i, 'vkey', 'message', 'signature') adversary⇩n'"

definition suf_cma⇩n :: "('i, 'vkey, 'message, 'signature) adversary⇩n ⇒ security ⇒ bool spmf"
where
  "⋀log. suf_cma⇩n 𝒜 η = do {
    ((i, m, sig), σ) ← exec_gpv (oracle⇩n η) (𝒜 η) (λ_. None);
    return_spmf (
      case σ i of None ⇒ False
      | Some (vkey, skey, log) ⇒ verify η vkey m sig ∧ (m, sig) ∉ set log)
  }"

definition advantage⇩n :: "('i, 'vkey, 'message, 'signature) adversary⇩n ⇒ advantage"
where "advantage⇩n 𝒜 η = spmf (suf_cma⇩n 𝒜 η) True"

lemma advantage⇩n_nonneg: "advantage⇩n 𝒜 η ≥ 0" by(simp add: advantage⇩n_def pmf_nonneg)

abbreviation secure_for⇩n :: "('i, 'vkey, 'message, 'signature) adversary⇩n ⇒ bool"
where "secure_for⇩n 𝒜 ≡ negligible (advantage⇩n 𝒜)"

definition ibounded_by⇩n' :: "('i, 'vkey, 'message, 'signature) adversary⇩n' ⇒ nat ⇒ bool"
where "ibounded_by⇩n' 𝒜 q = (interaction_any_bounded_by 𝒜 q)"

abbreviation ibounded_by⇩n :: "('i, 'vkey, 'message, 'signature) adversary⇩n ⇒ (security ⇒ nat) ⇒ bool"
where "ibounded_by⇩n ≡ rel_envir ibounded_by⇩n'"

definition lossless⇩n' :: "('i, 'vkey, 'message, 'signature) adversary⇩n' ⇒ bool"
where "lossless⇩n' 𝒜 = (lossless_gpv ℐ_full 𝒜)"

abbreviation lossless⇩n :: "('i, 'vkey, 'message, 'signature) adversary⇩n ⇒ bool"
where "lossless⇩n ≡ pred_envir lossless⇩n'"

end

end