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"
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
  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) 

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

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

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

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
    TComp clientHello [TAtom Nonce, TAtom Nonce, TAtom Nonce, TAtom Nonce, TAtom Nonce]"

abbreviation Γv_serverHello where
    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
    TComp clientKeyExchange [Γv_crypt]"

abbreviation Γv_HSMsgs where
  "Γv_HSMsgs  TComp concat [
    TAtom PubConst,

(* 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  [

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