Theory Messages

(*******************************************************************************

  Project: Refining Authenticated Key Agreement with Strong Adversaries

  Module:  Messages.thy (Isabelle/HOL 2016-1)
  ID:      $Id: Messages.thy 133008 2017-01-17 13:53:14Z csprenge $
  Author:  Joseph Lallemand, INRIA Nancy <joseph.lallemand@loria.fr>
           Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>
  
  Message datatype and quotient construction based on Diffie-Hellman 
  equational theory.

  Copyright (c) 2015-2016 Joseph Lallemand and Christoph Sprenger
  Licence: LGPL

*******************************************************************************)

section ‹Message definitions› 

theory Messages
imports Main
begin

(****************************************************************************************)
subsection ‹Messages›
(****************************************************************************************)

text ‹Agents›
datatype
  agent = Agent nat

text ‹Nonces›
typedecl fid_t

datatype fresh_t = 
  mk_fresh "fid_t" "nat"      (infixr ‹$› 65) 

fun fid :: "fresh_t ⇒ fid_t" where
  "fid (f $ n) = f"

fun num :: "fresh_t ⇒ nat" where
  "num (f $ n) = n"

datatype
  nonce_t =
    nonce_fresh "fresh_t"
  | nonce_atk "nat"


text ‹Keys›
datatype ltkey =
  sharK "agent" "agent"
| publK "agent"
| privK "agent"

datatype ephkey =
  epublK nonce_t
| eprivK nonce_t

datatype tag = insec | auth | confid | secure

text ‹Messages›

datatype cmsg =
  cAgent "agent"
| cNumber "nat"
| cNonce "nonce_t"
| cLtK "ltkey"
| cEphK "ephkey"
| cPair cmsg cmsg
| cEnc cmsg cmsg
| cAenc cmsg cmsg
| cSign cmsg cmsg
| cHash cmsg
| cTag tag
| cExp cmsg cmsg

fun catomic :: "cmsg ⇒ bool"
where
  "catomic (cAgent _) = True"
| "catomic (cNumber _) = True"
| "catomic (cNonce _) = True"
| "catomic (cLtK _) = True"
| "catomic (cEphK _) = True"
| "catomic (cTag _) = True"
|" catomic _ = False"


inductive eq :: "cmsg ⇒ cmsg ⇒ bool"
where
― ‹equations›
  Permute [intro]:"eq (cExp (cExp a b) c) (cExp (cExp a c) b)"
― ‹closure by context›
 | Tag[intro]: "eq (cTag t) (cTag t)"
 | Agent[intro]: "eq (cAgent A) (cAgent A)"
 | Nonce[intro]:"eq (cNonce x) (cNonce x)"
 | Number[intro]:"eq (cNumber x) (cNumber x)"
 | LtK[intro]:"eq (cLtK x) (cLtK x)"
 | EphK[intro]:"eq (cEphK x) (cEphK x)"
 | Pair[intro]:"eq a b ⟹ eq c d ⟹ eq (cPair a c) (cPair b d)"
 | Enc[intro]:"eq a b ⟹ eq c d ⟹ eq (cEnc a c) (cEnc b d)"
 | Aenc[intro]:"eq a b ⟹ eq c d ⟹ eq (cAenc a c) (cAenc b d)"
 | Sign[intro]:"eq a b ⟹ eq c d ⟹ eq (cSign a c) (cSign b d)"
 | Hash[intro]:"eq a b ⟹ eq (cHash a) (cHash b)"
 | Exp[intro]:"eq a b ⟹ eq c d ⟹ eq (cExp a c) (cExp b d)"
― ‹reflexive closure is not needed here because the context closure implies it›
― ‹symmetric closure is not needed as it is easier to include equations in both directions›
― ‹transitive closure›
 | Tr[intro]: "eq a b ⟹ eq b c ⟹ eq a c"

lemma eq_sym: "eq a b ⟷ eq b a"
by (auto elim: eq.induct)

