# Theory Smartcard

(* Author:     Giampaolo Bella, Catania University
*)

sectionTheory of smartcards

theory Smartcard
imports EventSC
begin

text
As smartcards handle long-term (symmetric) keys, this theoy extends and
supersedes theory Private.thy

An agent is bad if she reveals her PIN to the spy, not the shared key that
is embedded in her card. An agent's being bad implies nothing about her
smartcard, which independently may be stolen or cloned.

axiomatization
shrK    :: "agent => key" and  (*long-term keys saved in smart cards*)
crdK    :: "card  => key" and  (*smart cards' symmetric keys*)
pin     :: "agent => key" and  (*pin to activate the smart cards*)

(*Mostly for Shoup-Rubin*)
Pairkey :: "agent * agent => nat" and
pairK   :: "agent * agent => key"
where
inj_shrK: "inj shrK" and  ― ‹No two smartcards store the same key
inj_crdK: "inj crdK" and  ― ‹Nor do two cards
inj_pin : "inj pin" and   ― ‹Nor do two agents have the same pin

(*pairK is injective on each component, if we assume encryption to be a PRF
or at least collision free *)
inj_pairK    [iff]: "(pairK(A,B) = pairK(A',B')) = (A = A' & B = B')" and
comm_Pairkey [iff]: "Pairkey(A,B) = Pairkey(B,A)" and

(*long-term keys differ from each other*)
pairK_disj_crdK [iff]: "pairK(A,B)  crdK C" and
pairK_disj_shrK [iff]: "pairK(A,B)  shrK P" and
pairK_disj_pin [iff]:  "pairK(A,B)  pin P" and
shrK_disj_crdK [iff]:  "shrK P  crdK C" and
shrK_disj_pin [iff]:  "shrK P  pin Q" and
crdK_disj_pin [iff]:   "crdK C  pin P"

definition legalUse :: "card => bool" ("legalUse (_)") where
"legalUse C == C  stolen"

primrec illegalUse :: "card  => bool" where
illegalUse_def: "illegalUse (Card A) = ( (Card A  stolen  A  bad)    Card A  cloned )"

textinitState must be defined with care

initState  initState
begin

primrec initState where
(*Server knows all long-term keys; adding cards' keys may be redundant but
helps prove crdK_in_initState and crdK_in_used to distinguish cards' keys
from fresh (session) keys*)
initState_Server:  "initState Server =
(Key`(range shrK  range crdK  range pin  range pairK))
(Nonce`(range Pairkey))" |

(*Other agents know only their own*)
initState_Friend:  "initState (Friend i) = {Key (pin (Friend i))}" |

(*Spy knows bad agents' pins, cloned cards' keys, pairKs, and Pairkeys *)
initState_Spy: "initState Spy  =
(Key`((pin`bad)  (pin `{A. Card A  cloned})
(shrK`{A. Card A  cloned})
(crdK`cloned)
(pairK`{(X,A). Card A  cloned})))
(Nonce`(Pairkey`{(A,B). Card A  cloned & Card B  cloned}))"

end

textStill relying on axioms
axiomatization where
Key_supply_ax:  "finite KK   K. K  KK & Key K  used evs" and

