Theory Example_TLS

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

section ‹Proving Type-Flaw Resistance of the TLS Handshake Protocol›
theory Example_TLS
imports "../Typed_Model"
begin

declare [[code_timing]]

subsection ‹TLS example: Datatypes and functions setup›
datatype ex_atom = PrivKey | SymKey | PubConst | Agent | Nonce | Bot

datatype ex_fun =
  clientHello | clientKeyExchange | clientFinished
| serverHello | serverCert | serverHelloDone
| finished | changeCipher | x509 | prfun | master | pmsForm
| sign | hash | crypt | pub | concat | privkey nat
| pubconst ex_atom nat

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

instance ex_atom::finite
proof
  let ?S = "UNIV::ex_atom set"
  have "?S = {PrivKey, SymKey, PubConst, Agent, Nonce, Bot}" by (auto intro: ex_atom.exhaust)
  thus "finite ?S" by (metis finite.emptyI finite.insertI) 
qed

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 changeCipher = 0"
| "arity clientFinished = 4"
| "arity clientHello = 5"
| "arity clientKeyExchange = 1"
| "arity concat = 5"
| "arity crypt = 2"
| "arity finished = 1"
| "arity hash = 1"
| "arity master = 3"
| "arity pmsForm = 1"
| "arity prfun = 1"
| "arity (privkey _) = 0"
| "arity pub = 1"
| "arity (pubconst _ _) = 0"
| "arity serverCert = 1"
| "arity serverHello = 5"
| "arity serverHelloDone = 0"
| "arity sign = 2"
| "arity x509 = 2"

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

fun Anacrypt::"ex_term list ⇒ (ex_term list × ex_term list)" where
  "Anacrypt [Fun pub [k],m] = ([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 crypt T) = Anacrypt T"
| "Ana (Fun finished T) = ([], T)"
| "Ana (Fun master T) = ([], T)"
| "Ana (Fun pmsForm T) = ([], T)"
| "Ana (Fun serverCert T) = ([], T)"
| "Ana (Fun serverHello T) = ([], T)"
| "Ana (Fun sign T) = Anasign T"
| "Ana (Fun x509 T) = ([], T)"
| "Ana _ = ([], [])"


subsection ‹TLS 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"
    and wftrms = "im.wftrms"
by unfold_locales (metis assm1(1), metis assm1(2), rule Ana.simps, metis assm2, metis assm1(3))


subsection ‹TLS Example: 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 (privkey _) _) = TAtom PrivKey"
| "Γ (Fun changeCipher _) = TAtom PubConst"
| "Γ (Fun serverHelloDone _) = TAtom PubConst"
| "Γ (Fun (pubconst τ _) _) = TAtom τ"
| "Γ (Fun f T) = TComp f (map Γ T)"


subsection ‹TLS Example: 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:
  assumes "TComp f T ⊑ Γ (Var x)"
  shows "arity f > 0"
proof -
  have *: "TComp f T ⊑ Γv x" using assms 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 ?thesis using * unfolding Γv_def by fastforce
qed

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_keys_subterm: "Ana t = (K,T) ⟹ k ∈ set K ⟹ k ⊏ t"
proof (induct t rule: Ana.induct)
  case (1 U)
  then obtain m where "U = [Fun pub [k], m]" "K = [k]" "T = [m]"
    by (auto elim!: Anacrypt.elims Anasign.elims)
  thus ?case using Fun_subterm_inside_params[of k crypt U] by auto
qed (auto elim!: Anacrypt.elims Anasign.elims)

global_interpretation tm: typed_model' arity public Ana Γ
  by (unfold_locales, unfold wftrm_def[symmetric])
     (metis assm7, metis assm8, metis assm10, metis assm11, metis assm12, metis Ana_const,
      metis Ana_keys_subterm)

subsection ‹TLS example: Proving type-flaw resistance›
abbreviation Γv_clientHello where
  "Γv_clientHello ≡
    TComp clientHello [TAtom Nonce, TAtom Nonce, TAtom Nonce, TAtom Nonce, TAtom Nonce]"

