(* Title: HOL/Auth/Shared.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
Theory of Shared Keys (common to all symmetric-key protocols)
Shared, long-term keys; initial states of agents
*)
theory Shared
imports Event All_Symmetric
begin
consts
shrK ::
"agent \ key" (*symmetric keys*)
specification (shrK)
inj_shrK:
"inj shrK"
🍋 ‹No two agents
have the same long-term key
›
apply (rule exI [of _
"case_agent 0 (\n. n + 2) 1"])
apply (simp add: inj_on_def split: agent.split)
done
text‹Server knows all long-term keys; other agents know only their own
›
overloading
initState
≡ initState
begin
primrec initState
where
initState_Server:
"initState Server = Key ` range shrK"
| initState_Friend:
"initState (Friend i) = {Key (shrK (Friend i))}"
| initState_Spy:
"initState Spy = Key`shrK`bad"
end
subsection‹Basic properties of shrK
›
(*Injectiveness: Agents' long-term keys are distinct.*)
lemmas shrK_injective = inj_shrK [
THEN inj_eq]
declare shrK_injective [iff]
lemma invKey_K [simp]:
"invKey K = K"
apply (insert isSym_keys)
apply (simp add: symKeys_def)
done
lemma analz_Decrypt
' [dest]:
"\Crypt K X \ analz H; Key K \ analz H\ \ X \ analz H"
by auto
text‹Now cancel the
‹dest
› attribute given
to
‹analz.Decrypt
› in its
declaration.
›
declare analz.Decrypt [rule del]
text‹Rewrites should not refer
to 🍋‹initState(Friend i)
› because
that expression
is not
in normal form.
›
lemma keysFor_parts_initState [simp]:
"keysFor (parts (initState C)) = {}"
unfolding 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 (metis invKey_K keysFor_parts_insert)
lemma Crypt_imp_keysFor:
"Crypt K X \ H \ K \ keysFor H"
by (metis Crypt_imp_invKey_keysFor invKey_K)
subsection‹Function "knows"›
(*Spy sees shared keys of agents!*)
lemma Spy_knows_Spy_bad [intro!]:
"A \ bad \ Key (shrK A) \ knows Spy evs"
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*)
lemma Crypt_Spy_analz_bad:
"\Crypt (shrK A) X \ analz (knows Spy evs); A \ bad\
==> X
∈ analz (knows Spy evs)
"
by (metis Spy_knows_Spy_bad analz.Inj analz_Decrypt
')
(** Fresh keys never clash with long-term shared keys **)
(*Agents see their own shared keys!*)
lemma shrK_in_initState [iff]:
"Key (shrK A) \ initState A"
by (induct_tac
"A", auto)
lemma shrK_in_used [iff]:
"Key (shrK A) \ used evs"
by (rule initState_into_used, blast)
(*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
lemmas shrK_sym_neq = shrK_neq [
THEN not_sym]
declare shrK_sym_neq [simp]
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.
›
(*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 (no_asm_simp) add: used_Cons split: event.split)
apply (metis le_sup_iff msg_Nonce_supply)
done
lemma Nonce_supply1:
"\N. Nonce N \ used evs"
by (metis Nonce_supply_lemma order_eq_iff)
lemma Nonce_supply2:
"\N N'. Nonce N \ used evs \ Nonce N' \ used evs' \ N \ N'"
apply (cut_tac evs = evs
in Nonce_supply_lemma)
apply (cut_tac evs =
"evs'" in Nonce_supply_lemma, clarify)
apply (metis Suc_n_not_le_n nat_le_linear)
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 Nonce_supply_lemma)
apply (cut_tac evs =
"evs'" in Nonce_supply_lemma)
apply (cut_tac evs =
"evs''" in Nonce_supply_lemma, clarify)
apply (rule_tac x = N
in exI)
apply (rule_tac x =
"Suc (N+Na)" in exI)
apply (rule_tac x =
"Suc (Suc (N+Na+Nb))" in exI)
apply (simp (no_asm_simp) add: less_not_refl3 le_add1 le_add2 less_Suc_eq_le)
done
lemma Nonce_supply:
"Nonce (SOME N. Nonce N \ used evs) \ used evs"
apply (rule Nonce_supply_lemma [
THEN exE])
apply (rule someI, blast)
done
text‹Unlike the corresponding property of nonces, we cannot prove
🍋‹finite 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.
›
subsection‹Specialized Rewriting
for Theorems About
🍋‹analz
› and Image
›
lemma subset_Compl_range:
"A \ - (range shrK) \ shrK x \ A"
by blast
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
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])
subsection‹Tactics
for possibility
theorems›
ML
‹
structure Shared =
struct
(*Omitting used_Says makes the tactic much faster: it leaves expressions
such as Nonce ?N \<notin> used evs that match Nonce_supply*)
fun possibility_tac ctxt =
(REPEAT
(ALLGOALS (simp_tac (ctxt
delsimps [@{
thm used_Says}, @{
thm used_Notes}, @{
thm used_Gets}]
|> Simplifier.set_unsafe_solver 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 |> Simplifier.set_unsafe_solver safe_solver))
THEN
REPEAT_FIRST (resolve_tac ctxt [refl, conjI]))
val analz_image_freshK_ss =
simpset_of
(
🍋 |> Simplifier.del_simps @{thms image_insert image_Un}
|> Simplifier.del_simps @{thms imp_disjL}
(*reduces blow-up*)
|> Simplifier.add_simps @{thms analz_image_freshK_simps})
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 @{thms allI ballI impI}),
REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}),
ALLGOALS (asm_simp_tac (put_simpset Shared.analz_image_freshK_ss ctxt))])))
›
"for proving the Session Key Compromise theorem"
method_setup possibility =
‹
Scan.succeed (fn ctxt => SIMPLE_METHOD (Shared.possibility_tac ctxt))
›
"for proving possibility theorems"
method_setup basic_possibility =
‹
Scan.succeed (fn ctxt => SIMPLE_METHOD (Shared.basic_possibility_tac ctxt))
›
"for proving possibility theorems"
lemma knows_subset_knows_Cons:
"knows A evs \ knows A (e # evs)"
by (cases e) (auto simp: knows_Cons)
end
