Theory Example_Keyserver

(*  Title:      Example_Keyserver.thy
    Author:     Andreas Viktor Hess, DTU
    SPDX-License-Identifier: BSD-3-Clause
*)


section ‹The Keyserver Example›
theory Example_Keyserver
imports "../Stateful_Compositionality"
begin

text ‹\label{sec:Example-Keyserver}›
declare [[code_timing]]

subsection ‹Setup›
subsubsection ‹Datatypes and functions setup›
datatype ex_lbl = Label1 (‹𝟭›) | Label2 (‹𝟮›)

datatype ex_atom =
  Agent | Value | Attack | PrivFunSec
| Bot

datatype ex_fun =
  ring | valid | revoked | events | beginauth nat | endauth nat | pubkeys | seen
| invkey | tuple | tuple' | attack nat
| sign | crypt | update | pw
| encodingsecret | pubkey nat
| pubconst ex_atom nat

type_synonym ex_type = "(ex_fun, ex_atom) term_type"
type_synonym ex_var = "ex_type × nat"

lemma ex_atom_UNIV:
  "(UNIV::ex_atom set) = {Agent, Value, Attack, PrivFunSec, Bot}"
by (auto intro: ex_atom.exhaust)

instance ex_atom::finite
by intro_classes (metis ex_atom_UNIV finite.emptyI finite.insertI)

lemma ex_lbl_UNIV:
  "(UNIV::ex_lbl set) = {Label1, Label2}"
by (auto intro: ex_lbl.exhaust)

type_synonym ex_term = "(ex_fun, ex_var) term"
type_synonym ex_terms = "(ex_fun, ex_var) terms"

primrec arity::"ex_fun ⇒ nat" where
  "arity ring = 2"
| "arity valid = 3"
| "arity revoked = 3"
| "arity events = 1"
| "arity (beginauth _) = 3"
| "arity (endauth _) = 3"
| "arity pubkeys = 2"
| "arity seen = 2"
| "arity invkey = 2"
| "arity tuple = 2"
| "arity tuple' = 2"
| "arity (attack _) = 0"
| "arity sign = 2"
| "arity crypt = 2"
| "arity update = 4"
| "arity pw = 2"
| "arity (pubkey _) = 0"
| "arity encodingsecret = 0"
| "arity (pubconst _ _) = 0"

fun public::"ex_fun ⇒ bool" where
  "public (pubkey _) = False"
| "public encodingsecret = False"
| "public _ = True"

fun Anacrypt::"ex_term list ⇒ (ex_term list × ex_term list)" where
  "Anacrypt [k,m] = ([Fun invkey [Fun encodingsecret [], k]], [m])"
| "Anacrypt _ = ([], [])"

fun Anasign::"ex_term list ⇒ (ex_term list × ex_term list)" where
  "Anasign [k,m] = ([], [m])"
| "Anasign _ = ([], [])"

fun Ana::"ex_term ⇒ (ex_term list × ex_term list)" where
  "Ana (Fun tuple T) = ([], T)"
| "Ana (Fun tuple' T) = ([], T)"
| "Ana (Fun sign T) = Anasign T"
| "Ana (Fun crypt T) = Anacrypt T"
| "Ana _ = ([], [])"


subsubsection ‹Keyserver example: Locale interpretation›
lemma assm1:
  "Ana t = (K,M) ⟹ fvset (set K) ⊆ fv t"
  "Ana t = (K,M) ⟹ (⋀g S'. Fun g S' ⊑ t ⟹ length S' = arity g)
                ⟹ k ∈ set K ⟹ Fun f T' ⊑ k ⟹ length T' = arity f"
  "Ana t = (K,M) ⟹ K ≠ [] ∨ M ≠ [] ⟹ Ana (t ⋅ δ) = (K ⋅list δ, M ⋅list δ)"
by (rule Ana.cases[of "t"], auto elim!: Anacrypt.elims Anasign.elims)+

lemma assm2: "Ana (Fun f T) = (K, M) ⟹ set M ⊆ set T"
by (rule Ana.cases[of "Fun f T"]) (auto elim!: Anacrypt.elims Anasign.elims)