(*Needed because of Spy's knowledge of Pairkeys*)
Nonce_supply_ax: "finite NN   N. N  NN & Nonce N  used evs"

subsectionBasic properties of shrK

(*Injectiveness: Agents' long-term keys are distinct.*)
declare inj_shrK [THEN inj_eq, iff]
declare inj_crdK [THEN inj_eq, iff]
declare inj_pin  [THEN inj_eq, iff]

lemma invKey_K [simp]: "invKey K = K"
apply (insert isSym_keys)
done

lemma analz_Decrypt' [dest]:
" Crypt K X  analz H;  Key K   analz H   X  analz H"
by auto

textNow cancel the dest› attribute given to
analz.Decrypt› in its declaration.
declare analz.Decrypt [rule del]

textRewrites should not refer to  terminitState(Friend i) because
that expression is not in normal form.

textAdded to extend initstate with set of nonces
lemma parts_image_Nonce [simp]: "parts (Nonce`N) = Nonce`N"
by auto

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

(*Specialized to shared-key model: no @{term invKey}*)
lemma keysFor_parts_insert:
" K  keysFor (parts (insert X G));  X  synth (analz H)
K  keysFor (parts (G  H)) | Key K  parts H"
by (force dest: EventSC.keysFor_parts_insert)

lemma Crypt_imp_keysFor: "Crypt K X  H  K  keysFor H"
by (drule Crypt_imp_invKey_keysFor, simp)

subsectionFunction "knows"

(*Spy knows the pins of bad agents!*)
apply (induct_tac "evs")
apply (simp_all (no_asm_simp) add: imageI knows_Cons split: event.split)
done

(*Spy knows the long-term keys of cloned cards!*)
lemma Spy_knows_cloned [intro!]:
"Card A  cloned   Key (crdK (Card A))  knows Spy evs &
Key (shrK A)  knows Spy evs &
Key (pin A)   knows Spy evs &
( B. Key (pairK(B,A))  knows Spy evs)"
apply (induct_tac "evs")
apply (simp_all (no_asm_simp) add: imageI knows_Cons split: event.split)
done

lemma Spy_knows_cloned1 [intro!]: "C  cloned  Key (crdK C)  knows Spy evs"
apply (induct_tac "evs")
apply (simp_all (no_asm_simp) add: imageI knows_Cons split: event.split)
done

lemma Spy_knows_cloned2 [intro!]: " Card A  cloned; Card B  cloned
Nonce (Pairkey(A,B)) knows Spy evs"
apply (induct_tac "evs")
apply (simp_all (no_asm_simp) add: imageI knows_Cons split: event.split)
done

(*Spy only knows pins of bad agents!*)
apply (induct_tac "evs")
apply (simp_all (no_asm_simp) add: imageI knows_Cons split: event.split)
done

(*For case analysis on whether or not an agent is compromised*)
" Crypt (pin A) X  analz (knows Spy evs);  Abad
X  analz (knows Spy evs)"
apply (force dest!: analz.Decrypt)
done

(** Fresh keys never clash with other keys **)

lemma shrK_in_initState [iff]:
apply (induct_tac "A")
apply auto
done

lemma shrK_in_used [iff]: "Key (shrK A)  used evs"
apply (rule initState_into_used)
apply blast
done

lemma crdK_in_initState [iff]:
apply (induct_tac "A")
apply auto
done

lemma crdK_in_used [iff]: "Key (crdK A)  used evs"
apply (rule initState_into_used)
apply blast
done

lemma pin_in_initState [iff]: "Key (pin A)  initState A"
apply (induct_tac "A")
apply auto
done

lemma pin_in_used [iff]: "Key (pin A)  used evs"
apply (rule initState_into_used)
apply blast
done

lemma pairK_in_initState [iff]:
apply (induct_tac "X")
apply auto
done

lemma pairK_in_used [iff]: "Key (pairK X)  used evs"
apply (rule initState_into_used)
apply blast
done

(*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 [simp]: "Key K  used evs  shrK B  K"
by blast

lemma crdK_not_used [simp]: "Key K  used evs  K  range crdK"
apply clarify
done

lemma crdK_neq [simp]: "Key K  used evs  crdK C  K"
apply clarify
done

lemma pin_not_used [simp]: "Key K  used evs  K  range pin"
apply clarify
done

lemma pin_neq [simp]: "Key K  used evs  pin A  K"
apply clarify
done

lemma pairK_not_used [simp]: "Key K  used evs  K  range pairK"
apply clarify
done

lemma pairK_neq [simp]: "Key K  used evs  pairK(A,B)  K"
apply clarify
done

declare shrK_neq [THEN not_sym, simp]
declare crdK_neq [THEN not_sym, simp]
declare pin_neq [THEN not_sym, simp]
declare pairK_neq [THEN not_sym, simp]

subsectionFresh nonces

lemma Nonce_notin_initState [iff]: "Nonce N  parts (initState (Friend i))"
by auto

(*This lemma no longer holds of smartcard protocols, where the cards can store
nonces.

lemma Nonce_notin_used_empty [simp]: "Nonce N ∉ used []"
done

So, we must use old-style supply fresh nonce theorems relying on the appropriate axiom*)

subsectionSupply fresh nonces for possibility theorems.

lemma Nonce_supply1: "N. Nonce N  used evs"
apply (rule finite.emptyI [THEN Nonce_supply_ax, THEN exE], blast)
done

lemma Nonce_supply2:
"N N'. Nonce N  used evs & Nonce N'  used evs' & N  N'"
apply (cut_tac evs = evs in finite.emptyI [THEN Nonce_supply_ax])
apply (erule exE)
apply (cut_tac evs = evs' in finite.emptyI [THEN finite.insertI, THEN Nonce_supply_ax])
apply auto
done

lemma Nonce_supply3: "N N' N''. Nonce N  used evs & Nonce N'  used evs' &
Nonce N''  used evs'' & N  N' & N'  N'' & N  N''"
apply (cut_tac evs = evs in finite.emptyI [THEN Nonce_supply_ax])
apply (erule exE)
apply (cut_tac evs = evs' and a1 = N in finite.emptyI [THEN finite.insertI, THEN Nonce_supply_ax])
apply (erule exE)
apply (cut_tac evs = evs'' and a1 = Na and a2 = N in finite.emptyI [THEN finite.insertI, THEN finite.insertI, THEN Nonce_supply_ax])
apply blast
done

lemma Nonce_supply: "Nonce (SOME N. Nonce N  used evs)  used evs"
apply (rule finite.emptyI [THEN Nonce_supply_ax, THEN exE])
apply (rule someI, blast)
done

textUnlike the corresponding property of nonces, we cannot prove
termfinite KK  K. K  KK & Key K  used evs.
We have infinitely many agents and there is nothing to stop their
long-term keys from exhausting all the natural numbers.  Instead,
possibility theorems must assume the existence of a few keys.

subsectionSpecialized Rewriting for Theorems About termanalz and Image

lemma subset_Compl_range_shrK: "A  - (range shrK)  shrK x  A"
by blast

lemma subset_Compl_range_crdK: "A  - (range crdK)  crdK x  A"
apply blast
done

lemma subset_Compl_range_pin: "A  - (range pin)  pin x  A"
apply blast
done

lemma subset_Compl_range_pairK: "A  - (range pairK)  pairK x  A"
apply blast
done
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

(** Reverse the normal simplification of "image" to build up (not break down)
the set of keys.  Use analz_insert_eq with (Un_upper2 RS analz_mono) to
erase occurrences of forwarded message components (X). **)

lemmas analz_image_freshK_simps =
simp_thms mem_simps ― ‹these two allow its use with 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 subset_Compl_range_shrK subset_Compl_range_crdK
subset_Compl_range_pin subset_Compl_range_pairK
Key_not_used insert_Key_image Un_assoc [THEN sym]

(*Lemma for the trivial direction of the if-and-only-if*)
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])

subsectionTactics for possibility theorems

ML

structure Smartcard =
struct

(*Omitting used_Says makes the tactic much faster: it leaves expressions
such as  Nonce ?N ∉ used evs that match Nonce_supply*)
fun possibility_tac ctxt =
(REPEAT
(ALLGOALS (simp_tac (ctxt
delsimps @{thms used_Cons_simps}
setSolver safe_solver))
THEN
REPEAT_FIRST (eq_assume_tac ORELSE'
resolve_tac ctxt [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 =
REPEAT
(ALLGOALS (asm_simp_tac (ctxt setSolver safe_solver))
THEN
REPEAT_FIRST (resolve_tac ctxt [refl, conjI]))

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

(*Lets blast_tac perform this step without needing the simplifier*)
lemma invKey_shrK_iff [iff]:
"(Key (invKey K)  X) = (Key K  X)"
by auto

(*Specialized methods*)

method_setup analz_freshK =
Scan.succeed (fn ctxt =>
(SIMPLE_METHOD
(EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]),
REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}),
ALLGOALS (asm_simp_tac (put_simpset Smartcard.analz_image_freshK_ss ctxt))])))
"for proving the Session Key Compromise theorem"

method_setup possibility =
Scan.succeed (fn ctxt =>
SIMPLE_METHOD (Smartcard.possibility_tac ctxt))
"for proving possibility theorems"

method_setup basic_possibility =
Scan.succeed (fn ctxt =>
SIMPLE_METHOD (Smartcard.basic_possibility_tac ctxt))
"for proving possibility theorems"

lemma knows_subset_knows_Cons: "knows A evs  knows A (e # evs)"
by (induct e) (auto simp: knows_Cons)

(*Needed for actual protocols that will follow*)
declare shrK_disj_crdK[THEN not_sym, iff]
declare shrK_disj_pin[THEN not_sym, iff]
declare pairK_disj_shrK[THEN not_sym, iff]
declare pairK_disj_crdK[THEN not_sym, iff]
declare pairK_disj_pin[THEN not_sym, iff]
declare crdK_disj_pin[THEN not_sym, iff]

declare legalUse_def [iff] illegalUse_def [iff]

end