abbreviation Γv_serverHello where
  "Γv_serverHello ≡
    TComp serverHello [TAtom Nonce, TAtom Nonce, TAtom Nonce, TAtom Nonce, TAtom Nonce]"

abbreviation Γv_pub where
  "Γv_pub ≡ TComp pub [TAtom PrivKey]"

abbreviation Γv_x509 where
  "Γv_x509 ≡ TComp x509 [TAtom Agent, Γv_pub]"

abbreviation Γv_sign where
  "Γv_sign ≡ TComp sign [TAtom PrivKey, Γv_x509]"

abbreviation Γv_serverCert where
  "Γv_serverCert ≡ TComp serverCert [Γv_sign]"

abbreviation Γv_pmsForm where
  "Γv_pmsForm ≡ TComp pmsForm [TAtom SymKey]"

abbreviation Γv_crypt where
  "Γv_crypt ≡ TComp crypt [Γv_pub, Γv_pmsForm]"

abbreviation Γv_clientKeyExchange where
  "Γv_clientKeyExchange ≡
    TComp clientKeyExchange [Γv_crypt]"

abbreviation Γv_HSMsgs where
  "Γv_HSMsgs ≡ TComp concat [
    Γv_clientHello,
    Γv_serverHello,
    Γv_serverCert,
    TAtom PubConst,
    Γv_clientKeyExchange]"

(* Variables from TLS *)
abbreviation "T1 n ≡ Var (TAtom Nonce,n)"
abbreviation "T2 n ≡ Var (TAtom Nonce,n)"
abbreviation "RA n ≡ Var (TAtom Nonce,n)"
abbreviation "RB n ≡ Var (TAtom Nonce,n)"
abbreviation "S n ≡ Var (TAtom Nonce,n)"
abbreviation "Cipher n ≡ Var (TAtom Nonce,n)"
abbreviation "Comp n ≡ Var (TAtom Nonce,n)"
abbreviation "B n ≡ Var (TAtom Agent,n)"
abbreviation "Prca n ≡ Var (TAtom PrivKey,n)"
abbreviation "PMS n ≡ Var (TAtom SymKey,n)"
abbreviation "PB n ≡ Var (TComp pub [TAtom PrivKey],n)"
abbreviation "HSMsgs n ≡ Var (Γv_HSMsgs,n)"

subsubsection ‹Defining the over-approximation set›
abbreviation clientHellotrm where
  "clientHellotrm ≡ Fun clientHello [T1 0, RA 1, S 2, Cipher 3, Comp 4]"

abbreviation serverHellotrm where
  "serverHellotrm ≡ Fun serverHello [T2 0, RB 1, S 2, Cipher 3, Comp 4]"

abbreviation serverCerttrm where
  "serverCerttrm ≡ Fun serverCert [Fun sign [Prca 0, Fun x509 [B 1, PB 2]]]"

abbreviation serverHelloDonetrm where
  "serverHelloDonetrm ≡ Fun serverHelloDone []"

abbreviation clientKeyExchangetrm where
  "clientKeyExchangetrm ≡ Fun clientKeyExchange [Fun crypt [PB 0, Fun pmsForm [PMS 1]]]"

abbreviation changeCiphertrm where
  "changeCiphertrm ≡ Fun changeCipher []"

abbreviation finishedtrm where
  "finishedtrm ≡ Fun finished [Fun prfun [
      Fun clientFinished [
          Fun prfun [Fun master [PMS 0, RA 1, RB 2]],
          RA 3, RB 4, Fun hash [HSMsgs 5]
      ]
  ]]"

definition MTLS::"ex_term list" where
  "MTLS ≡ [
    clientHellotrm,
    serverHellotrm,
    serverCerttrm,
    serverHelloDonetrm,
    clientKeyExchangetrm,
    changeCiphertrm,
    finishedtrm
]"


subsection ‹Theorem: The TLS handshake protocol is type-flaw resistant›
theorem "tm.tfrset (set MTLS)"
by (rule tm.tfrset_if_comp_tfrset') eval

end