Theory Keys

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

  Project: Development of Security Protocols by Refinement

  Module:  Refinement/Keys.thy (Isabelle/HOL 2016-1)
  ID:      $Id: Keys.thy 132773 2016-12-09 15:30:22Z csprenge $
  Author:  Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>
  
  Symmetric (shared) and asymmetric (public/private) keys.
  (based on Larry Paulson's theory Public.thy)

  Copyright (c) 2012-2016 Christoph Sprenger 
  Licence: LGPL

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

section ‹Symmetric and Assymetric 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 ltkey =    ― ‹long-term keys›
  sharK "agent"     ― ‹key shared with server›
| publK "agent"     ― ‹agent's public key›
| privK "agent"     ― ‹agent's private key›

datatype key = 
  sesK "fresh_t"   ― ‹session key›
| ltK "ltkey"      ― ‹long-term key›

abbreviation
  shrK :: "agent  key" where
  "shrK A  ltK (sharK A)"

abbreviation
  pubK :: "agent  key" where
  "pubK A  ltK (publK A)"

abbreviation
  priK :: "agent  key" where
  "priK A  ltK (privK A)"


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 (ltK (publK A)) = priK A"
| "invKey (ltK (privK 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) 
   (rename_tac ltk, case_tac ltk, 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_sesK: "sesK f  symKeys"   ― ‹All session keys are symmetric›
by (simp add: symKeys_def)

lemma sym_shrK: "shrK 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  shrK ` AA"
by auto

lemma privateKey_notin_image_shrK: "priK x  shrK ` AA"
by auto

lemma shrK_notin_image_publicKey: "shrK x  pubK ` AA"
by auto

lemma shrK_notin_image_privateKey: "shrK x  priK ` AA" 
by auto

lemma sesK_notin_image_shrK [simp]: "sesK K  shrK`AA"
by (auto)

lemma shrK_notin_image_sesK [simp]: "shrK K  sesK`AA"
by (auto)

lemma sesK_image_eq [simp]: "(sesK x  sesK ` AA) = (x  AA)"
by auto

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


end