lemma eq_Sym [intro]: "eq a b ⟹ eq b a"
by (auto elim: eq.induct)

lemma eq_refl [simp, intro]: "eq a a"
by (induction a, auto)

text ‹inductive cases; keep the transitivity case, so we prove the the right lemmas by hand.›
lemma eq_Number: "eq (cNumber N) y ⟹  y = cNumber N"
  by (induction "cNumber N" y rule: eq.induct, auto)
lemma eq_Agent: "eq (cAgent A) y ⟹  y = cAgent A"
  by (induction "cAgent A" y rule: eq.induct, auto)
lemma eq_Nonce: "eq (cNonce N) y ⟹  y = cNonce N"
  by (induction "cNonce N" y rule: eq.induct, auto)
lemma eq_LtK: "eq (cLtK N) y ⟹  y = cLtK N"
  by (induction "cLtK N" y rule: eq.induct, auto)
lemma eq_EphK: "eq (cEphK N) y ⟹  y = cEphK N"
  by (induction "cEphK N" y rule: eq.induct, auto)
lemma eq_Tag: "eq (cTag N) y ⟹  y = cTag N"
  by (induction "cTag N" y rule: eq.induct, auto)
lemma eq_Hash: "eq (cHash X) y ⟹ ∃Y. y = cHash Y ∧ eq X Y"
  by (drule eq.induct [where P="λx. λy. ∀ X. x = cHash X ⟶ (∃Y. y = cHash Y ∧ eq X Y)"],
      auto elim!:Tr)
lemma eq_Pair: "eq (cPair X Y) y ⟹  ∃ X' Y'. y = cPair X' Y' ∧ eq X X' ∧ eq Y Y'"
  apply (drule eq.induct [where 
    P="λx. λy. ∀ X Y. x = cPair X Y ⟶ (∃ X' Y'. y = cPair X' Y' ∧ eq X X' ∧ eq Y Y')"])
  apply (auto elim!: Tr)
done
lemma eq_Enc: "eq (cEnc X Y) y ⟹  ∃ X' Y'. y = cEnc X' Y' ∧ eq X X' ∧ eq Y Y'"
  apply (drule eq.induct [where 
    P="λx. λy. ∀ X Y. x = cEnc X Y ⟶ (∃ X' Y'. y = cEnc X' Y' ∧ eq X X' ∧ eq Y Y')"])
  apply (auto elim!: Tr)
done
lemma eq_Aenc: "eq (cAenc X Y) y ⟹  ∃ X' Y'. y = cAenc X' Y' ∧ eq X X' ∧ eq Y Y'"
  apply (drule eq.induct [where 
    P="λx. λy. ∀ X Y. x = cAenc X Y ⟶ (∃ X' Y'. y = cAenc X' Y' ∧ eq X X' ∧ eq Y Y')"])
  apply (auto elim!: Tr)
done
lemma eq_Sign: "eq (cSign X Y) y ⟹  ∃ X' Y'. y = cSign X' Y' ∧ eq X X' ∧ eq Y Y'"
  apply (drule eq.induct [where 
    P="λx. λy. ∀ X Y. x = cSign X Y ⟶ (∃ X' Y'. y = cSign X' Y' ∧ eq X X' ∧ eq Y Y')"])
  apply (auto elim!: Tr)
done
lemma eq_Exp: "eq (cExp X Y) y ⟹  ∃ X' Y'. y = cExp X' Y'"
  apply (drule eq.induct [where 
    P="λx. λy. ∀ X Y. x = cExp X Y ⟶ (∃ X' Y'. y = cExp X' Y')"])
  apply (auto elim!: Tr)
done

lemmas eqD_aux = eq_Number eq_Agent eq_Nonce eq_LtK eq_EphK eq_Tag
                    eq_Hash eq_Pair eq_Enc eq_Aenc eq_Sign eq_Exp
lemmas eqD [dest] = eqD_aux eqD_aux [OF eq_Sym]


