Theory Keys

(*******************************************************************************  
  
  Symmetric (shared) and asymmetric (public/private) keys.
  (based on Larry Paulson's theory Public.thy)


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

section ‹Symmetric and Asymetric Keys›

theory Keys imports Agents begin

text ‹Divide keys into session and long-term keys. Define different kinds
of long-term keys in second step.›

datatype key =    ― ‹long-term keys›
  macK "as"     ― ‹local MACing key›     
| pubK "as"     ― ‹as's public key›
| priK "as"     ― ‹as's private key›


text‹The inverse of a symmetric key is itself; that of a public key
       is the private key and vice versa›

fun invKey :: "key ⇒ key" where
  "invKey (pubK A) = priK A"
| "invKey (priK A) = pubK A"
| "invKey K = K"

definition
  symKeys :: "key set" where
  "symKeys ≡ {K. invKey K = K}"

lemma invKey_K: "K ∈ symKeys ⟹ invKey K = K"
by (simp add: symKeys_def)


text ‹Most lemmas we need come for free with the inductive type definition:
injectiveness and distinctness.›

lemma invKey_invKey_id [simp]: "invKey (invKey K) = K"
by (cases K, auto) 

lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
apply (safe)
apply (drule_tac f=invKey in arg_cong, simp)
done


text ‹We get most lemmas below for free from the inductive definition
of type @{typ key}. Many of these are just proved as a reality check.›


subsection‹Asymmetric Keys›
(******************************************************************************)

text ‹No private key equals any public key (essential to ensure that private
keys are private!). A similar statement an axiom in Paulson's theory!›

lemma privateKey_neq_publicKey: "priK A ≠ pubK A'"
by auto

lemma publicKey_neq_privateKey: "pubK A ≠ priK A'"
by auto


subsection‹Basic properties of @{term pubK} and @{term priK}›

lemma publicKey_inject [iff]: "(pubK A = pubK A') = (A = A')"
by (auto)

lemma not_symKeys_pubK [iff]: "pubK A ∉ symKeys"
by (simp add: symKeys_def)

lemma not_symKeys_priK [iff]: "priK A ∉ symKeys"
by (simp add: symKeys_def)

lemma symKey_neq_priK: "K ∈ symKeys ⟹ K ≠ priK A"
by (auto simp add: symKeys_def)

lemma symKeys_neq_imp_neq: "(K ∈ symKeys) ≠ (K' ∈ symKeys) ⟹ K ≠ K'"
by blast

lemma symKeys_invKey_iff [iff]: "(invKey K ∈ symKeys) = (K ∈ symKeys)"
by (unfold symKeys_def, auto)


subsection‹"Image" equations that hold for injective functions›

lemma invKey_image_eq [simp]: "(invKey x ∈ invKey`A) = (x ∈ A)"
by auto

(*holds because invKey is injective*)

lemma invKey_pubK_image_priK_image [simp]: "invKey ` pubK ` AS = priK ` AS"
by (auto simp add: image_def)

lemma publicKey_notin_image_privateKey: "pubK A ∉ priK ` AS"
by auto

lemma privateKey_notin_image_publicKey: "priK x ∉ pubK ` AA"
by auto

lemma publicKey_image_eq [simp]: "(pubK x ∈ pubK ` AA) = (x ∈ AA)"
by auto

lemma privateKey_image_eq [simp]: "(priK A ∈ priK ` AS) = (A ∈ AS)"
by auto



subsection‹Symmetric Keys›
(******************************************************************************)

text ‹The following was stated as an axiom in Paulson's theory.›

lemma sym_shrK: "macK X ∈ symKeys"   ― ‹All shared keys are symmetric›
by (simp add: symKeys_def)


text ‹Symmetric keys and inversion›

lemma symK_eq_invKey: "⟦ SK = invKey K; SK ∈ symKeys ⟧ ⟹ K = SK" 
by (auto simp add: symKeys_def)


text ‹Image-related lemmas.›

lemma publicKey_notin_image_shrK: "pubK x ∉ macK ` AA"
by auto

lemma privateKey_notin_image_shrK: "priK x ∉ macK ` AA"
by auto

lemma shrK_notin_image_publicKey: "macK x ∉ pubK ` AA"
by auto

lemma shrK_notin_image_privateKey: "macK x ∉ priK ` AA" 
by auto

lemma shrK_image_eq [simp]: "(macK x ∈ macK ` AA) = (x ∈ AA)"
by auto


end