Theory Public

theory Public
imports Event
(*  Title:      HOL/Auth/Public.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge

Theory of Public Keys (common to all public-key protocols)

Private and public keys; initial states of agents

theory Public
imports Event

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

subsection{*Asymmetric Keys*}

datatype keymode = Signature | Encryption

publicKey :: "[keymode,agent] => key"

pubEK :: "agent => key" where
"pubEK == publicKey Encryption"

pubSK :: "agent => key" where
"pubSK == publicKey Signature"

privateKey :: "[keymode, agent] => key" where
"privateKey b A == invKey (publicKey b A)"

(*BEWARE!! priEK, priSK DON'T WORK with inj, range, image, etc.*)
priEK :: "agent => key" where
"priEK A == privateKey Encryption A"

priSK :: "agent => key" where
"priSK A == privateKey Signature A"

text{*These abbreviations give backward compatibility. They represent the
simple situation where the signature and encryption keys are the same.*}

pubK :: "agent => key" where
"pubK A == pubEK A"

priK :: "agent => key" where
"priK A == invKey (pubEK A)"

text{*By freeness of agents, no two agents have the same key. Since
@{term "True≠False"}, no agent has identical signing and encryption keys*}

specification (publicKey)
"publicKey b A = publicKey c A' ==> b=c & A=A'"
apply (rule exI [of _
"%b A. 2 * agent_case 0 (λn. n + 2) 1 A + keymode_case 0 1 b"])
apply (auto simp add: inj_on_def split: agent.split keymode.split)
apply presburger
apply presburger

axiomatization where
(*No private key equals any public key (essential to ensure that private
keys are private!) *)

privateKey_neq_publicKey [iff]: "privateKey b A ≠ publicKey c A'"

lemmas publicKey_neq_privateKey = privateKey_neq_publicKey [THEN not_sym]
declare publicKey_neq_privateKey [iff]

subsection{*Basic properties of @{term pubK} and @{term priK}*}

lemma publicKey_inject [iff]: "(publicKey b A = publicKey c A') = (b=c & A=A')"
by (blast dest!: injective_publicKey)

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

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

lemma symKey_neq_priEK: "K ∈ symKeys ==> K ≠ priEK A"
by auto

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)

lemma analz_symKeys_Decrypt:
"[| Crypt K X ∈ analz H; K ∈ symKeys; Key K ∈ analz H |]
==> X ∈ analz H"

by (auto simp add: symKeys_def)

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 publicKey_image_eq [simp]:
"(publicKey b x ∈ publicKey c ` AA) = (b=c & x ∈ AA)"
by auto

lemma privateKey_notin_image_publicKey [simp]: "privateKey b x ∉ publicKey c ` AA"
by auto

lemma privateKey_image_eq [simp]:
"(privateKey b A ∈ invKey ` publicKey c ` AS) = (b=c & A∈AS)"
by auto

lemma publicKey_notin_image_privateKey [simp]: "publicKey b A ∉ invKey ` publicKey c ` AS"
by auto

subsection{*Symmetric Keys*}

text{*For some protocols, it is convenient to equip agents with symmetric as
well as asymmetric keys. The theory @{text Shared} assumes that all keys
are symmetric.*}

shrK :: "agent => key" --{*long-term shared keys*}

specification (shrK)
inj_shrK: "inj shrK"
--{*No two agents have the same long-term key*}
apply (rule exI [of _ "agent_case 0 (λn. n + 2) 1"])
apply (simp add: inj_on_def split: agent.split)

axiomatization where
sym_shrK [iff]: "shrK X ∈ symKeys" --{*All shared keys are symmetric*}

text{*Injectiveness: Agents' long-term keys are distinct.*}
lemmas shrK_injective = inj_shrK [THEN inj_eq]
declare shrK_injective [iff]

lemma invKey_shrK [simp]: "invKey (shrK A) = shrK A"
by (simp add: invKey_K)

lemma analz_shrK_Decrypt:
"[| Crypt (shrK A) X ∈ analz H; Key(shrK A) ∈ analz H |] ==> X ∈ analz H"
by auto

lemma analz_Decrypt':
"[| Crypt K X ∈ analz H; K ∈ symKeys; Key K ∈ analz H |] ==> X ∈ analz H"
by (auto simp add: invKey_K)

lemma priK_neq_shrK [iff]: "shrK A ≠ privateKey b C"
by (simp add: symKeys_neq_imp_neq)

lemmas shrK_neq_priK = priK_neq_shrK [THEN not_sym]
declare shrK_neq_priK [simp]

lemma pubK_neq_shrK [iff]: "shrK A ≠ publicKey b C"
by (simp add: symKeys_neq_imp_neq)

lemmas shrK_neq_pubK = pubK_neq_shrK [THEN not_sym]
declare shrK_neq_pubK [simp]

lemma priEK_noteq_shrK [simp]: "priEK A ≠ shrK B"
by auto

lemma publicKey_notin_image_shrK [simp]: "publicKey b x ∉ shrK ` AA"
by auto

lemma privateKey_notin_image_shrK [simp]: "privateKey b x ∉ shrK ` AA"
by auto

lemma shrK_notin_image_publicKey [simp]: "shrK x ∉ publicKey b ` AA"
by auto

lemma shrK_notin_image_privateKey [simp]: "shrK x ∉ invKey ` publicKey b ` AA"
by auto

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

text{*For some reason, moving this up can make some proofs loop!*}
declare invKey_K [simp]

subsection{*Initial States of Agents*}

text{*Note: for all practical purposes, all that matters is the initial
knowledge of the Spy. All other agents are automata, merely following the

initState initState

primrec initState where
(*Agents know their private key and all public keys*)
"initState Server =
{Key (priEK Server), Key (priSK Server)} ∪
(Key ` range pubEK) ∪ (Key ` range pubSK) ∪ (Key ` range shrK)"

| initState_Friend:
"initState (Friend i) =
{Key (priEK(Friend i)), Key (priSK(Friend i)), Key (shrK(Friend i))} ∪
(Key ` range pubEK) ∪ (Key ` range pubSK)"

| initState_Spy:
"initState Spy =
(Key ` invKey ` pubEK ` bad) ∪ (Key ` invKey ` pubSK ` bad) ∪
(Key ` shrK ` bad) ∪
(Key ` range pubEK) ∪ (Key ` range pubSK)"


text{*These lemmas allow reasoning about @{term "used evs"} rather than
@{term "knows Spy evs"}, which is useful when there are private Notes.
Because they depend upon the definition of @{term initState}, they cannot
be moved up.*}

lemma used_parts_subset_parts [rule_format]:
"∀X ∈ used evs. parts {X} ⊆ used evs"
apply (induct evs)
prefer 2
apply (simp add: used_Cons split: event.split)
apply (metis Un_iff empty_subsetI insert_subset le_supI1 le_supI2 parts_subset_iff)
txt{*Base case*}
apply (auto dest!: parts_cut simp add: used_Nil)

lemma MPair_used_D: "{|X,Y|} ∈ used H ==> X ∈ used H & Y ∈ used H"
by (drule used_parts_subset_parts, simp, blast)

text{*There was a similar theorem in Event.thy, so perhaps this one can
be moved up if proved directly by induction.*}

lemma MPair_used [elim!]:
"[| {|X,Y|} ∈ used H;
[| X ∈ used H; Y ∈ used H |] ==> P |]
==> P"

by (blast dest: MPair_used_D)

text{*Rewrites should not refer to @{term "initState(Friend i)"} because
that expression is not in normal form.*}

lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}"
apply (unfold keysFor_def)
apply (induct_tac "C")
apply (auto intro: range_eqI)

lemma Crypt_notin_initState: "Crypt K X ∉ parts (initState B)"
by (induct B, auto)

lemma Crypt_notin_used_empty [simp]: "Crypt K X ∉ used []"
by (simp add: Crypt_notin_initState used_Nil)

(*** Basic properties of shrK ***)

(*Agents see their own shared keys!*)
lemma shrK_in_initState [iff]: "Key (shrK A) ∈ initState A"
by (induct_tac "A", auto)

lemma shrK_in_knows [iff]: "Key (shrK A) ∈ knows A evs"
by (simp add: initState_subset_knows [THEN subsetD])

lemma shrK_in_used [iff]: "Key (shrK A) ∈ used evs"
by (rule initState_into_used, blast)

(** Fresh keys never clash with long-term shared keys **)

(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
from long-term shared keys*)

lemma Key_not_used [simp]: "Key K ∉ used evs ==> K ∉ range shrK"
by blast

lemma shrK_neq: "Key K ∉ used evs ==> shrK B ≠ K"
by blast

lemmas neq_shrK = shrK_neq [THEN not_sym]
declare neq_shrK [simp]

subsection{*Function @{term spies} *}

lemma not_SignatureE [elim!]: "b ≠ Signature ==> b = Encryption"
by (cases b, auto)

text{*Agents see their own private keys!*}
lemma priK_in_initState [iff]: "Key (privateKey b A) ∈ initState A"
by (cases A, auto)

text{*Agents see all public keys!*}
lemma publicKey_in_initState [iff]: "Key (publicKey b A) ∈ initState B"
by (cases B, auto)

text{*All public keys are visible*}
lemma spies_pubK [iff]: "Key (publicKey b A) ∈ spies evs"
apply (induct_tac "evs")
apply (auto simp add: imageI knows_Cons split add: event.split)

lemmas analz_spies_pubK = spies_pubK [THEN analz.Inj]
declare analz_spies_pubK [iff]

text{*Spy sees private keys of bad agents!*}
lemma Spy_spies_bad_privateKey [intro!]:
"A ∈ bad ==> Key (privateKey b A) ∈ spies evs"
apply (induct_tac "evs")
apply (auto simp add: imageI knows_Cons split add: event.split)

text{*Spy sees long-term shared keys of bad agents!*}
lemma Spy_spies_bad_shrK [intro!]:
"A ∈ bad ==> Key (shrK A) ∈ spies evs"
apply (induct_tac "evs")
apply (simp_all add: imageI knows_Cons split add: event.split)

lemma publicKey_into_used [iff] :"Key (publicKey b A) ∈ used evs"
apply (rule initState_into_used)
apply (rule publicKey_in_initState [THEN parts.Inj])

lemma privateKey_into_used [iff]: "Key (privateKey b A) ∈ used evs"
apply(rule initState_into_used)
apply(rule priK_in_initState [THEN parts.Inj])

(*For case analysis on whether or not an agent is compromised*)
lemma Crypt_Spy_analz_bad:
"[| Crypt (shrK A) X ∈ analz (knows Spy evs); A ∈ bad |]
==> X ∈ analz (knows Spy evs)"

by force

subsection{*Fresh Nonces*}

lemma Nonce_notin_initState [iff]: "Nonce N ∉ parts (initState B)"
by (induct_tac "B", auto)

lemma Nonce_notin_used_empty [simp]: "Nonce N ∉ used []"
by (simp add: used_Nil)

subsection{*Supply fresh nonces for possibility theorems*}

text{*In any trace, there is an upper bound N on the greatest nonce in use*}
lemma Nonce_supply_lemma: "EX N. ALL n. N<=n --> Nonce n ∉ used evs"
apply (induct_tac "evs")
apply (rule_tac x = 0 in exI)
apply (simp_all (no_asm_simp) add: used_Cons split add: event.split)
apply safe
apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+

lemma Nonce_supply1: "EX N. Nonce N ∉ used evs"
by (rule Nonce_supply_lemma [THEN exE], blast)

lemma Nonce_supply: "Nonce (@ N. Nonce N ∉ used evs) ∉ used evs"
apply (rule Nonce_supply_lemma [THEN exE])
apply (rule someI, fast)

subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*}

lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} Un H"
by blast

lemma insert_Key_image: "insert (Key K) (Key`KK ∪ C) = Key ` (insert K KK) ∪ C"
by blast

lemma Crypt_imp_keysFor :"[|Crypt K X ∈ H; K ∈ symKeys|] ==> K ∈ keysFor H"
by (drule Crypt_imp_invKey_keysFor, simp)

text{*Lemma for the trivial direction of the if-and-only-if of the
Session Key Compromise Theorem*}

lemma analz_image_freshK_lemma:
"(Key K ∈ analz (Key`nE ∪ H)) --> (K ∈ nE | Key K ∈ analz H) ==>
(Key K ∈ analz (Key`nE ∪ H)) = (K ∈ nE | Key K ∈ analz H)"

by (blast intro: analz_mono [THEN [2] rev_subsetD])

lemmas analz_image_freshK_simps =
simp_thms mem_simps --{*these two allow its use with @{text "only:"}*}
image_insert [THEN sym] image_Un [THEN sym] empty_subsetI insert_subset
analz_insert_eq Un_upper2 [THEN analz_mono, THEN subsetD]
Key_not_used insert_Key_image Un_assoc [THEN sym]

ML {*
structure Public =

val analz_image_freshK_ss =
(@{context} delsimps [image_insert, image_Un]
delsimps [@{thm imp_disjL}] (*reduces blow-up*)
addsimps @{thms analz_image_freshK_simps})

(*Tactic for possibility theorems*)
fun possibility_tac ctxt =
REPEAT (*omit used_Says so that Nonces start from different traces!*)
(ALLGOALS (simp_tac (ctxt delsimps [@{thm used_Says}]))
REPEAT_FIRST (eq_assume_tac ORELSE'
resolve_tac [refl, conjI, @{thm Nonce_supply}]))

(*For harder protocols (such as Recur) where we have to set up some
nonces and keys initially*)
fun basic_possibility_tac ctxt =
(ALLGOALS (asm_simp_tac (ctxt setSolver safe_solver))
REPEAT_FIRST (resolve_tac [refl, conjI]))


method_setup analz_freshK = {*
Scan.succeed (fn ctxt =>
(EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
ALLGOALS (asm_simp_tac (put_simpset Public.analz_image_freshK_ss ctxt))]))) *}

"for proving the Session Key Compromise theorem"

subsection{*Specialized Methods for Possibility Theorems*}

method_setup possibility = {*
Scan.succeed (SIMPLE_METHOD o Public.possibility_tac) *}

"for proving possibility theorems"

method_setup basic_possibility = {*
Scan.succeed (SIMPLE_METHOD o Public.basic_possibility_tac) *}

"for proving possibility theorems"