text ‹Quotient construction›

quotient_type msg = cmsg / eq
morphisms Re Ab
by (auto simp add:equivp_def)


lift_definition Number :: "nat ⇒ msg" is cNumber by -
lift_definition Nonce :: "nonce_t ⇒ msg" is cNonce by -
lift_definition Agent :: "agent ⇒ msg" is cAgent by -
lift_definition LtK :: "ltkey ⇒ msg" is cLtK by -
lift_definition EphK :: "ephkey ⇒ msg" is cEphK by -
lift_definition Pair :: "msg ⇒ msg ⇒ msg" is cPair by auto
lift_definition Enc :: "msg ⇒ msg ⇒ msg" is cEnc by auto
lift_definition Aenc :: "msg ⇒ msg ⇒ msg" is cAenc by auto
lift_definition Exp :: "msg ⇒ msg ⇒ msg" is cExp by auto
lift_definition Tag :: "tag ⇒ msg" is cTag by -
lift_definition Hash :: "msg ⇒ msg" is cHash by auto
lift_definition Sign :: "msg ⇒ msg ⇒ msg" is cSign by auto

lemmas msg_defs = 
  Agent_def Number_def Nonce_def LtK_def EphK_def Pair_def 
  Enc_def Aenc_def Exp_def Hash_def Tag_def Sign_def


text ‹Commutativity of exponents›

lemma permute_exp [simp]: "Exp (Exp X Y) Z = Exp (Exp X Z) Y"
by (transfer, auto)

lift_definition atomic :: "msg ⇒ bool" is catomic by (erule eq.induct, auto)

abbreviation 
  composed :: "msg ⇒ bool" where
  "composed X ≡ ¬atomic X"

lemma atomic_Agent [simp, intro]: "atomic (Agent X)" by (transfer, auto)
lemma atomic_Tag [simp, intro]: "atomic (Tag X)" by (transfer, auto)
lemma atomic_Nonce [simp, intro]: "atomic (Nonce X)" by (transfer, auto)
lemma atomic_Number [simp, intro]: "atomic (Number X)" by (transfer, auto)
lemma atomic_LtK [simp, intro]: "atomic (LtK X)" by (transfer, auto)
lemma atomic_EphK [simp, intro]: "atomic (EphK X)" by (transfer, auto)

lemma non_atomic_Pair [simp]: "¬atomic (Pair x y)" by (transfer, auto)
lemma non_atomic_Enc [simp]: "¬atomic (Enc x y)" by (transfer, auto)
lemma non_atomic_Aenc [simp]: "¬atomic (Aenc x y)" by (transfer, auto)
lemma non_atomic_Sign [simp]: "¬atomic (Sign x y)" by (transfer, auto)
lemma non_atomic_Exp [simp]: "¬atomic (Exp x y)" by (transfer, auto)
lemma non_atomic_Hash [simp]: "¬atomic (Hash x)" by (transfer, auto)

lemma Nonce_Nonce: "(Nonce X = Nonce X') = (X = X')" by transfer auto
lemma Nonce_Agent: "Nonce X ≠ Agent X'" by transfer auto
lemma Nonce_Number: "Nonce X ≠ Number X'" by transfer auto
lemma Nonce_Hash: "Nonce X ≠ Hash  X'" by transfer auto
lemma Nonce_Tag: "Nonce X ≠ Tag  X'" by transfer auto
lemma Nonce_EphK: "Nonce X ≠ EphK  X'" by transfer auto
lemma Nonce_LtK: "Nonce X ≠ LtK  X'" by transfer auto
lemma Nonce_Pair: "Nonce X ≠ Pair  X' Y'" by transfer auto
lemma Nonce_Enc: "Nonce X ≠ Enc  X' Y'" by transfer auto
lemma Nonce_Aenc: "Nonce X ≠ Aenc  X' Y'" by transfer auto
lemma Nonce_Sign: "Nonce X ≠ Sign  X' Y'" by transfer auto
lemma Nonce_Exp: "Nonce X ≠ Exp  X' Y'" by transfer auto

