Theory Public_SET

theory Public_SET
imports Event_SET
(*  Title:      HOL/SET_Protocol/Public_SET.thy
Author: Giampaolo Bella
Author: Fabio Massacci
Author: Lawrence C Paulson
*)


header{*The Public-Key Theory, Modified for SET*}

theory Public_SET
imports Event_SET
begin

subsection{*Symmetric and Asymmetric Keys*}

text{*definitions influenced by the wish to assign asymmetric keys
- since the beginning - only to RCA and CAs, namely we need a partial
function on type Agent*}



text{*The SET specs mention two signature keys for CAs - we only have one*}

consts
publicKey :: "[bool, agent] => key"
--{*the boolean is TRUE if a signing key*}

abbreviation "pubEK == publicKey False"
abbreviation "pubSK == publicKey True"

(*BEWARE!! priEK, priSK DON'T WORK with inj, range, image, etc.*)
abbreviation "priEK A == invKey (pubEK A)"
abbreviation "priSK A == invKey (pubSK A)"

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


specification (publicKey)
injective_publicKey:
"publicKey b A = publicKey c A' ==> b=c & A=A'"
(*<*)
apply (rule exI [of _ "%b A. 2 * nat_of_agent A + (if b then 1 else 0)"])
apply (auto simp add: inj_on_def inj_nat_of_agent [THEN inj_eq] split: agent.split)
apply (drule_tac f="%x. x mod 2" in arg_cong, simp add: mod_Suc)+
(*or this, but presburger won't abstract out the function applications
apply presburger+
*)

done
(*>*)

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

privateKey_neq_publicKey [iff]:
"invKey (publicKey b A) ≠ publicKey b' A'"

declare privateKey_neq_publicKey [THEN not_sym, iff]


subsection{*Initial Knowledge*}

text{*This information is not necessary. Each protocol distributes any needed
certificates, and anyway our proofs require a formalization of the Spy's
knowledge only. However, the initial knowledge is as follows:
All agents know RCA's public keys;
RCA and CAs know their own respective keys;
RCA (has already certified and therefore) knows all CAs public keys;
Spy knows all keys of all bad agents.*}


overloading initState "initState"
begin

primrec initState where
(*<*)
initState_CA:
"initState (CA i) =
(if i=0 then Key ` ({priEK RCA, priSK RCA} Un
pubEK ` (range CA) Un pubSK ` (range CA))
else {Key (priEK (CA i)), Key (priSK (CA i)),
Key (pubEK (CA i)), Key (pubSK (CA i)),
Key (pubEK RCA), Key (pubSK RCA)})"


| initState_Cardholder:
"initState (Cardholder i) =
{Key (priEK (Cardholder i)), Key (priSK (Cardholder i)),
Key (pubEK (Cardholder i)), Key (pubSK (Cardholder i)),
Key (pubEK RCA), Key (pubSK RCA)}"


| initState_Merchant:
"initState (Merchant i) =
{Key (priEK (Merchant i)), Key (priSK (Merchant i)),
Key (pubEK (Merchant i)), Key (pubSK (Merchant i)),
Key (pubEK RCA), Key (pubSK RCA)}"


| initState_PG:
"initState (PG i) =
{Key (priEK (PG i)), Key (priSK (PG i)),
Key (pubEK (PG i)), Key (pubSK (PG i)),
Key (pubEK RCA), Key (pubSK RCA)}"

(*>*)
| initState_Spy:
"initState Spy = Key ` (invKey ` pubEK ` bad Un
invKey ` pubSK ` bad Un
range pubEK Un range pubSK)"


end


text{*Injective mapping from agents to PANs: an agent can have only one card*}

consts pan :: "agent => nat"

specification (pan)
inj_pan: "inj pan"
--{*No two agents have the same PAN*}
(*<*)
apply (rule exI [of _ "nat_of_agent"])
apply (simp add: inj_on_def inj_nat_of_agent [THEN inj_eq])
done
(*>*)

declare inj_pan [THEN inj_eq, iff]

consts
XOR :: "nat*nat => nat" --{*no properties are assumed of exclusive-or*}


subsection{*Signature Primitives*}

definition
(* Signature = Message + signed Digest *)
sign :: "[key, msg]=>msg"
where "sign K X = {|X, Crypt K (Hash X) |}"

definition
(* Signature Only = signed Digest Only *)
signOnly :: "[key, msg]=>msg"
where "signOnly K X = Crypt K (Hash X)"

definition
(* Signature for Certificates = Message + signed Message *)
signCert :: "[key, msg]=>msg"
where "signCert K X = {|X, Crypt K X |}"

definition
(* Certification Authority's Certificate.
Contains agent name, a key, a number specifying the key's target use,
a key to sign the entire certificate.

Should prove if signK=priSK RCA and C=CA i,
then Ka=pubEK i or pubSK i depending on T ??
*)

cert :: "[agent, key, msg, key] => msg"
where "cert A Ka T signK = signCert signK {|Agent A, Key Ka, T|}"

definition
(* Cardholder's Certificate.
Contains a PAN, the certified key Ka, the PANSecret PS,
a number specifying the target use for Ka, the signing key signK.
*)

certC :: "[nat, key, nat, msg, key] => msg"
where "certC PAN Ka PS T signK =
signCert signK {|Hash {|Nonce PS, Pan PAN|}, Key Ka, T|}"


(*cert and certA have no repeated elements, so they could be abbreviations,
but that's tricky and makes proofs slower*)


abbreviation "onlyEnc == Number 0"
abbreviation "onlySig == Number (Suc 0)"
abbreviation "authCode == Number (Suc (Suc 0))"

subsection{*Encryption Primitives*}

definition EXcrypt :: "[key,key,msg,msg] => msg" where
--{*Extra Encryption*}
(*K: the symmetric key EK: the public encryption key*)
"EXcrypt K EK M m =
{|Crypt K {|M, Hash m|}, Crypt EK {|Key K, m|}|}"


definition EXHcrypt :: "[key,key,msg,msg] => msg" where
--{*Extra Encryption with Hashing*}
(*K: the symmetric key EK: the public encryption key*)
"EXHcrypt K EK M m =
{|Crypt K {|M, Hash m|}, Crypt EK {|Key K, m, Hash M|}|}"


definition Enc :: "[key,key,key,msg] => msg" where
--{*Simple Encapsulation with SIGNATURE*}
(*SK: the sender's signing key
K: the symmetric key
EK: the public encryption key*)

"Enc SK K EK M =
{|Crypt K (sign SK M), Crypt EK (Key K)|}"


definition EncB :: "[key,key,key,msg,msg] => msg" where
--{*Encapsulation with Baggage. Keys as above, and baggage b.*}
"EncB SK K EK M b =
{|Enc SK K EK {|M, Hash b|}, b|}"



subsection{*Basic Properties of pubEK, pubSK, priEK and priSK *}

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

lemma privateKey_eq_iff [iff]:
"(invKey (publicKey b A) = invKey (publicKey b' A')) = (b=b' & A=A')"
by auto

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

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

lemma symKeys_invKey_eq [simp]: "K ∈ symKeys ==> invKey K = K"
by (simp add: symKeys_def)

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

text{*Can be slow (or even loop) as a simprule*}
lemma symKeys_neq_imp_neq: "(K ∈ symKeys) ≠ (K' ∈ symKeys) ==> K ≠ K'"
by blast

text{*These alternatives to @{text symKeys_neq_imp_neq} don't seem any better
in practice.*}

lemma publicKey_neq_symKey: "K ∈ symKeys ==> publicKey b A ≠ K"
by blast

lemma symKey_neq_publicKey: "K ∈ symKeys ==> K ≠ publicKey b A"
by blast

lemma privateKey_neq_symKey: "K ∈ symKeys ==> invKey (publicKey b A) ≠ K"
by blast

lemma symKey_neq_privateKey: "K ∈ symKeys ==> K ≠ invKey (publicKey b A)"
by blast

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

by auto


subsection{*"Image" Equations That Hold for Injective Functions *}

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

text{*holds because invKey is injective*}
lemma publicKey_image_eq [iff]:
"(publicKey b A ∈ publicKey c ` AS) = (b=c & A∈AS)"
by auto

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

lemma privateKey_notin_image_publicKey [iff]:
"invKey (publicKey b A) ∉ publicKey c ` AS"
by auto

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

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

text{*for proving @{text new_keys_not_used}*}
lemma keysFor_parts_insert:
"[| K ∈ keysFor (parts (insert X H)); X ∈ synth (analz H) |]
==> K ∈ keysFor (parts H) | Key (invKey K) ∈ parts H"

by (force dest!:
parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD]
analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD]
intro: analz_into_parts)

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

text{*Agents see their own private keys!*}
lemma privateKey_in_initStateCA [iff]:
"Key (invKey (publicKey b A)) ∈ initState A"
by (case_tac "A", auto)

text{*Agents see their own public keys!*}
lemma publicKey_in_initStateCA [iff]: "Key (publicKey b A) ∈ initState A"
by (case_tac "A", auto)

text{*RCA sees CAs' public keys! *}
lemma pubK_CA_in_initState_RCA [iff]:
"Key (publicKey b (CA i)) ∈ initState RCA"
by auto


text{*Spy knows all public keys*}
lemma knows_Spy_pubEK_i [iff]: "Key (publicKey b A) ∈ knows Spy evs"
apply (induct_tac "evs")
apply (simp_all add: imageI knows_Cons split add: event.split)
done

declare knows_Spy_pubEK_i [THEN analz.Inj, iff]
(*needed????*)

text{*Spy sees private keys of bad agents! [and obviously public keys too]*}
lemma knows_Spy_bad_privateKey [intro!]:
"A ∈ bad ==> Key (invKey (publicKey b A)) ∈ knows Spy evs"
by (rule initState_subset_knows [THEN subsetD], simp)


subsection{*Fresh Nonces for Possibility Theorems*}

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)

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

lemma Nonce_supply1: "∃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)
done


subsection{*Specialized Methods for Possibility Theorems*}

ML
{*
(*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}, @{thm used_Notes}]))
THEN
REPEAT_FIRST (eq_assume_tac ORELSE'
resolve_tac [refl, conjI, @{thm Nonce_supply}]))

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


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