lemma assm6: "0 < arity f ⟹ public f" by (cases f) simp_all

global_interpretation im: intruder_model arity public Ana
  defines wftrm = "im.wftrm"
by unfold_locales (metis assm1(1), metis assm1(2),rule Ana.simps, metis assm2, metis assm1(3))

type_synonym ex_strand_step = "(ex_fun,ex_var) strand_step"
type_synonym ex_strand = "(ex_fun,ex_var) strand"


subsubsection ‹Typing function›
definition Γv::"ex_var ⇒ ex_type" where
  "Γv v = (if (∀t ∈ subterms (fst v). case t of
                (TComp f T) ⇒ arity f > 0 ∧ arity f = length T
              | _ ⇒ True)
           then fst v else TAtom Bot)"

fun Γ::"ex_term ⇒ ex_type" where
  "Γ (Var v) = Γv v"
| "Γ (Fun (attack _) _) = TAtom Attack"
| "Γ (Fun (pubkey _) _) = TAtom Value"
| "Γ (Fun encodingsecret _) = TAtom PrivFunSec"
| "Γ (Fun (pubconst τ _) _) = TAtom τ"
| "Γ (Fun f T) = TComp f (map Γ T)"


subsubsection ‹Locale interpretation: typed model›
lemma assm7: "arity c = 0 ⟹ ∃a. ∀X. Γ (Fun c X) = TAtom a" by (cases c) simp_all

lemma assm8: "0 < arity f ⟹ Γ (Fun f X) = TComp f (map Γ X)" by (cases f) simp_all

lemma assm9: "infinite {c. Γ (Fun c []) = TAtom a ∧ public c}"
proof -
  let ?T = "(range (pubconst a))::ex_fun set"
  have *:
      "⋀x y::nat. x ∈ UNIV ⟹ y ∈ UNIV ⟹ (pubconst a x = pubconst a y) = (x = y)"
      "⋀x::nat. x ∈ UNIV ⟹ pubconst a x ∈ ?T"
      "⋀y::ex_fun. y ∈ ?T ⟹ ∃x ∈ UNIV. y = pubconst a x"
    by auto
  have "?T ⊆ {c. Γ (Fun c []) = TAtom a ∧ public c}" by auto
  moreover have "∃f::nat ⇒ ex_fun. bij_betw f UNIV ?T"
    using bij_betwI'[OF *] by blast
  hence "infinite ?T" by (metis nat_not_finite bij_betw_finite)
  ultimately show ?thesis using infinite_super by blast
qed

lemma assm10: "TComp f T ⊑ Γ t ⟹ arity f > 0"
proof (induction rule: Γ.induct)
  case (1 x)
  hence *: "TComp f T ⊑ Γv x" by simp
  hence "Γv x ≠ TAtom Bot" unfolding Γv_def by force
  hence "∀t ∈ subterms (fst x). case t of
            (TComp f T) ⇒ arity f > 0 ∧ arity f = length T
          | _ ⇒ True"
    unfolding Γv_def by argo
  thus ?case using * unfolding Γv_def by fastforce 
qed auto

lemma assm11: "im.wftrm (Γ (Var x))"
proof -
  have "im.wftrm (Γv x)" unfolding Γv_def im.wftrm_def by auto 
  thus ?thesis by simp
qed