lemma Agent_Nonce: "Agent X ≠ Nonce  X'" by transfer auto
lemma Agent_Agent: "(Agent X = Agent X') = (X = X')" by transfer auto
lemma Agent_Number: "Agent X ≠ Number  X'" by transfer auto
lemma Agent_Hash: "Agent X ≠ Hash  X'" by transfer auto
lemma Agent_Tag: "Agent X ≠ Tag  X'" by transfer auto
lemma Agent_EphK: "Agent X ≠ EphK  X'" by transfer auto
lemma Agent_LtK: "Agent X ≠ LtK  X'" by transfer auto
lemma Agent_Pair: "Agent X ≠ Pair  X' Y'" by transfer auto
lemma Agent_Enc: "Agent X ≠ Enc  X' Y'" by transfer auto
lemma Agent_Aenc: "Agent X ≠ Aenc  X' Y'" by transfer auto
lemma Agent_Sign: "Agent X ≠ Sign  X' Y'" by transfer auto
lemma Agent_Exp: "Agent X ≠ Exp  X' Y'" by transfer auto

lemma Number_Nonce: "Number X ≠ Nonce  X'" by transfer auto
lemma Number_Agent: "Number X ≠ Agent  X'" by transfer auto
lemma Number_Number: "(Number X = Number X') = (X = X')" by transfer auto
lemma Number_Hash: "Number X ≠ Hash  X'" by transfer auto
lemma Number_Tag: "Number X ≠ Tag  X'" by transfer auto
lemma Number_EphK: "Number X ≠ EphK  X'" by transfer auto
lemma Number_LtK: "Number X ≠ LtK  X'" by transfer auto
lemma Number_Pair: "Number X ≠ Pair  X' Y'" by transfer auto
lemma Number_Enc: "Number X ≠ Enc  X' Y'" by transfer auto
lemma Number_Aenc: "Number X ≠ Aenc  X' Y'" by transfer auto
lemma Number_Sign: "Number X ≠ Sign  X' Y'" by transfer auto
lemma Number_Exp: "Number X ≠ Exp  X' Y'" by transfer auto

lemma Hash_Nonce: "Hash X ≠ Nonce  X'" by transfer auto
lemma Hash_Agent: "Hash X ≠ Agent  X'" by transfer auto
lemma Hash_Number: "Hash X ≠ Number  X'" by transfer auto
lemma Hash_Hash: "(Hash X = Hash X') = (X = X')" by transfer auto
lemma Hash_Tag: "Hash X ≠ Tag  X'" by transfer auto
lemma Hash_EphK: "Hash X ≠ EphK  X'" by transfer auto
lemma Hash_LtK: "Hash X ≠ LtK  X'" by transfer auto
lemma Hash_Pair: "Hash X ≠ Pair  X' Y'" by transfer auto
lemma Hash_Enc: "Hash X ≠ Enc  X' Y'" by transfer auto
lemma Hash_Aenc: "Hash X ≠ Aenc  X' Y'" by transfer auto
lemma Hash_Sign: "Hash X ≠ Sign  X' Y'" by transfer auto
lemma Hash_Exp: "Hash X ≠ Exp  X' Y'" by transfer auto

lemma Tag_Nonce: "Tag X ≠ Nonce  X'" by transfer auto
lemma Tag_Agent: "Tag X ≠ Agent  X'" by transfer auto
lemma Tag_Number: "Tag X ≠ Number  X'" by transfer auto
lemma Tag_Hash: "Tag X ≠ Hash  X'" by transfer auto
lemma Tag_Tag: "(Tag X = Tag X') = (X = X')" by transfer auto
lemma Tag_EphK: "Tag X ≠ EphK  X'" by transfer auto
lemma Tag_LtK: "Tag X ≠ LtK  X'" by transfer auto
lemma Tag_Pair: "Tag X ≠ Pair  X' Y'" by transfer auto
lemma Tag_Enc: "Tag X ≠ Enc  X' Y'" by transfer auto
lemma Tag_Aenc: "Tag X ≠ Aenc  X' Y'" by transfer auto
lemma Tag_Sign: "Tag X ≠ Sign  X' Y'" by transfer auto
lemma Tag_Exp: "Tag X ≠ Exp  X' Y'" by transfer auto

