Theory Event_Systems
chapter‹Verification Infrastructure›
text‹Here we define event systems, the term algebra, and the Dolev--Yao adversary›
section ‹Event Systems›
text ‹This theory contains definitions of event systems, trace, traces, reachability, simulation,
and proves the soundness of simulation for proving trace inclusion. We also derive some related
simulation rules.›
theory Event_Systems
imports Main
begin
record ('e, 's) ES =
init :: "'s ⇒ bool"
trans :: "'s ⇒ 'e ⇒ 's ⇒ bool" ("(4_: _─_→ _)" [50, 50, 50] 90)
subsection ‹Reachable states and invariants›
inductive
reach :: "('e, 's) ES ⇒ 's ⇒ bool" for E
where
reach_init [simp, intro]: "init E s ⟹ reach E s"
| reach_trans [intro]: "⟦ E: s ─e→ s'; reach E s ⟧ ⟹ reach E s'"
thm reach.induct
text ‹Abbreviation for stating that a predicate is an invariant of an event system.›
definition Inv :: "('e, 's) ES ⇒ ('s ⇒ bool) ⇒ bool" where
"Inv E I ⟷ (∀s. reach E s ⟶ I s)"
lemmas InvI = Inv_def [THEN iffD2, rule_format]
lemmas InvE [elim] = Inv_def [THEN iffD1, elim_format, rule_format]
lemma Invariant_rule [case_names Inv_init Inv_trans]:
assumes "⋀s0. init E s0 ⟹ I s0"
and "⋀s e s'. ⟦E: s ─e→ s'; reach E s; I s⟧ ⟹ I s'"
shows "Inv E I"
unfolding Inv_def
proof (intro allI impI)
fix s
assume "reach E s"
then show "I s" using assms
by (induction s rule: reach.induct) (auto)
qed
text ‹Invariant rule that allows strengthening the proof with another invariant.›
lemma Invariant_rule_Inv [case_names Inv_other Inv_init Inv_trans]:
assumes "Inv E J"
and "⋀s0. init E s0 ⟹ I s0"
and "⋀s e s'. ⟦E: s ─e→ s'; reach E s; I s; J s; J s'⟧ ⟹ I s'"
shows "Inv E I"
unfolding Inv_def
proof (intro allI impI)
fix s
assume "reach E s"
then show "I s" using assms
by (induction s rule: reach.induct)(auto 3 4)
qed
subsection ‹Traces›
type_synonym 'e trace = "'e list"
inductive
trace :: "('e, 's) ES ⇒ 's ⇒ 'e trace ⇒ 's ⇒ bool" ("(4_: _ ─⟨_⟩→ _)" [50, 50, 50] 90)
for E s
where
trace_nil [simp,intro!]:
"E: s ─⟨[]⟩→ s"
| trace_snoc [intro]:
"⟦ E: s ─⟨τ⟩→ s'; E: s' ─e→ s'' ⟧ ⟹ E: s ─⟨τ @ [e]⟩→ s''"
thm trace.induct
inductive_cases trace_nil_invert [elim!]: "E: s ─⟨[]⟩→ t"
inductive_cases trace_snoc_invert [elim]: "E: s ─⟨τ @ [e]⟩→ t"
lemma trace_init_independence [elim]:
assumes "E: s ─⟨τ⟩→ s'" "trans E = trans F"
shows "F: s ─⟨τ⟩→ s'"
using assms
by (induction rule: trace.induct) auto
lemma trace_single [simp, intro!]: "⟦ E: s ─e→ s' ⟧ ⟹ E: s ─⟨[e]⟩→ s'"
by (auto intro: trace_snoc[where τ = "[]", simplified])
text ‹Next, we prove an introduction rule for a "cons" trace and a case analysis rule
distinguishing the empty trace and a "cons" trace.›
lemma trace_consI:
assumes
"E: s'' ─⟨τ⟩→ s'" "E: s ─e→ s''"
shows
"E: s ─⟨e # τ⟩→ s'"
using assms
by (induction rule: trace.induct) (auto dest: trace_snoc)
lemma trace_cases_cons:
assumes
"E: s ─⟨τ⟩→ s'"
"⟦ τ = []; s' = s ⟧ ⟹ P"
"⋀e τ' s''. ⟦ τ = e # τ'; E: s ─e→ s''; E: s'' ─⟨τ'⟩→ s' ⟧ ⟹ P"
shows "P"
using assms
by (induction rule: trace.induct) fastforce+
lemma trace_consD: "(E: s ─⟨e # τ⟩→ s') ⟹ ∃ s''. (E: s ─e→ s'') ∧ (E: s'' ─⟨τ⟩→ s')"
by(auto elim: trace_cases_cons)
text ‹We show how a trace can be appended to another.›
lemma trace_append: "(E: s ─⟨τ⇩1⟩→ s') ∧ (E: s' ─⟨τ⇩2⟩→ s'') ⟹ E: s ─⟨τ⇩1@τ⇩2⟩→ s''"
by(induction τ⇩1 arbitrary: s)
(auto dest!: trace_consD intro: trace_consI)
lemma trace_append_invert: "(E: s ─⟨τ⇩1@τ⇩2⟩→ s'') ⟹ ∃s' . (E: s ─⟨τ⇩1⟩→ s') ∧ (E: s' ─⟨τ⇩2⟩→ s'')"
by (induction τ⇩1 arbitrary: s) (auto intro!: trace_consI dest!: trace_consD)
text‹We prove an induction scheme for combining two traces, similar to @{text list_induct2}.›
lemma trace_induct2 [consumes 3, case_names Nil Snoc]:
"⟦E: s ─⟨τ⟩→ s''; F: t ─⟨σ⟩→ t''; length τ = length σ;
P [] s [] t;
⋀τ s' e s'' σ t' f t''.
⟦E: s ─⟨τ⟩→ s'; E: s'─e→ s''; F: t ─⟨σ⟩→ t'; F: t'─f→ t''; P τ s' σ t'⟧
⟹ P (τ @ [e]) s'' (σ @ [f]) t''⟧
⟹ P τ s'' σ t''"
proof (induction τ s'' arbitrary: σ t'' rule: trace.induct)
case trace_nil
then show ?case by auto
next
case (trace_snoc τ s' e s'')
from ‹length (τ @ [e]) = length σ› and ‹F: t ─⟨σ⟩→ t''›
obtain f σ' t'
where "σ = σ' @ [f]" "length τ = length σ'" "F: t ─⟨σ'⟩→ t'" "F: t' ─f→ t''"
by (auto elim: trace.cases)
then show ?case using trace_snoc by blast
qed
subsubsection ‹Relate traces to reachability and invariants›
lemma reach_trace_equiv: "reach E s ⟷ (∃s0 τ. init E s0 ∧ E: s0 ─⟨τ⟩→ s)" (is "?A ⟷ ?B")
proof
assume "?A" then show "?B"
by (induction s rule: reach.induct) auto
next
assume "?B"
then obtain s0 τ where "E: s0 ─⟨τ⟩→ s" "init E s0" by blast
then show "?A"
by (induction τ s rule: trace.induct) auto
qed
lemma reach_traceI: "⟦init E s0; E: s0 ─⟨τ⟩→ s⟧ ⟹ reach E s"
by(auto simp add: reach_trace_equiv)
lemma reach_trace_extend: "⟦E: s ─⟨τ⟩→ s'; reach E s⟧ ⟹ reach E s'"
by (induction τ s' rule: trace.induct) auto
lemma Inv_trace: "⟦Inv E I; init E s0; E: s0 ─⟨τ⟩→ s'⟧ ⟹ I s'"
by (auto simp add: Inv_def reach_trace_equiv)
subsubsection ‹Trace semantics of event systems›
text ‹We define the set of traces of an event system.›
definition traces :: "('e, 's) ES ⇒ 'e trace set" where
"traces E = {τ. ∃s s'. init E s ∧ E: s ─⟨τ⟩→ s'}"
lemma tracesI [intro]: "⟦ init E s; E: s ─⟨τ⟩→ s' ⟧ ⟹ τ ∈ traces E"
by (auto simp add: traces_def)
lemma tracesE [elim]: "⟦ τ ∈ traces E; ⋀s s'. ⟦ init E s; E: s ─⟨τ⟩→ s' ⟧ ⟹ P ⟧ ⟹ P"
by (auto simp add: traces_def)
lemma traces_nil [simp, intro!]: "init E s ⟹ [] ∈ traces E"
by (auto simp add: traces_def)
text‹We now define a trace property satisfaction relation: an event system satisfies a property
@{term "φ"}, if its traces are contained in @{term φ}.›
definition trace_property :: "('e, 's) ES ⇒ 'e trace set ⇒ bool" (infix "⊨⇩E⇩S" 90) where
"E ⊨⇩E⇩S φ ⟷ traces E ⊆ φ"
lemmas trace_propertyI = trace_property_def [THEN iffD2, OF subsetI, rule_format]
lemmas trace_propertyE [elim] = trace_property_def [THEN iffD1, THEN subsetD, elim_format]
lemmas trace_propertyD = trace_property_def [THEN iffD1, THEN subsetD, rule_format]
text ‹Rules for showing trace properties using a stronger trace-state invariant.›
lemma trace_invariant:
assumes
"τ ∈ traces E"
"⋀s s'. ⟦ init E s; E: s ─⟨τ⟩→ s' ⟧ ⟹ I τ s'"
"⋀s. I τ s ⟹ τ ∈ φ"
shows "τ ∈ φ" using assms
by (auto)
lemma trace_property_rule:
assumes
"⋀s0. init E s0 ⟹ I [] s0"
"⋀s s' τ e s''.
⟦ init E s; E: s ─⟨τ⟩→ s'; E: s' ─e→ s''; I τ s'; reach E s' ⟧ ⟹ I (τ@[e]) s''"
"⋀τ s. ⟦ I τ s; reach E s ⟧ ⟹ τ ∈ φ"
shows "E ⊨⇩E⇩S φ"
proof (rule trace_propertyI, erule trace_invariant[where I="λτ s. I τ s ∧ reach E s"])
fix τ s s'
assume "E: s ─⟨τ⟩→ s'" and "init E s"
then show "I τ s' ∧ reach E s'"
by (induction τ s' rule: trace.induct) (auto simp add: assms)
qed (auto simp add: assms)
text ‹Similar to @{thm trace_property_rule}, but allows matching pure state invariants directly.›
lemma Inv_trace_property:
assumes "Inv E I" and "[] ∈ φ"
and "(⋀s τ s' e s''.
⟦init E s; E: s ─⟨τ⟩→ s'; E: s' ─e→ s''; I s; I s'; reach E s'; τ ∈ φ⟧ ⟹ τ@[e] ∈ φ)"
shows "E ⊨⇩E⇩S φ"
using assms(1,2)
by (intro trace_property_rule[where I="λτ s. τ ∈ φ"]) (auto intro: assms(3))
subsection ‹Simulation›
text ‹We first define the simulation preorder on pairs of states and derive a series of
useful coinduction principles.›
coinductive
sim :: "('e, 's ) ES ⇒ ('f, 't ) ES ⇒ ('e ⇒ 'f) ⇒ 's ⇒ 't ⇒ bool"
for E F π
where
"⟦ ⋀e s'. (E: s ─e→ s') ⟹ ∃t'. (F: t ─π e→ t') ∧ sim E F π s' t' ⟧ ⟹ sim E F π s t"
abbreviation
simS :: "('e, 's ) ES ⇒ ('f, 't ) ES ⇒ 's ⇒ ('e ⇒ 'f) ⇒ 't ⇒ bool"
("(5_,_: _ ⊑⇩_ _)" [50, 50, 50, 60, 50] 90)
where
"simS E F s π t ≡ sim E F π s t"
lemmas sim_coinduct_id = sim.coinduct[where π=id, consumes 1, case_names sim]
text ‹We prove a simplified and slightly weaker coinduction rule for simulation and
register it as the default rule for @{term sim}.›
lemma sim_coinduct_weak [consumes 1, case_names sim, coinduct pred: sim]:
assumes
"R s t"
"⋀s t a s'. ⟦ R s t; E: s─a→ s'⟧ ⟹ (∃t'. (F: t─π a→ t') ∧ R s' t')"
shows
"E,F: s ⊑⇩π t"
using assms
by (coinduction arbitrary: s t rule: sim.coinduct) (fastforce)
lemma sim_refl: "E,E: s ⊑⇩id s"
by (coinduction arbitrary: s) auto
lemma sim_trans: "⟦ E,F: s ⊑⇩π1 t; F,G: t ⊑⇩π2 u ⟧ ⟹ E,G: s ⊑⇩(π2 ∘ π1) u"
proof (coinduction arbitrary: s t u)
case (sim a s' s t)
with ‹E,F: s ⊑⇩π1 t› obtain t' where "F: t ─π1 a→ t'" "E,F: s' ⊑⇩π1 t'"
by (cases rule: sim.cases) auto
moreover
from ‹F,G: t ⊑⇩π2 u› ‹F: t ─π1 a→ t'› obtain u' where "G: u ─π2 (π1 a)→ u'" "F,G: t' ⊑⇩π2 u'"
by (cases rule: sim.cases) auto
ultimately
have "∃t' u'. (G: u ─π2 (π1 a)→ u') ∧ (E,F: s' ⊑⇩π1 t') ∧ (F,G: t' ⊑⇩π2 u')"
by auto
then show ?case by auto
qed
text ‹Extend transition simulation to traces.›
lemma trace_sim:
assumes "E: s ─⟨τ⟩→ s'" "E,F: s ⊑⇩π t"
shows "∃t'. (F: t ─⟨map π τ⟩→ t') ∧ (E,F: s' ⊑⇩π t')"
using assms
proof (induction τ s' rule: trace.induct)
case trace_nil
then show ?case by auto
next
case (trace_snoc τ s' e s'')
then obtain t' where "F: t ─⟨map π τ⟩→ t'" "E,F: s' ⊑⇩π t'" by auto
from ‹E,F: s' ⊑⇩π t'› ‹E: s'─e→ s''›
obtain t'' where "F: t' ─π e→ t''" "E,F: s'' ⊑⇩π t''" by (elim sim.cases) fastforce
then show ?case using ‹F: t ─⟨map π τ⟩→ t'› ‹E: s ─⟨τ⟩→ s'› ‹E: s'─e→ s''› by auto
qed
subsubsection ‹Simulation for event systems›
definition
sim_ES :: "('e, 's ) ES ⇒ ('e ⇒ 'f) ⇒ ('f, 't ) ES ⇒ bool" ("(3_ ⊑⇩_ _)" [50, 60, 50] 95)
where
"E ⊑⇩π F ⟷ (∃R.
(∀s0. init E s0 ⟶ (∃t0. init F t0 ∧ R s0 t0)) ∧
(∀s t. R s t ⟶ E,F: s ⊑⇩π t))"
lemma sim_ES_I:
assumes
"⋀s0. init E s0 ⟹ (∃t0. init F t0 ∧ R s0 t0)" and
"⋀s t. R s t ⟹ E,F: s ⊑⇩π t"
shows "E ⊑⇩π F"
using assms
by (auto simp add: sim_ES_def)
lemma sim_ES_E:
assumes
"E ⊑⇩π F"
"⋀R. ⟦ ⋀s0. init E s0 ⟹ (∃t0. init F t0 ∧ R s0 t0); ⋀s t. R s t ⟹ E,F: s ⊑⇩π t ⟧ ⟹ P"
shows "P"
using assms
by (auto simp add: sim_ES_def)
text ‹Different rules to set up a simulation proof. Include reachability or weaker invariant(s)
in precondition of ``simulation square''.›
lemma simulate_ES:
assumes
init: "⋀s0. init E s0 ⟹ (∃t0. init F t0 ∧ R s0 t0)" and
step: "⋀s t a s'. ⟦ R s t; reach E s; reach F t; E: s─a→ s' ⟧
⟹ (∃t'. (F: t─π a→ t') ∧ R s' t')"
shows "E ⊑⇩π F"
by (auto 4 4 intro!: sim_ES_I[where R="λs t. R s t ∧ reach E s ∧ reach F t"] dest: init
intro: sim_coinduct_weak[where R="λs t. R s t ∧ reach E s ∧ reach F t"] dest: step)
lemma simulate_ES_with_invariants:
assumes
init: "⋀s0. init E s0 ⟹ (∃t0. init F t0 ∧ R s0 t0)" and
step: "⋀s t a s'.
⟦ R s t; I s; J t; E: s─a→ s' ⟧ ⟹ (∃t'. (F: t─π a→ t') ∧ R s' t')" and
invE: "⋀s. reach E s ⟶ I s" and
invE: "⋀t. reach F t ⟶ J t"
shows "E ⊑⇩π F" using assms
by (auto intro: simulate_ES[where R=R])
lemmas simulate_ES_with_invariant = simulate_ES_with_invariants[where J="λs. True", simplified]
text ‹Variants with a functional simulation relation, aka refinement mapping.›
lemma simulate_ES_fun:
assumes
init: "⋀s0. init E s0 ⟹ init F (h s0)" and
step: "⋀s a s'. ⟦ E: s─a→ s'; reach E s; reach F (h s) ⟧ ⟹ F: h s─π a→ h s'"
shows "E ⊑⇩π F"
using assms
by (auto intro!: simulate_ES[where R="λs t. t = h s"])
lemma simulate_ES_fun_with_invariants:
assumes
init: "⋀s0. init E s0 ⟹ init F (h s0)" and
step: "⋀s a s'. ⟦ E: s─a→ s'; I s; J (h s) ⟧ ⟹ F: h s─π a→ h s'" and
invE: "⋀s. reach E s ⟶ I s" and
invF: "⋀t. reach F t ⟶ J t"
shows "E ⊑⇩π F"
using assms
by (auto intro!: simulate_ES_fun)
lemmas simulate_ES_fun_with_invariant =
simulate_ES_fun_with_invariants[where J="λt. True", simplified]
text ‹Reflexivity and transitivity for ES simulation.›
lemma sim_ES_refl: "E ⊑⇩id E"
by (auto intro: sim_ES_I[where R="(=)"] sim_refl)
lemma sim_ES_trans:
assumes "E ⊑⇩π1 F" and "F ⊑⇩π2 G" shows "E ⊑⇩(π2 ∘ π1) G"
proof -
from ‹E ⊑⇩π1 F› obtain R⇩1 where
"⋀s0. init E s0 ⟹ (∃t0. init F t0 ∧ R⇩1 s0 t0)"
"⋀s t. R⇩1 s t ⟹ E,F: s ⊑⇩π1 t"
by (auto elim!: sim_ES_E)
moreover
from ‹F ⊑⇩π2 G› obtain R⇩2 where
"⋀t0. init F t0 ⟹ (∃u0. init G u0 ∧ R⇩2 t0 u0)"
"⋀t u. R⇩2 t u ⟹ F,G: t ⊑⇩π2 u"
by (auto elim!: sim_ES_E)
ultimately show ?thesis
by (auto intro!: sim_ES_I[where R="R⇩1 OO R⇩2"] sim_trans simp add: OO_def) blast
qed
subsubsection ‹Soundness for trace inclusion and property preservation›
lemma simulation_soundness: "E ⊑⇩π F ⟹ (map π)`traces E ⊆ traces F"
by (fastforce simp add: sim_ES_def image_def dest: trace_sim)
lemmas simulation_rule = simulate_ES [THEN simulation_soundness]
lemmas simulation_rule_id = simulation_rule[where π="id", simplified]
text ‹This allows us to show that properties are preserved under simulation.›
corollary property_preservation:
"⟦E ⊑⇩π F; F ⊨⇩E⇩S P; ⋀τ. map π τ ∈ P ⟹ τ ∈ Q ⟧ ⟹ E ⊨⇩E⇩S Q"
by (auto simp add: trace_property_def dest: simulation_soundness)
subsection ‹Simulation up to simulation preorder›
lemma sim_coinduct_upto_sim [consumes 1, case_names sim]:
assumes
major: "R s t" and
S: "⋀s t a s'. ⟦ R s t; E: s ─a→ s'⟧ ⟹
∃t'. (F: t ─π a→ t') ∧ ((sim E E id) OO R OO (sim F F id)) s' t'"
shows
"E,F: s ⊑⇩π t"
proof -
let ?R_upto = "((sim E E id) OO R OO (sim F F id))"
from major have "?R_upto s t" by (auto intro: sim_refl)
then show ?thesis
proof (coinduction arbitrary: s t)
case (sim a s' s t)
from ‹((sim E E id) OO R OO (sim F F id)) s t› obtain s1 t1 where
"E,E: s ⊑⇩id s1" "R s1 t1" "F,F: t1 ⊑⇩id t" by (elim relcomppE)
from ‹E,E: s ⊑⇩id s1› ‹E: s─a→ s'›
obtain s1' where "E: s1─a→ s1'" "E,E: s' ⊑⇩id s1'" by (cases rule: sim.cases) auto
from ‹R s1 t1› ‹E: s1─a→ s1'› S
obtain t1' where "F: t1─π a→ t1'" "?R_upto s1' t1'" by force
from ‹F,F: t1 ⊑⇩id t› ‹F: t1─π a→ t1'›
obtain t' where "F: t─π a→ t'" "F,F: t1' ⊑⇩id t'" by (cases rule: sim.cases) auto
from ‹F: t─π a→ t'› ‹E,E: s' ⊑⇩id s1'› ‹?R_upto s1' t1'› ‹F,F: t1' ⊑⇩id t'›
have "((sim E E id) OO R OO (sim F F id)) s' t'"
apply(auto simp add: OO_def) using comp_id sim_trans by metis
then have "∃t'. (F: t─π a→ t') ∧ ?R_upto s' t'"
using ‹F: t─π a→ t'› by (auto intro: sim_trans)
then show ?case using S by fastforce
qed
qed
end