lemma assm12: "Γ (Var (τ, n)) = Γ (Var (τ, m))"
apply (cases "∀t ∈ subterms τ. case t of
                (TComp f T) ⇒ arity f > 0 ∧ arity f = length T
              | _ ⇒ True")
by (auto simp add: Γv_def)

lemma Ana_const: "arity c = 0 ⟹ Ana (Fun c T) = ([], [])"
by (cases c) simp_all

lemma Ana_subst': "Ana (Fun f T) = (K,M) ⟹ Ana (Fun f T ⋅ δ) = (K ⋅list δ,M ⋅list δ)"
by (cases f) (auto elim!: Anacrypt.elims Anasign.elims)

global_interpretation tm: typing_result arity public Ana Γ
  apply (unfold_locales, unfold wftrm_def[symmetric])
  by
   (metis assm7, metis assm8, metis assm10, metis assm11, metis assm9, metis assm6)


subsubsection ‹Locale interpretation: labeled stateful typed model›
global_interpretation stm: labeled_stateful_typing' arity public Ana Γ tuple 𝟭 𝟮
by unfold_locales
   (metis assm12, metis Ana_const, metis Ana_subst', fast, rule arity.simps, metis Ana_subst')

type_synonym ex_stateful_strand_step = "(ex_fun,ex_var) stateful_strand_step"
type_synonym ex_stateful_strand = "(ex_fun,ex_var) stateful_strand"

type_synonym ex_labeled_stateful_strand_step =
  "(ex_fun,ex_var,ex_lbl) labeled_stateful_strand_step"

type_synonym ex_labeled_stateful_strand =
  "(ex_fun,ex_var,ex_lbl) labeled_stateful_strand"


subsection ‹Theorem: Type-flaw resistance of the keyserver example from the CSF18 paper›
abbreviation "PK n ≡ Var (TAtom Value,n)"
abbreviation "A n ≡ Var (TAtom Agent,n)"
abbreviation "X n ≡ (TAtom Agent,n)"

abbreviation "ringset t ≡ Fun ring [Fun encodingsecret [], t]"
abbreviation "validset t t' ≡ Fun valid [Fun encodingsecret [], t, t']"
abbreviation "revokedset t t' ≡ Fun revoked [Fun encodingsecret [], t, t']"
abbreviation "eventsset ≡ Fun events [Fun encodingsecret []]"

(* Note: We will use Sks as a constraint, but it actually represents all steps that might occur
         in the protocol *)
abbreviation Sks::"(ex_fun,ex_var) stateful_strand_step list" where
  "Sks ≡ [
    insert⟨Fun (attack 0) [], eventsset⟩,
    delete⟨PK 0, validset (A 0) (A 0)⟩,
    ∀(TAtom Agent,0)⟨PK 0 not in revokedset (A 0) (A 0)⟩,
    ∀(TAtom Agent,0)⟨PK 0 not in validset (A 0) (A 0)⟩,
    insert⟨PK 0, validset (A 0) (A 0)⟩,
    insert⟨PK 0, ringset (A 0)⟩,
    insert⟨PK 0, revokedset (A 0) (A 0)⟩,
    select⟨PK 0, validset (A 0) (A 0)⟩,
    select⟨PK 0, ringset (A 0)⟩,
    receive⟨[Fun invkey [Fun encodingsecret [], PK 0]]⟩,
    receive⟨[Fun sign [Fun invkey [Fun encodingsecret [], PK 0], Fun tuple' [A 0, PK 0]]]⟩,
    send⟨[Fun invkey [Fun encodingsecret [], PK 0]]⟩,
    send⟨[Fun sign [Fun invkey [Fun encodingsecret [], PK 0], Fun tuple' [A 0, PK 0]]]⟩
]"

theorem "stm.tfrsst Sks"
proof -
  let ?M = "concat (map subterms_list (trms_listsst Sks@map (pair' tuple) (setops_listsst Sks)))"
  have "comp_tfrsst arity Ana Γ tuple (set ?M) Sks" by eval
  thus ?thesis by (rule stm.tfrsst_if_comp_tfrsst)
qed


subsection ‹Theorem: Type-flaw resistance of the keyserver examples from the ESORICS18 paper›
abbreviation "signmsg t t' ≡ Fun sign [t, t']"
abbreviation "cryptmsg t t' ≡ Fun crypt [t, t']"
abbreviation "invkeymsg t ≡ Fun invkey [Fun encodingsecret [], t]"
abbreviation "updatemsg a b c d ≡ Fun update [a,b,c,d]"
abbreviation "pwmsg t t' ≡ Fun pw [t, t']"

abbreviation "beginauthset n t t' ≡ Fun (beginauth n) [Fun encodingsecret [], t, t']"
abbreviation "endauthset n t t' ≡ Fun (endauth n) [Fun encodingsecret [], t, t']"
abbreviation "pubkeysset t ≡ Fun pubkeys [Fun encodingsecret [], t]"
abbreviation "seenset t ≡ Fun seen [Fun encodingsecret [], t]"

declare [[coercion "Var::ex_var ⇒ ex_term"]]
declare [[coercion_enabled]]

(* Note: S'ks contains the (slightly over-approximated) steps that can occur in the
         reachable constraints of 𝒫ks,1 and 𝒫ks,2 modulo variable renaming *)
definition S'ks::"ex_labeled_stateful_strand_step list" where
  "S'ks ≡ [
⌦‹constraint steps from the first protocol (duplicate steps are ignored)›

    ⌦‹rule R^1_1›
    ⟨𝟭, send⟨[invkeymsg (PK 0)]⟩⟩,
    ⟨⋆, ⟨PK 0 in validset (A 0) (A 1)⟩⟩,
    ⟨𝟭, receive⟨[Fun (attack 0) []]⟩⟩,

    ⌦‹rule R^2_1›
    ⟨𝟭, send⟨[signmsg (invkeymsg (PK 0)) (Fun tuple' [A 0, PK 0])]⟩⟩,
    ⟨⋆, ⟨PK 0 in validset (A 0) (A 1)⟩⟩,
    ⟨⋆, ∀X 0, X 1⟨PK 0 not in validset (Var (X 0)) (Var (X 1))⟩⟩,
    ⟨𝟭, ∀X 0, X 1⟨PK 0 not in revokedset (Var (X 0)) (Var (X 1))⟩⟩,
    ⟨⋆, ⟨PK 0 not in beginauthset 0 (A 0) (A 1)⟩⟩,

    ⌦‹rule R^3_1›
    ⟨⋆, ⟨PK 0 in beginauthset 0 (A 0) (A 1)⟩⟩,
    ⟨⋆, ⟨PK 0 in endauthset 0 (A 0) (A 1)⟩⟩,

    ⌦‹rule R^4_1›
    ⟨⋆, receive⟨[PK 0]⟩⟩,
    ⟨⋆, receive⟨[invkeymsg (PK 0)]⟩⟩,

    ⌦‹rule R^5_1›
    ⟨𝟭, insert⟨PK 0, ringset (A 0)⟩⟩,
    ⟨⋆, insert⟨PK 0, validset (A 0) (A 1)⟩⟩,
    ⟨⋆, insert⟨PK 0, beginauthset 0 (A 0) (A 1)⟩⟩,
    ⟨⋆, insert⟨PK 0, endauthset 0 (A 0) (A 1)⟩⟩,

    ⌦‹rule R^6_1›
    ⟨𝟭, select⟨PK 0, ringset (A 0)⟩⟩,
    ⟨𝟭, delete⟨PK 0, ringset (A 0)⟩⟩,
    
    ⌦‹rule R^7_1›
    ⟨⋆, ⟨PK 0 not in endauthset 0 (A 0) (A 1)⟩⟩,
    ⟨⋆, delete⟨PK 0, validset (A 0) (A 1)⟩⟩,
    ⟨𝟭, insert⟨PK 0, revokedset (A 0) (A 1)⟩⟩,

    ⌦‹rule R^8_1›
    ⌦‹nothing new›

    ⌦‹rule R^9_1›
    ⟨𝟭, send⟨[PK 0]⟩⟩,
    
    ⌦‹rule R^10_1›
    ⟨𝟭, send⟨[Fun (attack 0) []]⟩⟩,

⌦‹constraint steps from the second protocol (duplicate steps are ignored)›
    ⌦‹rule R^2_1›
    ⟨𝟮, send⟨[invkeymsg (PK 0)]⟩⟩,
    ⟨⋆, ⟨PK 0 in validset (A 0) (A 1)⟩⟩,
    ⟨𝟮, receive⟨[Fun (attack 1) []]⟩⟩,

    ⌦‹rule R^2_2›
    ⟨𝟮, send⟨[cryptmsg (PK 0) (updatemsg (A 0) (A 1) (PK 1) (pwmsg (A 0) (A 1)))]⟩⟩,
    ⟨𝟮, select⟨PK 0, pubkeysset (A 0)⟩⟩,
    ⟨𝟮, ∀X 0⟨PK 0 not in pubkeysset (Var (X 0))⟩⟩,
    ⟨𝟮, ∀X 0⟨PK 0 not in seenset (Var (X 0))⟩⟩,

    ⌦‹rule R^3_2›
    ⟨⋆, ⟨PK 0 in beginauthset 1 (A 0) (A 1)⟩⟩,
    ⟨⋆, ⟨PK 0 in endauthset 1 (A 0) (A 1)⟩⟩,

    ⌦‹rule R^4_2›
    ⟨⋆, receive⟨[PK 0]⟩⟩,
    ⟨⋆, receive⟨[invkeymsg (PK 0)]⟩⟩,

    ⌦‹rule R^5_2›
    ⟨𝟮, select⟨PK 0, pubkeysset (A 0)⟩⟩,
    ⟨⋆, insert⟨PK 0, beginauthset 1 (A 0) (A 1)⟩⟩,
    ⟨𝟮, receive⟨[cryptmsg (PK 0) (updatemsg (A 0) (A 1) (PK 1) (pwmsg (A 0) (A 1)))]⟩⟩,

    ⌦‹rule R^6_2›
    ⟨⋆, ⟨PK 0 not in endauthset 1 (A 0) (A 1)⟩⟩,
    ⟨⋆, insert⟨PK 0, validset (A 0) (A 1)⟩⟩,
    ⟨⋆, insert⟨PK 0, endauthset 1 (A 0) (A 1)⟩⟩,
    ⟨𝟮, insert⟨PK 0, seenset (A 0)⟩⟩,

    ⌦‹rule R^7_2›
    ⟨𝟮, receive⟨[pwmsg (A 0) (A 1)]⟩⟩,

    ⌦‹rule R^8_2›
    ⌦‹nothing new›

    ⌦‹rule R^9_2›
    ⟨𝟮, insert⟨PK 0, pubkeysset (A 0)⟩⟩,

    ⌦‹rule R^10_2›
    ⟨𝟮, send⟨[Fun (attack 1) []]⟩⟩
]"

theorem "stm.tfrsst (unlabel S'ks)"
proof -
  let ?S = "unlabel S'ks"
  let ?M = "concat (map subterms_list (trms_listsst ?S@map (pair' tuple) (setops_listsst ?S)))"
  have "comp_tfrsst arity Ana Γ tuple (set ?M) ?S" by eval
  thus ?thesis by (rule stm.tfrsst_if_comp_tfrsst)
qed


subsection ‹Theorem: The steps of the keyserver protocols from the ESORICS18 paper satisfy the conditions for parallel composition›
theorem
  fixes S f
  defines "S ≡ [PK 0, invkeymsg (PK 0), Fun encodingsecret []]@concat (
                map (λs. [s, Fun tuple [PK 0, s]])
                    [validset (A 0) (A 1), beginauthset 0 (A 0) (A 1), endauthset 0 (A 0) (A 1),
                     beginauthset 1 (A 0) (A 1), endauthset 1 (A 0) (A 1)])@
                [A 0]"
    and "f ≡ λM. {t ⋅ δ | t δ. t ∈ M ∧ tm.wtsubst δ ∧ im.wftrms (subst_range δ) ∧ fv (t ⋅ δ) = {}}"
    and "Sec ≡ (f (set S)) - {m. im.intruder_synth {} m}"
  shows "stm.par_complsst S'ks Sec"
proof -
  let ?N = "λP. set (concat (map subterms_list (trms_listsst P@map (pair' tuple) (setops_listsst P))))"
  let ?M = "λl. ?N (proj_unl l S'ks)"
  have "comp_par_complsst public arity Ana Γ tuple S'ks ?M (set S)"
    unfolding S_def by eval
  thus ?thesis
    using stm.par_complsst_if_comp_par_complsst[of S'ks ?M "set S"]
    unfolding Sec_def f_def wftrm_def[symmetric] by blast
qed

end