lemma EphK_Nonce: "EphK X ≠ Nonce  X'" by transfer auto
lemma EphK_Agent: "EphK X ≠ Agent  X'" by transfer auto
lemma EphK_Number: "EphK X ≠ Number  X'" by transfer auto
lemma EphK_Hash: "EphK X ≠ Hash  X'" by transfer auto
lemma EphK_Tag: "EphK X ≠ Tag  X'" by transfer auto
lemma EphK_EphK: "(EphK X = EphK X') = (X = X')" by transfer auto
lemma EphK_LtK: "EphK X ≠ LtK  X'" by transfer auto
lemma EphK_Pair: "EphK X ≠ Pair  X' Y'" by transfer auto
lemma EphK_Enc: "EphK X ≠ Enc  X' Y'" by transfer auto
lemma EphK_Aenc: "EphK X ≠ Aenc  X' Y'" by transfer auto
lemma EphK_Sign: "EphK X ≠ Sign  X' Y'" by transfer auto
lemma EphK_Exp: "EphK X ≠ Exp  X' Y'" by transfer auto

lemma LtK_Nonce: "LtK X ≠ Nonce  X'" by transfer auto
lemma LtK_Agent: "LtK X ≠ Agent  X'" by transfer auto
lemma LtK_Number: "LtK X ≠ Number  X'" by transfer auto
lemma LtK_Hash: "LtK X ≠ Hash  X'" by transfer auto
lemma LtK_Tag: "LtK X ≠ Tag  X'" by transfer auto
lemma LtK_EphK: "LtK X ≠ EphK  X'" by transfer auto
lemma LtK_LtK: "(LtK X = LtK X') = (X = X')" by transfer auto
lemma LtK_Pair: "LtK X ≠ Pair  X' Y'" by transfer auto
lemma LtK_Enc: "LtK X ≠ Enc  X' Y'" by transfer auto
lemma LtK_Aenc: "LtK X ≠ Aenc  X' Y'" by transfer auto
lemma LtK_Sign: "LtK X ≠ Sign  X' Y'" by transfer auto
lemma LtK_Exp: "LtK X ≠ Exp  X' Y'" by transfer auto

lemma Pair_Nonce: "Pair X Y ≠ Nonce  X'" by transfer auto
lemma Pair_Agent: "Pair X Y ≠ Agent  X'" by transfer auto
lemma Pair_Number: "Pair X Y ≠ Number  X'" by transfer auto
lemma Pair_Hash: "Pair X Y ≠ Hash  X'" by transfer auto
lemma Pair_Tag: "Pair X Y ≠ Tag  X'" by transfer auto
lemma Pair_EphK: "Pair X Y ≠ EphK  X'" by transfer auto
lemma Pair_LtK: "Pair X Y ≠ LtK  X'" by transfer auto
lemma Pair_Pair: "(Pair X Y = Pair X' Y') = (X = X' ∧ Y = Y')" by transfer auto
lemma Pair_Enc: "Pair X Y ≠ Enc  X' Y'" by transfer auto
lemma Pair_Aenc: "Pair X Y ≠ Aenc  X' Y'" by transfer auto
lemma Pair_Sign: "Pair X Y ≠ Sign  X' Y'" by transfer auto
lemma Pair_Exp: "Pair X Y ≠ Exp  X' Y'" by transfer auto