"for proving possibility theorems"

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

"for proving possibility theorems"


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 Un C) = Key ` (insert K KK) Un C"
by blast

text{*Needed for @{text DK_fresh_not_KeyCryptKey}*}
lemma publicKey_in_used [iff]: "Key (publicKey b A) ∈ used evs"
by auto

lemma privateKey_in_used [iff]: "Key (invKey (publicKey b A)) ∈ used evs"
by (blast intro!: initState_into_used)

text{*Reverse the normal simplification of "image" to build up (not break down)
the set of keys. Based on @{text analz_image_freshK_ss}, but simpler.*}

lemmas analz_image_keys_simps =
simp_thms mem_simps --{*these two allow its use with @{text "only:"}*}
image_insert [THEN sym] image_Un [THEN sym]
rangeI symKeys_neq_imp_neq
insert_Key_singleton insert_Key_image Un_assoc [THEN sym]


(*General lemmas proved by Larry*)

subsection{*Controlled Unfolding of Abbreviations*}

text{*A set is expanded only if a relation is applied to it*}
lemma def_abbrev_simp_relation:
"A = B ==> (A ∈ X) = (B ∈ X) &
(u = A) = (u = B) &
(A = u) = (B = u)"

by auto

text{*A set is expanded only if one of the given functions is applied to it*}
lemma def_abbrev_simp_function:
"A = B
==> parts (insert A X) = parts (insert B X) &
analz (insert A X) = analz (insert B X) &
keysFor (insert A X) = keysFor (insert B X)"

by auto

subsubsection{*Special Simplification Rules for @{term signCert}*}

text{*Avoids duplicating X and its components!*}
lemma parts_insert_signCert:
"parts (insert (signCert K X) H) =
insert {|X, Crypt K X|} (parts (insert (Crypt K X) H))"

by (simp add: signCert_def insert_commute [of X])

text{*Avoids a case split! [X is always available]*}
lemma analz_insert_signCert:
"analz (insert (signCert K X) H) =
insert {|X, Crypt K X|} (insert (Crypt K X) (analz (insert X H)))"

by (simp add: signCert_def insert_commute [of X])

lemma keysFor_insert_signCert: "keysFor (insert (signCert K X) H) = keysFor H"
by (simp add: signCert_def)

text{*Controlled rewrite rules for @{term signCert}, just the definitions
of the others. Encryption primitives are just expanded, despite their huge
redundancy!*}

lemmas abbrev_simps [simp] =
parts_insert_signCert analz_insert_signCert keysFor_insert_signCert
sign_def [THEN def_abbrev_simp_relation]
sign_def [THEN def_abbrev_simp_function]
signCert_def [THEN def_abbrev_simp_relation]
signCert_def [THEN def_abbrev_simp_function]
certC_def [THEN def_abbrev_simp_relation]
certC_def [THEN def_abbrev_simp_function]
cert_def [THEN def_abbrev_simp_relation]
cert_def [THEN def_abbrev_simp_function]
EXcrypt_def [THEN def_abbrev_simp_relation]
EXcrypt_def [THEN def_abbrev_simp_function]
EXHcrypt_def [THEN def_abbrev_simp_relation]
EXHcrypt_def [THEN def_abbrev_simp_function]
Enc_def [THEN def_abbrev_simp_relation]
Enc_def [THEN def_abbrev_simp_function]
EncB_def [THEN def_abbrev_simp_relation]
EncB_def [THEN def_abbrev_simp_function]


subsubsection{*Elimination Rules for Controlled Rewriting *}

lemma Enc_partsE:
"!!R. [|Enc SK K EK M ∈ parts H;
[|Crypt K (sign SK M) ∈ parts H;
Crypt EK (Key K) ∈ parts H|] ==> R|]
==> R"


by (unfold Enc_def, blast)

lemma EncB_partsE:
"!!R. [|EncB SK K EK M b ∈ parts H;
[|Crypt K (sign SK {|M, Hash b|}) ∈ parts H;
Crypt EK (Key K) ∈ parts H;
b ∈ parts H|] ==> R|]
==> R"

by (unfold EncB_def Enc_def, blast)

lemma EXcrypt_partsE:
"!!R. [|EXcrypt K EK M m ∈ parts H;
[|Crypt K {|M, Hash m|} ∈ parts H;
Crypt EK {|Key K, m|} ∈ parts H|] ==> R|]
==> R"

by (unfold EXcrypt_def, blast)


subsection{*Lemmas to Simplify Expressions Involving @{term analz} *}

lemma analz_knows_absorb:
"Key K ∈ analz (knows Spy evs)
==> analz (Key ` (insert K H) ∪ knows Spy evs) =
analz (Key ` H ∪ knows Spy evs)"

by (simp add: analz_insert_eq Un_upper2 [THEN analz_mono, THEN subsetD])

lemma analz_knows_absorb2:
"Key K ∈ analz (knows Spy evs)
==> analz (Key ` (insert X (insert K H)) ∪ knows Spy evs) =
analz (Key ` (insert X H) ∪ knows Spy evs)"

apply (subst insert_commute)
apply (erule analz_knows_absorb)
done

lemma analz_insert_subset_eq:
"[|X ∈ analz (knows Spy evs); knows Spy evs ⊆ H|]
==> analz (insert X H) = analz H"

apply (rule analz_insert_eq)
apply (blast intro: analz_mono [THEN [2] rev_subsetD])
done

lemmas analz_insert_simps =
analz_insert_subset_eq Un_upper2
subset_insertI [THEN [2] subset_trans]


subsection{*Freshness Lemmas*}

lemma in_parts_Says_imp_used:
"[|Key K ∈ parts {X}; Says A B X ∈ set evs|] ==> Key K ∈ used evs"
by (blast intro: parts_trans dest!: Says_imp_knows_Spy [THEN parts.Inj])

text{*A useful rewrite rule with @{term analz_image_keys_simps}*}
lemma Crypt_notin_image_Key: "Crypt K X ∉ Key ` KK"
by auto

lemma fresh_notin_analz_knows_Spy:
"Key K ∉ used evs ==> Key K ∉ analz (knows Spy evs)"
by (auto dest: analz_into_parts)

end