- Installed specific code generator for equality enforcing that
arguments do not have function types, which would result in
an error message during compilation.
- Added test case generators for basic types.
(* Title: HOL/Auth/Public
ID: $Id$
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 = Event:
subsection{*Asymmetric Keys*}
consts
(*the bool is TRUE if a signing key*)
publicKey :: "[bool,agent] => key"
syntax
pubEK :: "agent => key"
pubSK :: "agent => key"
privateKey :: "[bool,agent] => key"
priEK :: "agent => key"
priSK :: "agent => key"
translations
"pubEK" == "publicKey False"
"pubSK" == "publicKey True"
(*BEWARE!! priEK, priSK DON'T WORK with inj, range, image, etc.*)
"privateKey b A" == "invKey (publicKey b A)"
"priEK A" == "privateKey False A"
"priSK A" == "privateKey True A"
text{*These translations give backward compatibility. They represent the
simple situation where the signature and encryption keys are the same.*}
syntax
pubK :: "agent => key"
priK :: "agent => key"
translations
"pubK A" == "pubEK A"
"priK A" == "invKey (pubEK A)"
axioms
(*By freeness of agents, no two agents have the same key. Since true\<noteq>false,
no agent has identical signing and encryption keys*)
injective_publicKey:
"publicKey b A = publicKey c A' ==> b=c & A=A'"
(*No private key equals any public key (essential to ensure that private
keys are private!) *)
privateKey_neq_publicKey [iff]: "privateKey b A \<noteq> publicKey c A'"
declare privateKey_neq_publicKey [THEN not_sym, iff]
subsection{*Basic properties of @{term pubK} and @{term priK}*}
lemma [iff]: "(publicKey b A = publicKey c A') = (b=c & A=A')"
by (blast dest!: injective_publicKey)
lemma not_symKeys_pubK [iff]: "publicKey b A \<notin> symKeys"
by (simp add: symKeys_def)
lemma not_symKeys_priK [iff]: "privateKey b A \<notin> symKeys"
by (simp add: symKeys_def)
lemma symKey_neq_priEK: "K \<in> symKeys ==> K \<noteq> priEK A"
by auto
lemma symKeys_neq_imp_neq: "(K \<in> symKeys) \<noteq> (K' \<in> symKeys) ==> K \<noteq> K'"
by blast
lemma symKeys_invKey_iff [iff]: "(invKey K \<in> symKeys) = (K \<in> symKeys)"
by (unfold symKeys_def, auto)
lemma analz_symKeys_Decrypt:
"[| Crypt K X \<in> analz H; K \<in> symKeys; Key K \<in> analz H |]
==> X \<in> analz H"
by (auto simp add: symKeys_def)
subsection{*"Image" equations that hold for injective functions*}
lemma invKey_image_eq [simp]: "(invKey x \<in> invKey`A) = (x \<in> A)"
by auto
(*holds because invKey is injective*)
lemma publicKey_image_eq [simp]:
"(publicKey b x \<in> publicKey c ` AA) = (b=c & x \<in> AA)"
by auto
lemma privateKey_notin_image_publicKey [simp]: "privateKey b x \<notin> publicKey c ` AA"
by auto
lemma privateKey_image_eq [simp]:
"(privateKey b A \<in> invKey ` publicKey c ` AS) = (b=c & A\<in>AS)"
by auto
lemma publicKey_notin_image_privateKey [simp]: "publicKey b A \<notin> 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.*}
consts
shrK :: "agent => key" --{*long-term shared keys*}
axioms
inj_shrK: "inj shrK" --{*No two agents have the same key*}
sym_shrK [iff]: "shrK X \<in> symKeys" --{*All shared keys are symmetric*}
(*Injectiveness: Agents' long-term keys are distinct.*)
declare inj_shrK [THEN inj_eq, iff]
lemma priK_neq_shrK [iff]: "shrK A \<noteq> privateKey b C"
by (simp add: symKeys_neq_imp_neq)
declare priK_neq_shrK [THEN not_sym, simp]
lemma pubK_neq_shrK [iff]: "shrK A \<noteq> publicKey b C"
by (simp add: symKeys_neq_imp_neq)
declare pubK_neq_shrK [THEN not_sym, simp]
lemma priEK_noteq_shrK [simp]: "priEK A \<noteq> shrK B"
by auto
lemma publicKey_notin_image_shrK [simp]: "publicKey b x \<notin> shrK ` AA"
by auto
lemma privateKey_notin_image_shrK [simp]: "privateKey b x \<notin> shrK ` AA"
by auto
lemma shrK_notin_image_publicKey [simp]: "shrK x \<notin> publicKey b ` AA"
by auto
lemma shrK_notin_image_privateKey [simp]: "shrK x \<notin> invKey ` publicKey b ` AA"
by auto
lemma shrK_image_eq [simp]: "(shrK x \<in> shrK ` AA) = (x \<in> AA)"
by auto
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
protocol.*}
primrec
(*Agents know their private key and all public keys*)
initState_Server:
"initState Server =
{Key (priEK Server), Key (priSK Server)} \<union>
(Key ` range pubEK) \<union> (Key ` range pubSK) \<union> (Key ` range shrK)"
initState_Friend:
"initState (Friend i) =
{Key (priEK(Friend i)), Key (priSK(Friend i)), Key (shrK(Friend i))} \<union>
(Key ` range pubEK) \<union> (Key ` range pubSK)"
initState_Spy:
"initState Spy =
(Key ` invKey ` pubEK ` bad) \<union> (Key ` invKey ` pubSK ` bad) \<union>
(Key ` shrK ` bad) \<union>
(Key ` range pubEK) \<union> (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]:
"\<forall>X \<in> used evs. parts {X} \<subseteq> used evs"
apply (induct evs)
prefer 2
apply (simp add: used_Cons)
apply (rule ballI)
apply (case_tac a, auto)
apply (auto dest!: parts_cut)
txt{*Base case*}
apply (simp add: used_Nil)
done
lemma MPair_used_D: "{|X,Y|} \<in> used H ==> X \<in> used H & Y \<in> used H"
by (drule used_parts_subset_parts, simp, blast)
lemma MPair_used [elim!]:
"[| {|X,Y|} \<in> used H;
[| X \<in> used H; Y \<in> 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)
done
lemma Crypt_notin_initState: "Crypt K X \<notin> parts (initState B)"
by (induct B, auto)
lemma Crypt_notin_used_empty [simp]: "Crypt K X \<notin> 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) \<in> initState A"
by (induct_tac "A", auto)
lemma shrK_in_knows [iff]: "Key (shrK A) \<in> knows A evs"
by (simp add: initState_subset_knows [THEN subsetD])
lemma shrK_in_used [iff]: "Key (shrK A) \<in> 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: "Key K \<notin> used evs ==> K \<notin> range shrK"
by blast
lemma shrK_neq: "Key K \<notin> used evs ==> shrK B \<noteq> K"
by blast
subsection{*Function @{term spies} *}
text{*Agents see their own private keys!*}
lemma priK_in_initState [iff]: "Key (privateKey b A) \<in> initState A"
by (induct_tac "A", auto)
text{*Agents see all public keys!*}
lemma publicKey_in_initState [iff]: "Key (publicKey b A) \<in> initState B"
by (case_tac "B", auto)
text{*All public keys are visible*}
lemma spies_pubK [iff]: "Key (publicKey b A) \<in> spies evs"
apply (induct_tac "evs")
apply (simp_all add: imageI knows_Cons split add: event.split)
done
declare spies_pubK [THEN analz.Inj, iff]
text{*Spy sees private keys of bad agents!*}
lemma Spy_spies_bad_privateKey [intro!]:
"A \<in> bad ==> Key (privateKey b A) \<in> spies evs"
apply (induct_tac "evs")
apply (simp_all add: imageI knows_Cons split add: event.split)
done
text{*Spy sees long-term shared keys of bad agents!*}
lemma Spy_spies_bad_shrK [intro!]:
"A \<in> bad ==> Key (shrK A) \<in> spies evs"
apply (induct_tac "evs")
apply (simp_all add: imageI knows_Cons split add: event.split)
done
lemma publicKey_into_used [iff] :"Key (publicKey b A) \<in> used evs"
apply (rule initState_into_used)
apply (rule publicKey_in_initState [THEN parts.Inj])
done
lemma privateKey_into_used [iff]: "Key (privateKey b A) \<in> used evs"
apply(rule initState_into_used)
apply(rule priK_in_initState [THEN parts.Inj])
done
subsection{*Fresh Nonces*}
lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState B)"
by (induct_tac "B", auto)
lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> 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 \<notin> 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)+
done
lemma Nonce_supply1: "EX N. Nonce N \<notin> used evs"
by (rule Nonce_supply_lemma [THEN exE], blast)
lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs"
apply (rule Nonce_supply_lemma [THEN exE])
apply (rule someI, fast)
done
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 \<union> C) = Key ` (insert K KK) \<union> C"
by blast
ML
{*
val Key_not_used = thm "Key_not_used";
val insert_Key_singleton = thm "insert_Key_singleton";
val insert_Key_image = thm "insert_Key_image";
*}
(*
val not_symKeys_pubK = thm "not_symKeys_pubK";
val not_symKeys_priK = thm "not_symKeys_priK";
val symKeys_neq_imp_neq = thm "symKeys_neq_imp_neq";
val analz_symKeys_Decrypt = thm "analz_symKeys_Decrypt";
val invKey_image_eq = thm "invKey_image_eq";
val pubK_image_eq = thm "pubK_image_eq";
val priK_pubK_image_eq = thm "priK_pubK_image_eq";
val keysFor_parts_initState = thm "keysFor_parts_initState";
val priK_in_initState = thm "priK_in_initState";
val spies_pubK = thm "spies_pubK";
val Spy_spies_bad = thm "Spy_spies_bad";
val Nonce_notin_initState = thm "Nonce_notin_initState";
val Nonce_notin_used_empty = thm "Nonce_notin_used_empty";
*)
lemma invKey_K [simp]: "K \<in> symKeys ==> invKey K = K"
by (simp add: symKeys_def)
lemma Crypt_imp_keysFor :"[|K \<in> symKeys; Crypt K X \<in> H|] ==> K \<in> keysFor H"
by (drule Crypt_imp_invKey_keysFor, simp)
subsection{*Specialized Methods for Possibility Theorems*}
ML
{*
val Nonce_supply1 = thm "Nonce_supply1";
val Nonce_supply = thm "Nonce_supply";
(*Tactic for possibility theorems (Isar interface)*)
fun gen_possibility_tac ss state = state |>
REPEAT (*omit used_Says so that Nonces start from different traces!*)
(ALLGOALS (simp_tac (ss delsimps [used_Says]))
THEN
REPEAT_FIRST (eq_assume_tac ORELSE'
resolve_tac [refl, conjI, Nonce_supply]))
(*Tactic for possibility theorems (ML script version)*)
fun possibility_tac state = gen_possibility_tac (simpset()) state
*}
method_setup possibility = {*
Method.ctxt_args (fn ctxt =>
Method.METHOD (fn facts =>
gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *}
"for proving possibility theorems"
lemmas analz_image_freshK_simps =
simp_thms mem_simps --{*these two allow its use with @{text "only:"}*}
disj_comms
image_insert [THEN sym] image_Un [THEN sym] empty_subsetI insert_subset
analz_insert_eq Un_upper2 [THEN analz_mono, THEN [2] rev_subsetD]
insert_Key_singleton
Key_not_used insert_Key_image Un_assoc [THEN sym]
ML
{*
val analz_image_freshK_ss =
simpset() delsimps [image_insert, image_Un]
delsimps [imp_disjL] (*reduces blow-up*)
addsimps thms"analz_image_freshK_simps"
*}
axioms
Key_supply_ax: "finite KK ==> \<exists>K\<in>symKeys. K \<notin> KK & Key K \<notin> used evs"
--{*Unlike the corresponding property of nonces, this cannot be proved.
We have infinitely many agents and there is nothing to stop their
long-term keys from exhausting all the natural numbers. The axiom
assumes that their keys are dispersed so as to leave room for infinitely
many fresh session keys. We could, alternatively, restrict agents to
an unspecified finite number. We could however replace @{term"used evs"}
by @{term "used []"}.*}
lemma Key_supply1: "\<exists>K\<in>symKeys. Key K \<notin> used evs"
by (rule Finites.emptyI [THEN Key_supply_ax, THEN bexE], blast)
end