lemma Enc_Nonce: "Enc X Y ≠ Nonce  X'" by transfer auto
lemma Enc_Agent: "Enc X Y ≠ Agent  X'" by transfer auto
lemma Enc_Number: "Enc X Y ≠ Number  X'" by transfer auto
lemma Enc_Hash: "Enc X Y ≠ Hash  X'" by transfer auto
lemma Enc_Tag: "Enc X Y ≠ Tag  X'" by transfer auto
lemma Enc_EphK: "Enc X Y ≠ EphK  X'" by transfer auto
lemma Enc_LtK: "Enc X Y ≠ LtK  X'" by transfer auto
lemma Enc_Pair: "Enc X Y ≠ Pair  X' Y'" by transfer auto
lemma Enc_Enc: "(Enc X Y = Enc X' Y') = (X = X' ∧ Y = Y')" by transfer auto
lemma Enc_Aenc: "Enc X Y ≠ Aenc  X' Y'" by transfer auto
lemma Enc_Sign: "Enc X Y ≠ Sign  X' Y'" by transfer auto
lemma Enc_Exp: "Enc X Y ≠ Exp  X' Y'" by transfer auto

lemma Aenc_Nonce: "Aenc X Y ≠ Nonce  X'" by transfer auto
lemma Aenc_Agent: "Aenc X Y ≠ Agent  X'" by transfer auto
lemma Aenc_Number: "Aenc X Y ≠ Number  X'" by transfer auto
lemma Aenc_Hash: "Aenc X Y ≠ Hash  X'" by transfer auto
lemma Aenc_Tag: "Aenc X Y ≠ Tag  X'" by transfer auto
lemma Aenc_EphK: "Aenc X Y ≠ EphK  X'" by transfer auto
lemma Aenc_LtK: "Aenc X Y ≠ LtK  X'" by transfer auto
lemma Aenc_Pair: "Aenc X Y ≠ Pair  X' Y'" by transfer auto
lemma Aenc_Enc: "Aenc X Y ≠ Enc  X' Y'" by transfer auto
lemma Aenc_Aenc: "(Aenc X Y = Aenc X' Y') = (X = X' ∧ Y = Y')" by transfer auto
lemma Aenc_Sign: "Aenc X Y ≠ Sign  X' Y'" by transfer auto
lemma Aenc_Exp: "Aenc X Y ≠ Exp  X' Y'" by transfer auto

lemma Sign_Nonce: "Sign X Y ≠ Nonce  X'" by transfer auto
lemma Sign_Agent: "Sign X Y ≠ Agent  X'" by transfer auto
lemma Sign_Number: "Sign X Y ≠ Number  X'" by transfer auto
lemma Sign_Hash: "Sign X Y ≠ Hash  X'" by transfer auto
lemma Sign_Tag: "Sign X Y ≠ Tag  X'" by transfer auto
lemma Sign_EphK: "Sign X Y ≠ EphK  X'" by transfer auto
lemma Sign_LtK: "Sign X Y ≠ LtK  X'" by transfer auto
lemma Sign_Pair: "Sign X Y ≠ Pair  X' Y'" by transfer auto
lemma Sign_Enc: "Sign X Y ≠ Enc  X' Y'" by transfer auto
lemma Sign_Aenc: "Sign X Y ≠ Aenc  X' Y'" by transfer auto
lemma Sign_Sign: "(Sign X Y = Sign X' Y') = (X = X' ∧ Y = Y')" by transfer auto
lemma Sign_Exp: "Sign X Y ≠ Exp  X' Y'" by transfer auto

