Theory s0g_secrecy
section ‹Secrecy with Leaking (global version)›
theory s0g_secrecy imports Refinement Agents
begin
text ‹This model extends the global secrecy model by adding a ‹leak›
event, which models that the adversary can learn messages through leaks of
some (unspecified) kind.›
text ‹Proof tool configuration. Avoid annoying automatic unfolding of
‹dom›.›
declare domIff [simp, iff del]
subsection ‹State›
text ‹The only state variable is a knowledge relation, an authorization
relation, and a leakage relation.
@{term "(d, A) ∈ kn s"} means that the agent @{term "A"} knows data @{term "d"}.
@{term "(d, A) ∈ az s"} means that the agent @{term "A"} is authorized to
know data @{term "d"}.
@{term "(d, A) ∈ lk s"} means that data @{term "d"} has leaked to agent
@{term "A"}. Leakage models potential unauthorized knowledge.
›
record 'd s0g_state =
kn :: "('d × agent) set"
az :: "('d × agent) set"
lk :: "'d set"
type_synonym
'd s0g_obs = "'d s0g_state"
abbreviation
"lkr s ≡ lk s × UNIV"
subsection ‹Invariant definitions›
text ‹Global secrecy is stated as an invariant.›
definition
s0g_secrecy :: "'d s0g_state set"
where
"s0g_secrecy ≡ {s. kn s ⊆ az s ∪ lkr s}"
lemmas s0g_secrecyI = s0g_secrecy_def [THEN setc_def_to_intro, rule_format]
lemmas s0g_secrecyE [elim] =
s0g_secrecy_def [THEN setc_def_to_elim, rule_format]
text ‹Data that someone is authorized to know and leaked data is known
by someone.›
definition
s0g_dom :: "'d s0g_state set"
where
"s0g_dom ≡ {s. Domain (az s ∪ lkr s) ⊆ Domain (kn s)}"
lemmas s0g_domI = s0g_dom_def [THEN setc_def_to_intro, rule_format]
lemmas s0g_domE [elim] = s0g_dom_def [THEN setc_def_to_elim, rule_format]
subsection ‹Events›
text ‹New secrets may be generated anytime.›
definition
s0g_gen :: "['d, agent, agent set] ⇒ ('d s0g_state × 'd s0g_state) set"
where
"s0g_gen d A G ≡ {(s, s1).
A ∈ G ∧
d ∉ Domain (kn s) ∧
s1 = s⦇
kn := insert (d, A) (kn s),
az := az s ∪ {d} × (if G ∩ bad = {} then G else UNIV)
⦈
}"
text ‹Learning secrets.›
definition
s0g_learn ::
"['d, agent] ⇒ ('d s0g_state × 'd s0g_state) set"
where
"s0g_learn d B ≡ {(s, s1).
(d, B) ∈ az s ∪ lkr s ∧
s1 = s⦇ kn := insert (d, B) (kn s) ⦈
}"
text ‹Leaking secrets.›
definition
s0g_leak ::
"'d ⇒ ('d s0g_state × 'd s0g_state) set"
where
"s0g_leak d ≡ {(s, s1).
d ∈ Domain (kn s) ∧
s1 = s⦇ lk := insert d (lk s) ⦈
}"
subsection ‹Specification›
definition
s0g_init :: "'d s0g_state set"
where
"s0g_init ≡ s0g_secrecy ∩ s0g_dom"
definition
s0g_trans :: "('d s0g_state × 'd s0g_state) set" where
"s0g_trans ≡ (⋃d A B G.
s0g_gen d A G ∪
s0g_learn d B ∪
s0g_leak d ∪
Id
)"
definition
s0g :: "('d s0g_state, 'd s0g_obs) spec" where
"s0g ≡ ⦇
init = s0g_init,
trans = s0g_trans,
obs = id
⦈"
lemmas s0g_defs =
s0g_def s0g_init_def s0g_trans_def
s0g_gen_def s0g_learn_def s0g_leak_def
lemma s0g_obs_id [simp]: "obs s0g = id"
by (simp add: s0g_def)
text ‹All state predicates are trivially observable.›
lemma s0g_anyP_observable [iff]: "observable (obs s0g) P"
by (auto)
subsection ‹Invariant proofs›
subsection ‹inv1: Secrecy›
lemma PO_s0g_secrecy_init [iff]:
"init s0g ⊆ s0g_secrecy"
by (auto simp add: s0g_defs intro!: s0g_secrecyI)
lemma PO_s0g_secrecy_trans [iff]:
"{s0g_secrecy} trans s0g {> s0g_secrecy}"
apply (auto simp add: s0g_defs PO_hoare_defs intro!: s0g_secrecyI)
apply (auto)
done
lemma PO_s0g_secrecy [iff]:"reach s0g ⊆ s0g_secrecy"
by (rule inv_rule_basic, auto)
text ‹As en external invariant.›
lemma PO_s0g_obs_secrecy [iff]:"oreach s0g ⊆ s0g_secrecy"
by (rule external_from_internal_invariant) (auto del: subsetI)
subsection ‹inv2: Authorized and leaked data is known to someone›
lemma PO_s0g_dom_init [iff]:
"init s0g ⊆ s0g_dom"
by (auto simp add: s0g_defs intro!: s0g_domI)
lemma PO_s0g_dom_trans [iff]:
"{s0g_dom} trans s0g {> s0g_dom}"
apply (auto simp add: s0g_defs PO_hoare_defs intro!: s0g_domI)
apply (blast)+
done
lemma PO_s0g_dom [iff]: "reach s0g ⊆ s0g_dom"
by (rule inv_rule_basic, auto)
text ‹As en external invariant.›
lemma PO_s0g_obs_dom [iff]: "oreach s0g ⊆ s0g_dom"
by (rule external_from_internal_invariant) (auto del: subsetI)
end