(* Title: HOL/SET_Protocol/Public_SET.thy
Author: Giampaolo Bella
Author: Fabio Massacci
Author: Lawrence C Paulson
*)
section‹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
🍋‹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}
∪
pubEK ` (range CA)
∪ 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 \
invKey ` pubSK ` bad
∪
range pubEK
∪ 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 ‹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
‹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: 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: 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 (SOME 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 ctxt [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 |> Simplifier.set_unsafe_solver safe_solver))
THEN
REPEAT_FIRST (resolve_tac ctxt [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
🍋‹analz
› and Image
›
lemma insert_Key_singleton:
"insert (Key K) H = Key ` {K} \ H"
by blast
lemma insert_Key_image:
"insert (Key K) (Key`KK \ C) = Key ` (insert K KK) \ C"
by blast
text‹Needed
for ‹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
‹analz_image_freshK_ss
›, but simpler.
›
lemmas analz_image_keys_simps =
simp_thms mem_simps
🍋 ‹these two allow its
use with ‹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 🍋‹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 🍋‹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
🍋‹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 🍋‹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