lemma Exp_Nonce: "Exp X Y ≠ Nonce  X'" by transfer auto
lemma Exp_Agent: "Exp X Y ≠ Agent  X'" by transfer auto
lemma Exp_Number: "Exp X Y ≠ Number  X'" by transfer auto
lemma Exp_Hash: "Exp X Y ≠ Hash  X'" by transfer auto
lemma Exp_Tag: "Exp X Y ≠ Tag  X'" by transfer auto
lemma Exp_EphK: "Exp X Y ≠ EphK  X'" by transfer auto
lemma Exp_LtK: "Exp X Y ≠ LtK  X'" by transfer auto
lemma Exp_Pair: "Exp X Y ≠ Pair  X' Y'" by transfer auto
lemma Exp_Enc: "Exp X Y ≠ Enc  X' Y'" by transfer auto
lemma Exp_Aenc: "Exp X Y ≠ Aenc  X' Y'" by transfer auto
lemma Exp_Sign: "Exp X Y ≠ Sign  X' Y'" by transfer auto


lemmas msg_inject [iff, induct_simp] =
  Nonce_Nonce Agent_Agent Number_Number Hash_Hash Tag_Tag EphK_EphK LtK_LtK 
  Pair_Pair Enc_Enc Aenc_Aenc Sign_Sign

lemmas msg_distinct [simp, induct_simp] =
  Nonce_Agent Nonce_Number Nonce_Hash Nonce_Tag Nonce_EphK Nonce_LtK Nonce_Pair 
  Nonce_Enc Nonce_Aenc Nonce_Sign Nonce_Exp 
  Agent_Nonce Agent_Number Agent_Hash Agent_Tag Agent_EphK Agent_LtK Agent_Pair 
  Agent_Enc Agent_Aenc Agent_Sign Agent_Exp 
  Number_Nonce Number_Agent Number_Hash Number_Tag Number_EphK Number_LtK 
  Number_Pair Number_Enc Number_Aenc Number_Sign Number_Exp 
  Hash_Nonce Hash_Agent Hash_Number Hash_Tag Hash_EphK Hash_LtK Hash_Pair 
  Hash_Enc Hash_Aenc Hash_Sign Hash_Exp 
  Tag_Nonce Tag_Agent Tag_Number Tag_Hash Tag_EphK Tag_LtK Tag_Pair 
  Tag_Enc Tag_Aenc Tag_Sign Tag_Exp 
  EphK_Nonce EphK_Agent EphK_Number EphK_Hash EphK_Tag EphK_LtK EphK_Pair 
  EphK_Enc EphK_Aenc EphK_Sign EphK_Exp 
  LtK_Nonce LtK_Agent LtK_Number LtK_Hash LtK_Tag LtK_EphK LtK_Pair 
  LtK_Enc LtK_Aenc LtK_Sign LtK_Exp 
  Pair_Nonce Pair_Agent Pair_Number Pair_Hash Pair_Tag Pair_EphK Pair_LtK 
  Pair_Enc Pair_Aenc Pair_Sign Pair_Exp 
  Enc_Nonce Enc_Agent Enc_Number Enc_Hash Enc_Tag Enc_EphK Enc_LtK Enc_Pair 
  Enc_Aenc Enc_Sign Enc_Exp 
  Aenc_Nonce Aenc_Agent Aenc_Number Aenc_Hash Aenc_Tag Aenc_EphK Aenc_LtK 
  Aenc_Pair Aenc_Enc Aenc_Sign Aenc_Exp 
  Sign_Nonce Sign_Agent Sign_Number Sign_Hash Sign_Tag Sign_EphK Sign_LtK 
  Sign_Pair Sign_Enc Sign_Aenc Sign_Exp 
  Exp_Nonce Exp_Agent Exp_Number Exp_Hash Exp_Tag Exp_EphK Exp_LtK Exp_Pair 
  Exp_Enc Exp_Aenc Exp_Sign 


consts Ngen :: nat
abbreviation "Gen ≡ Number Ngen"
abbreviation "cGen ≡ cNumber Ngen"

abbreviation 
  "InsecTag ≡ Tag insec"

abbreviation 
  "AuthTag ≡ Tag auth"

abbreviation 
  "ConfidTag ≡ Tag confid"

abbreviation 
  "SecureTag ≡ Tag secure"

abbreviation 
  "Tags ≡ range Tag"

abbreviation
  NonceF :: "fresh_t ⇒ msg" where
  "NonceF N ≡ Nonce (nonce_fresh N)"

abbreviation
  NonceA :: "nat ⇒ msg" where
  "NonceA N ≡ Nonce (nonce_atk N)"

abbreviation
  shrK :: "agent ⇒ agent ⇒ msg" where
  "shrK A B ≡ LtK (sharK A B)"

abbreviation
  pubK :: "agent ⇒ msg" where
  "pubK A ≡ LtK (publK A)"

abbreviation
  priK :: "agent ⇒ msg" where
  "priK A ≡ LtK (privK A)"

abbreviation
  epubK :: "nonce_t ⇒ msg" where
  "epubK N ≡ EphK (epublK N)"

abbreviation
  epriK :: "nonce_t ⇒ msg" where
  "epriK N ≡ EphK (eprivK N)"

abbreviation
  epubKF :: "fresh_t ⇒ msg" where
  "epubKF N ≡ EphK (epublK (nonce_fresh N))"

abbreviation
  epriKF :: "fresh_t ⇒ msg" where
  "epriKF N ≡ EphK (eprivK (nonce_fresh N))"

abbreviation
  epubKA :: "nat ⇒ msg" where
  "epubKA N ≡ EphK (epublK (nonce_atk N))"

abbreviation
  epriKA :: "nat ⇒ msg" where
  "epriKA N ≡ EphK (eprivK (nonce_atk N))"


text‹Concrete syntax: messages appear as <A,B,NA>, etc...›

syntax
  "_MTuple"      :: "['a, args] ⇒ 'a * 'b"  (‹(‹indent=2 notation=‹mixfix message tuple››⟨_,/ _⟩)›)
syntax_consts
  "_MTuple" ⇌ Pair
translations
  "⟨x, y, z⟩" ⇌ "⟨x, ⟨y, z⟩⟩"
  "⟨x, y⟩"    ⇌ "CONST Pair x y"

text ‹hash macs›
abbreviation
  hmac :: "msg ⇒ msg ⇒ msg" where
  "hmac M K ≡ Hash ⟨M, K⟩"


text ‹recover some kind of injectivity for Exp›
lemma eq_expgen: 
  "eq X Y ⟹ (∀ X'. X = cExp cGen X' ⟶ (∃ Z. Y = (cExp cGen Z) ∧ eq X' Z)) ∧
              (∀ Y'. Y = cExp cGen Y' ⟶ (∃ Z. X = (cExp cGen Z) ∧ eq Y' Z))"
by (erule eq.induct, auto elim!: Tr)

lemma Exp_Gen_inj: "Exp Gen X = Exp Gen Y ⟹ X = Y"
by (transfer, auto dest: eq_expgen)


lemma eq_expexpgen: 
  "eq X Y ⟹ (∀ X' X''. X = cExp (cExp cGen X') X'' ⟶ 
                (∃ Y' Y''. Y = cExp (cExp cGen Y') Y'' ∧ 
                   ((eq X' Y' ∧ eq X'' Y'') ∨ (eq X' Y'' ∧ eq X'' Y'))))" 
apply (erule eq.induct, simp_all) 
apply ((drule eq_expgen)+, force)
apply (auto, blast+)
done

lemma Exp_Exp_Gen_inj:
  "Exp (Exp Gen X) X' = Z ⟹
   (∃ Y Y'. Z = Exp (Exp Gen Y) Y' ∧ ((X = Y ∧ X' = Y') ∨ (X = Y' ∧ X' = Y)))"
by (transfer, auto dest: eq_expexpgen)

lemma Exp_Exp_Gen_inj2:
  "Exp (Exp Gen X) X' = Exp Z Y' ⟹
  (Y' = X ∧ Z = Exp Gen X') ∨ (Y' = X' ∧ Z = Exp Gen X)"
apply (transfer, auto)
apply (drule eq_expexpgen, auto)+
done



end