Theory Unwinding_fin
section ‹Unwinding Proof Method for Finitary Relative Security›
text ‹ This theory formalizes the notion of unwinding for finitary relative security,
and proves its soundness. ›
theory Unwinding_fin
imports Relative_Security
begin
subsection ‹ The types and operators underlying unwinding: status, matching operators, etc. ›
context Rel_Sec
begin
datatype status = Eq | Diff
fun updStat :: "status ⇒ bool × 'a ⇒ bool × 'a ⇒ status" where
"updStat Eq (True,a) (True,a') = (if a = a' then Eq else Diff)"
|"updStat stat _ _ = stat"
definition "sstatO' statO sv1 sv2 = updStat statO (isIntV sv1, getObsV sv1) (isIntV sv2, getObsV sv2)"
definition "sstatA' statA s1 s2 = updStat statA (isIntO s1, getObsO s1) (isIntO s2, getObsO s2)"
definition initCond ::
"(enat ⇒ 'stateO ⇒ 'stateO ⇒ status ⇒ 'stateV ⇒ 'stateV ⇒ status ⇒ bool) ⇒ bool" where
"initCond Δ ≡ ∀s1 s2.
istateO s1 ∧ istateO s2
⟶
(∃sv1 sv2. istateV sv1 ∧ istateV sv2 ∧ corrState sv1 s1 ∧ corrState sv2 s2
∧ Δ ∞ s1 s2 Eq sv1 sv2 Eq)"
definition "match1_1 Δ s1 s1' s2 statA sv1 sv2 statO ≡
∃sv1'. validTransV (sv1,sv1') ∧
Δ ∞ s1' s2 statA sv1' sv2 statO"
definition "match1_12 Δ s1 s1' s2 statA sv1 sv2 statO ≡
∃sv1' sv2'.
let statO' = sstatO' statO sv1 sv2 in
validTransV (sv1,sv1') ∧
validTransV (sv2,sv2') ∧
Δ ∞ s1' s2 statA sv1' sv2' statO'"
definition "match1 Δ s1 s2 statA sv1 sv2 statO ≡
¬ isIntO s1 ⟶
(∀s1'. validTransO (s1,s1')
⟶
(¬ isSecO s1 ∧ Δ ∞ s1' s2 statA sv1 sv2 statO) ∨
(eqSec sv1 s1 ∧ ¬ isIntV sv1 ∧ match1_1 Δ s1 s1' s2 statA sv1 sv2 statO) ∨
(eqSec sv1 s1 ∧ ¬ isSecV sv2 ∧ Van.eqAct sv1 sv2 ∧ match1_12 Δ s1 s1' s2 statA sv1 sv2 statO))"
lemmas match1_defs = match1_def match1_1_def match1_12_def
lemma match1_1_mono:
"Δ ≤ Δ' ⟹ match1_1 Δ s1 s1' s2 statA sv1 sv2 statO ⟹ match1_1 Δ' s1 s1' s2 statA sv1 sv2 statO"
unfolding le_fun_def match1_1_def by auto
lemma match1_12_mono:
"Δ ≤ Δ' ⟹ match1_12 Δ s1 s1' s2 statA sv1 sv2 statO ⟹ match1_12 Δ' s1 s1' s2 statA sv1 sv2 statO"
unfolding le_fun_def match1_12_def by fastforce
lemma match1_mono:
assumes "Δ ≤ Δ'"
shows "match1 Δ s1 s2 statA sv1 sv2 statO ⟹ match1 Δ' s1 s2 statA sv1 sv2 statO"
unfolding match1_def apply clarify subgoal for s1' apply(erule allE[of _ s1'])
using match1_1_mono[OF assms, of s1 s1' s2 statA sv1 sv2 statO]
match1_12_mono[OF assms, of s1 s1' s2 statA sv1 sv2 statO]
assms[unfolded le_fun_def, rule_format, of _ s1' s2 statA sv1 sv2 statO]
by auto .
definition "match2_1 Δ s1 s2 s2' statA sv1 sv2 statO ≡
∃sv2'. validTransV (sv2,sv2') ∧
Δ ∞ s1 s2' statA sv1 sv2' statO"
definition "match2_12 Δ s1 s2 s2' statA sv1 sv2 statO ≡
∃sv1' sv2'.
let statO' = sstatO' statO sv1 sv2 in
validTransV (sv1,sv1') ∧
validTransV (sv2,sv2') ∧
Δ ∞ s1 s2' statA sv1' sv2' statO'"
definition "match2 Δ s1 s2 statA sv1 sv2 statO ≡
¬ isIntO s2 ⟶
(∀s2'. validTransO (s2,s2')
⟶
(¬ isSecO s2 ∧ Δ ∞ s1 s2' statA sv1 sv2 statO) ∨
(eqSec sv2 s2 ∧ ¬ isIntV sv2 ∧ match2_1 Δ s1 s2 s2' statA sv1 sv2 statO) ∨
(¬ isSecV sv1 ∧ eqSec sv2 s2 ∧ Van.eqAct sv1 sv2 ∧ match2_12 Δ s1 s2 s2' statA sv1 sv2 statO))"
lemmas match2_defs = match2_def match2_1_def match2_12_def
lemma match2_1_mono:
"Δ ≤ Δ' ⟹ match2_1 Δ s1 s1' s2 statA sv1 sv2 statO ⟹ match2_1 Δ' s1 s1' s2 statA sv1 sv2 statO"
unfolding le_fun_def match2_1_def by auto
lemma match2_12_mono:
"Δ ≤ Δ' ⟹ match2_12 Δ s1 s1' s2 statA sv1 sv2 statO ⟹ match2_12 Δ' s1 s1' s2 statA sv1 sv2 statO"
unfolding le_fun_def match2_12_def by fastforce
lemma match2_mono:
assumes "Δ ≤ Δ'"
shows "match2 Δ s1 s2 statA sv1 sv2 statO ⟹ match2 Δ' s1 s2 statA sv1 sv2 statO"
unfolding match2_def apply clarify subgoal for s2' apply(erule allE[of _ s2'])
using match2_1_mono[OF assms, of s1 s2 s2' statA sv1 sv2 statO]
match2_12_mono[OF assms, of s1 s2 s2' statA sv1 sv2 statO]
assms[unfolded le_fun_def, rule_format, of _ s1 s2' statA sv1 sv2 statO]
by auto .
definition "match12_1 Δ s1' s2' statA' sv1 sv2 statO ≡
∃sv1'. validTransV (sv1,sv1') ∧
Δ ∞ s1' s2' statA' sv1' sv2 statO"
definition "match12_2 Δ s1' s2' statA' sv1 sv2 statO ≡
∃sv2'. validTransV (sv2,sv2') ∧
Δ ∞ s1' s2' statA' sv1 sv2' statO"
definition "match12_12 Δ s1' s2' statA' sv1 sv2 statO ≡
∃sv1' sv2'.
let statO' = sstatO' statO sv1 sv2 in
validTransV (sv1,sv1') ∧
validTransV (sv2,sv2') ∧
(statA' = Diff ⟶ statO' = Diff) ∧
Δ ∞ s1' s2' statA' sv1' sv2' statO'"
definition "match12 Δ s1 s2 statA sv1 sv2 statO ≡
∀s1' s2'.
let statA' = sstatA' statA s1 s2 in
validTransO (s1,s1') ∧
validTransO (s2,s2') ∧
Opt.eqAct s1 s2 ∧
isIntO s1 ∧ isIntO s2
⟶
(¬ isSecO s1 ∧ ¬ isSecO s2 ∧ (statA = statA' ∨ statO = Diff) ∧ Δ ∞ s1' s2' statA' sv1 sv2 statO)
∨
(¬ isSecO s2 ∧ eqSec sv1 s1 ∧ ¬ isIntV sv1 ∧
(statA = statA' ∨ statO = Diff) ∧
match12_1 Δ s1' s2' statA' sv1 sv2 statO)
∨
(¬ isSecO s1 ∧ eqSec sv2 s2 ∧ ¬ isIntV sv2 ∧
(statA = statA' ∨ statO = Diff) ∧
match12_2 Δ s1' s2' statA' sv1 sv2 statO)
∨
(eqSec sv1 s1 ∧ eqSec sv2 s2 ∧ Van.eqAct sv1 sv2 ∧
match12_12 Δ s1' s2' statA' sv1 sv2 statO)"
lemmas match12_defs = match12_def match12_1_def match12_2_def match12_12_def
lemma match12_simpleI:
assumes "⋀s1' s2' statA'.
statA' = sstatA' statA s1 s2 ⟹
validTransO (s1,s1') ⟹
validTransO (s2,s2') ⟹
Opt.eqAct s1 s2 ⟹
(¬ isSecO s1 ∧ ¬ isSecO s2 ∧ (statA = statA' ∨ statO = Diff) ∧ Δ ∞ s1' s2' statA' sv1 sv2 statO)
∨
(eqSec sv1 s1 ∧ eqSec sv2 s2 ∧ Van.eqAct sv1 sv2 ∧
match12_12 Δ s1' s2' statA' sv1 sv2 statO)"
shows "match12 Δ s1 s2 statA sv1 sv2 statO"
using assms unfolding match12_def Let_def by blast
lemma match12_1_mono:
"Δ ≤ Δ' ⟹ match12_1 Δ s1' s2' statA' sv1 sv2 statO ⟹ match12_1 Δ' s1' s2' statA' sv1 sv2 statO"
unfolding le_fun_def match12_1_def by auto
lemma match12_2_mono:
"Δ ≤ Δ' ⟹ match12_2 Δ s1 s2' statA' sv1 sv2 statO ⟹ match12_2 Δ' s1 s2' statA' sv1 sv2 statO"
unfolding le_fun_def match12_2_def by auto
lemma match12_12_mono:
"Δ ≤ Δ' ⟹ match12_12 Δ s1' s2' statA' sv1 sv2 statO ⟹ match12_12 Δ' s1' s2' statA' sv1 sv2 statO"
unfolding le_fun_def match12_12_def by fastforce
lemma match12_mono:
assumes "Δ ≤ Δ'"
shows "match12 Δ s1 s2 statA sv1 sv2 statO ⟹ match12 Δ' s1 s2 statA sv1 sv2 statO"
unfolding match12_def apply clarify subgoal for s1' s2' apply(erule allE[of _ s1']) apply(erule allE[of _ s2'])
using match12_1_mono[OF assms, of s1' s2' _ sv1 sv2 statO]
match12_2_mono[OF assms, of s1' s2' _ sv1 sv2 statO]
match12_12_mono[OF assms, of s1' s2' _ sv1 sv2 statO]
assms[unfolded le_fun_def, rule_format, of _ s1' s2'
"sstatA' statA s1 s2" sv1 sv2 statO]
by simp metis .
definition "match Δ s1 s2 statA sv1 sv2 statO ≡
match1 Δ s1 s2 statA sv1 sv2 statO
∧
match2 Δ s1 s2 statA sv1 sv2 statO
∧
match12 Δ s1 s2 statA sv1 sv2 statO"
lemmas match_defs = match1_def match2_def match12_def
lemmas match_deep_defs = match1_defs match2_defs match12_defs
lemma match_mono:
assumes "Δ ≤ Δ'"
shows "match Δ s1 s2 statA sv1 sv2 statO ⟹ match Δ' s1 s2 statA sv1 sv2 statO"
unfolding match_def using match1_mono[OF assms] match2_mono[OF assms] match12_mono[OF assms] by auto
definition "move_1 Δ w s1 s2 statA sv1 sv2 statO ≡
∃sv1'. validTransV (sv1,sv1') ∧
Δ w s1 s2 statA sv1' sv2 statO"
definition "move_2 Δ w s1 s2 statA sv1 sv2 statO ≡
∃sv2'. validTransV (sv2,sv2') ∧
Δ w s1 s2 statA sv1 sv2' statO"
definition "move_12 Δ w s1 s2 statA sv1 sv2 statO ≡
∃sv1' sv2'.
let statO' = sstatO' statO sv1 sv2 in
validTransV (sv1,sv1') ∧ validTransV (sv2,sv2') ∧
Δ w s1 s2 statA sv1' sv2' statO'"
definition "proact Δ w s1 s2 statA sv1 sv2 statO ≡
(¬ isSecV sv1 ∧ ¬ isIntV sv1 ∧ move_1 Δ w s1 s2 statA sv1 sv2 statO)
∨
(¬ isSecV sv2 ∧ ¬ isIntV sv2 ∧ move_2 Δ w s1 s2 statA sv1 sv2 statO)
∨
(¬ isSecV sv1 ∧ ¬ isSecV sv2 ∧ Van.eqAct sv1 sv2 ∧ move_12 Δ w s1 s2 statA sv1 sv2 statO)"
lemmas proact_defs = proact_def move_1_def move_2_def move_12_def
lemma move_1_mono:
"Δ ≤ Δ' ⟹ move_1 Δ meas s1 s2 statA sv1 sv2 statO ⟹ move_1 Δ' meas s1 s2 statA sv1 sv2 statO"
unfolding le_fun_def move_1_def by auto
lemma move_2_mono:
"Δ ≤ Δ' ⟹ move_2 Δ meas s1 s2 statA sv1 sv2 statO ⟹ move_2 Δ' meas s1 s2 statA sv1 sv2 statO"
unfolding le_fun_def move_2_def by auto
lemma move_12_mono:
"Δ ≤ Δ' ⟹ move_12 Δ meas s1 s2 statA sv1 sv2 statO ⟹ move_12 Δ' meas s1 s2 statA sv1 sv2 statO"
unfolding le_fun_def move_12_def by fastforce
lemma proact_mono:
assumes "Δ ≤ Δ'"
shows "proact Δ meas s1 s2 statA sv1 sv2 statO ⟹ proact Δ' meas s1 s2 statA sv1 sv2 statO"
unfolding proact_def using move_1_mono[OF assms] move_2_mono[OF assms] move_12_mono[OF assms] by auto
subsection ‹ The definition of unwinding ›
definition unwindCond ::
"(enat ⇒ 'stateO ⇒ 'stateO ⇒ status ⇒ 'stateV ⇒ 'stateV ⇒ status ⇒ bool) ⇒ bool"
where
"unwindCond Δ ≡ ∀w s1 s2 statA sv1 sv2 statO.
reachO s1 ∧ reachO s2 ∧ reachV sv1 ∧ reachV sv2 ∧
Δ w s1 s2 statA sv1 sv2 statO
⟶
(finalO s1 ⟷ finalO s2) ∧ (finalV sv1 ⟷ finalO s1) ∧ (finalV sv2 ⟷ finalO s2)
∧
(statA = Eq ⟶ (isIntO s1 ⟷ isIntO s2))
∧
((∃v < w. proact Δ v s1 s2 statA sv1 sv2 statO)
∨
match Δ s1 s2 statA sv1 sv2 statO
)"
lemma unwindCond_simpleI:
assumes
"⋀w s1 s2 statA sv1 sv2 statO.
reachO s1 ⟹ reachO s2 ⟹ reachV sv1 ⟹ reachV sv2 ⟹
Δ w s1 s2 statA sv1 sv2 statO
⟹
(finalO s1 ⟷ finalO s2) ∧ (finalV sv1 ⟷ finalO s1) ∧ (finalV sv2 ⟷ finalO s2)"
and
"⋀w s1 s2 statA sv1 sv2 statO.
reachO s1 ⟹ reachO s2 ⟹ reachV sv1 ⟹ reachV sv2 ⟹
Δ w s1 s2 statA sv1 sv2 statO ⟹ statA = Eq
⟹
isIntO s1 ⟷ isIntO s2"
and
"⋀w s1 s2 statA sv1 sv2 statO.
reachO s1 ⟹ reachO s2 ⟹ reachV sv1 ⟹ reachV sv2 ⟹
Δ w s1 s2 statA sv1 sv2 statO
⟹
match Δ s1 s2 statA sv1 sv2 statO"
shows "unwindCond Δ"
using assms unfolding unwindCond_def by auto
subsection ‹ The soundness of unwinding ›
definition "ψ s1 tr1 s2 tr2 statO sv1 trv1 sv2 trv2 ≡
trv1 ≠ [] ∧ trv2 ≠ [] ∧
Van.validFromS sv1 trv1 ∧
Van.validFromS sv2 trv2 ∧
(finalV (lastt sv1 trv1) ⟷ finalO (lastt s1 tr1)) ∧ (finalV (lastt sv2 trv2) ⟷ finalO (lastt s2 tr2)) ∧
Van.S trv1 = Opt.S tr1 ∧ Van.S trv2 = Opt.S tr2 ∧
Van.A trv1 = Van.A trv2 ∧
(statO = Eq ∧ Opt.O tr1 ≠ Opt.O tr2 ⟶ Van.O trv1 ≠ Van.O trv2)"
lemma ψ_completedFrom: "completedFromO s1 tr1 ⟹ completedFromO s2 tr2 ⟹
ψ s1 tr1 s2 tr2 statO sv1 trv1 sv2 trv2
⟹ completedFromV sv1 trv1 ∧ completedFromV sv2 trv2"
unfolding ψ_def Opt.completedFrom_def Van.completedFrom_def lastt_def
by presburger
lemma completedFromO_lastt: "completedFromO s1 tr1 ⟹ finalO (lastt s1 tr1)"
unfolding Opt.completedFrom_def lastt_def by auto
lemma rsecure_strong:
assumes
"⋀s1 tr1 s2 tr2.
istateO s1 ∧ Opt.validFromS s1 tr1 ∧ completedFromO s1 tr1 ∧
istateO s2 ∧ Opt.validFromS s2 tr2 ∧ completedFromO s2 tr2 ∧
Opt.A tr1 = Opt.A tr2 ∧ (isIntO s1 ∧ isIntO s2 ⟶ getActO s1 = getActO s2)
⟹
∃sv1 trv1 sv2 trv2.
istateV sv1 ∧ istateV sv2 ∧ corrState sv1 s1 ∧ corrState sv2 s2 ∧
ψ s1 tr1 s2 tr2 Eq sv1 trv1 sv2 trv2"
shows rsecure
unfolding rsecure_def3 apply clarify
subgoal for s1 tr1 s2 tr2
using assms[of s1 tr1 s2 tr2]
using ψ_completedFrom ψ_def completedFromO_lastt by (metis (full_types))
.
proposition unwindCond_ex_ψ:
assumes unwind: "unwindCond Δ"
and Δ: "Δ w s1 s2 statA sv1 sv2 statO" and stat: "(statA = Diff ⟶ statO = Diff)"
and v: "Opt.validFromS s1 tr1" "Opt.completedFrom s1 tr1" "Opt.validFromS s2 tr2" "Opt.completedFrom s2 tr2"
and tr14: "Opt.A tr1 = Opt.A tr2"
and r: "reachO s1" "reachO s2" "reachV sv1" "reachV sv2"
shows "∃trv1 trv2. ψ s1 tr1 s2 tr2 statO sv1 trv1 sv2 trv2"
using assms(2-)
proof(induction "length tr1 + length tr2" w
arbitrary: s1 s2 statA sv1 sv2 statO tr1 tr2 rule: less2_induct')
case (less w tr1 tr2 s1 s2 statA sv1 sv2 statO)
note ok = `statA = Diff ⟶ statO = Diff`
note Δ = `Δ w s1 s2 statA sv1 sv2 statO`
note A34 = `Opt.A tr1 = Opt.A tr2`
note r34 = less.prems(8,9) note r12 = less.prems(10,11)
note r = r34 r12
note r3 = r34(1) note r4 = r34(2) note r1 = r12(1) note r2 = r12(2)
have i34: "statA = Eq ⟶ isIntO s1 = isIntO s2"
and f34: "finalO s1 = finalO s2 ∧ finalV sv1 = finalO s1 ∧ finalV sv2 = finalO s2"
using Δ unwind[unfolded unwindCond_def] r by auto
have proact_match: "(∃v<w. proact Δ v s1 s2 statA sv1 sv2 statO) ∨ match Δ s1 s2 statA sv1 sv2 statO"
using Δ unwind[unfolded unwindCond_def] r by auto
show ?case using proact_match proof safe
fix v assume v: "v < w"
assume "proact Δ v s1 s2 statA sv1 sv2 statO"
thus ?thesis unfolding proact_def proof safe
assume sv1: "¬ isSecV sv1" "¬ isIntV sv1" and "move_1 Δ v s1 s2 statA sv1 sv2 statO"
then obtain sv1'
where 0: "validTransV (sv1,sv1')"
and Δ: "Δ v s1 s2 statA sv1' sv2 statO"
unfolding move_1_def by auto
have r1': "reachV sv1'" using r1 0 by (metis Van.reach.Step fst_conv snd_conv)
obtain trv1 trv2 where ψ: "ψ s1 tr1 s2 tr2 statO sv1' trv1 sv2 trv2"
using less(2)[OF v, of tr1 tr2 s1 s2 statA sv1' sv2 statO, simplified, OF Δ ok _ _ _ _ _ r34 r1' r2]
using A34 less.prems(3-6) by blast
show ?thesis apply(rule exI[of _ "sv1 # trv1"]) apply(rule exI[of _ trv2])
using ψ ok 0 sv1 unfolding ψ_def Van.completedFrom_def by auto
next
assume sv2: "¬ isSecV sv2" "¬ isIntV sv2" and "move_2 Δ v s1 s2 statA sv1 sv2 statO"
then obtain sv2'
where 0: "validTransV (sv2,sv2')"
and Δ: "Δ v s1 s2 statA sv1 sv2' statO"
unfolding move_2_def by auto
have r2': "reachV sv2'" using r2 0 by (metis Van.reach.Step fst_conv snd_conv)
obtain trv1 trv2 where ψ: "ψ s1 tr1 s2 tr2 statO sv1 trv1 sv2' trv2"
using less(2)[OF v, of tr1 tr2 s1 s2 statA sv1 sv2' statO, simplified, OF Δ ok _ _ _ _ _ r34 r1 r2']
using A34 less.prems(3-6) by blast
show ?thesis apply(rule exI[of _ trv1]) apply(rule exI[of _ "sv2 # trv2"])
using ψ ok 0 sv2 unfolding ψ_def Van.completedFrom_def by auto
next
assume sv12: "¬ isSecV sv1" "¬ isSecV sv2" "Van.eqAct sv1 sv2"
and "move_12 Δ v s1 s2 statA sv1 sv2 statO"
then obtain sv1' sv2' statO'
where 0: "statO' = sstatO' statO sv1 sv2"
"validTransV (sv1,sv1') " "¬ isSecV sv1"
"validTransV (sv2,sv2')" "¬ isSecV sv2"
"Van.eqAct sv1 sv2"
and Δ: "Δ v s1 s2 statA sv1' sv2' statO'"
unfolding move_12_def by auto
have r12': "reachV sv1'" "reachV sv2'" using r1 r2 0 by (metis Van.reach.Step fst_conv snd_conv)+
have ok': "statA = Diff ⟶ statO' = Diff" using ok 0 unfolding sstatO'_def by (cases statO, auto)
obtain trv1 trv2 where ψ: "ψ s1 tr1 s2 tr2 statO' sv1' trv1 sv2' trv2"
using less(2)[OF v, of tr1 tr2 s1 s2 statA sv1' sv2' statO', simplified, OF Δ ok' _ _ _ _ _ r34 r12']
using A34 less.prems(3-6) by blast
show ?thesis apply(rule exI[of _ "sv1 # trv1"]) apply(rule exI[of _ "sv2 # trv2"])
using ψ ok' 0 sv12 unfolding ψ_def sstatO'_def Van.completedFrom_def
using Van.A.Cons_unfold Van.eqAct_def completedFromO_lastt less.prems(4)
less.prems(6) by auto
qed
next
assume m: "match Δ s1 s2 statA sv1 sv2 statO"
show ?thesis
proof(cases "length tr1 ≤ Suc 0")
case True note tr1 = True
hence "tr1 = [] ∨ tr1 = [s1]"
by (metis Opt.validFromS_Cons_iff le_0_eq le_SucE length_0_conv length_Suc_conv less.prems(3))
hence "finalO s1" using less(3-6)
using Opt.completed_Cons Opt.completed_Nil by blast
hence f4: "finalO s2" using f34 by blast
hence tr2: "tr2 = [] ∨ tr2 = [s2]"
by (metis Opt.final_def Simple_Transition_System.validFromS_Cons_iff less.prems(5) neq_Nil_conv)
show ?thesis apply(rule exI[of _ "[sv1]"], rule exI[of _ "[sv2]"]) using tr1 tr2
using f4 f34
using completedFromO_lastt less.prems(4)
by (auto simp add: lastt_def ψ_def)
next
case False
then obtain s13 tr1' where tr1: "tr1 = s13 # tr1'" and tr1'NE: "tr1' ≠ []"
by (cases tr1, auto)
have s13[simp]: "s13 = s1" using `Opt.validFromS s1 tr1`
by (simp add: Opt.validFromS_Cons_iff tr1)
obtain s1' where
trn3: "validTransO (s1,s1')" and
tr1': "Opt.validFromS s1' tr1'" using `Opt.validFromS s1 tr1`
unfolding tr1 s13 by (metis tr1'NE Simple_Transition_System.validFromS_Cons_iff)
have r3': "reachO s1'" using r3 trn3 by (metis Opt.reach.Step fst_conv snd_conv)
have f3: "¬ finalO s1" using Opt.final_def trn3 by blast
hence f4: "¬ finalO s2" using f34 by blast
hence tr2: "¬ length tr2 ≤ Suc 0"
by (metis (no_types, opaque_lifting) Opt.completed_Cons Opt.completed_Nil
Simple_Transition_System.validFromS_Cons_iff Suc_n_not_le_n bot_nat_0.extremum le_Suc_eq length_Cons less.prems(5) less.prems(6) list.exhaust order_antisym_conv)
then obtain s24 tr2' where tr2: "tr2 = s24 # tr2'" and tr2'NE: "tr2' ≠ []"
by (cases tr2, auto)
have s24[simp]: "s24 = s2" using `Opt.validFromS s2 tr2`
by (simp add: Opt.validFromS_Cons_iff tr2)
obtain s2' where
trn4: "validTransO (s2,s2') ∨ (s2 = s2' ∧ tr2' = [])" and
tr2': "Opt.validFromS s2' tr2'" using `Opt.validFromS s2 tr2`
unfolding tr2 s24 using Opt.validFromS_Cons_iff by auto
have r34': "reachO s1'" "reachO s2'"
using r3 trn3 r4 trn4 by (metis Opt.reach.Step fst_conv snd_conv)+
note r3' = r34'(1) note r4' = r34'(2)
define statA' where statA': "statA' = sstatA' statA s1 s2"
have "¬ isIntO s1 ∨ ¬ isIntO s2 ∨ (isIntO s1 ∧ isIntO s2)"
by auto
thus ?thesis
proof safe
assume isAO3: "¬ isIntO s1"
have O33': "Opt.O tr1 = Opt.O tr1'" "Opt.A tr1 = Opt.A tr1'"
using isAO3 unfolding tr1 by auto
have A34': "Opt.A tr1' = Opt.A tr2"
using A34 O33'(2) by auto
have m: "match1 Δ s1 s2 statA sv1 sv2 statO" using m unfolding match_def by auto
have "(¬ isSecO s1 ∧ Δ ∞ s1' s2 statA sv1 sv2 statO) ∨
(eqSec sv1 s1 ∧ ¬ isIntV sv1 ∧ match1_1 Δ s1 s1' s2 statA sv1 sv2 statO) ∨
(eqSec sv1 s1 ∧ ¬ isSecV sv2 ∧ Van.eqAct sv1 sv2 ∧ match1_12 Δ s1 s1' s2 statA sv1 sv2 statO)"
using m isAO3 trn3 ok unfolding match1_def by auto
thus ?thesis
proof safe
assume "¬ isSecO s1" and Δ: "Δ ∞ s1' s2 statA sv1 sv2 statO"
hence S3: "Opt.S tr1' = Opt.S tr1" unfolding tr1 by auto
obtain trv1 trv2 where ψ: "ψ s1 tr1' s2 tr2 statO sv1 trv1 sv2 trv2"
using less(1)[of tr1' tr2, OF _ Δ _ _ _ _ _ _ r3' r4 r12, unfolded O33', simplified]
using less.prems tr1' ok A34' f3 f4 unfolding tr1 Opt.completedFrom_def
by (auto split: if_splits simp: ψ_def lastt_def)
show ?thesis apply(rule exI[of _ trv1]) apply(rule exI[of _ trv2])
using ψ O33' S3 unfolding ψ_def
using completedFromO_lastt less.prems(4)
by (auto simp add: tr1 tr1'NE)
next
assume trn13: "eqSec sv1 s1" and
Atrn1: "¬ isIntV sv1" and "match1_1 Δ s1 s1' s2 statA sv1 sv2 statO"
then obtain sv1' where
trn1: "validTransV (sv1,sv1') " and
Δ: "Δ ∞ s1' s2 statA sv1' sv2 statO"
unfolding match1_1_def by auto
have r1': "reachV sv1'"using r1 trn1 by (metis Van.reach.Step fst_conv snd_conv)
obtain trv1 trv2 where ψ: "ψ s1 tr1' s2 tr2 statO sv1' trv1 sv2 trv2"
using less(1)[of tr1' tr2, OF _ Δ _ _ _ _ _ _ r3' r4 r1' r2, unfolded O33', simplified]
using less.prems tr1' ok A34' f3 f4 unfolding tr1 tr2 Opt.completedFrom_def
by (auto simp: ψ_def lastt_def split: if_splits)
show ?thesis apply(rule exI[of _ "sv1 # trv1"]) apply(rule exI[of _ trv2])
using ψ O33' unfolding tr1 tr2 Van.completedFrom_def
using Van.validFromS_Cons trn1 tr1'NE tr2'NE
using isAO3 ok Atrn1 eqSec_S_Cons trn13
unfolding ψ_def using completedFromO_lastt less.prems(4) tr1 by auto
next
assume sv2: "¬ isSecV sv2" and trn13: "eqSec sv1 s1" and
Atrn12: "Van.eqAct sv1 sv2" and "match1_12 Δ s1 s1' s2 statA sv1 sv2 statO"
then obtain sv1' sv2' statO' where
statO': "statO' = sstatO' statO sv1 sv2" and
trn1: "validTransV (sv1,sv1') " and
trn2: "validTransV (sv2,sv2')" and
Δ: "Δ ∞ s1' s2 statA sv1' sv2' statO'"
unfolding match1_12_def by auto
have r12': "reachV sv1'" "reachV sv2'"
using r1 trn1 r2 trn2 by (metis Van.reach.Step fst_conv snd_conv)+
obtain trv1 trv2 where ψ: "ψ s1' tr1' s2 tr2 statO' sv1' trv1 sv2' trv2"
using less(1)[of tr1' tr2, OF _ Δ _ _ _ _ _ _ r3' r4 r12', unfolded O33', simplified]
using less.prems tr1' ok A34' f3 f4 unfolding tr1 tr2 Opt.completedFrom_def statO' sstatO'_def
by auto presburger+
show ?thesis apply(rule exI[of _ "sv1 # trv1"]) apply(rule exI[of _ "sv2 # trv2"])
using ψ O33' tr1'NE tr2'NE sv2
using Van.validFromS_Cons trn1 trn2
using isAO3 ok Atrn12 eqSec_S_Cons trn13 f3 f34 s13
unfolding ψ_def tr1 Van.completedFrom_def Van.eqAct_def statO' sstatO'_def
using Van.A.Cons_unfold tr1' trn3 by auto
qed
next
assume isAO4: "¬ isIntO s2"
have O44': "Opt.O tr2 = Opt.O tr2'" "Opt.A tr2 = Opt.A tr2'"
using isAO4 unfolding tr2 by auto
have A34': "Opt.A tr1 = Opt.A tr2'"
using A34 O44'(2) by auto
have m: "match2 Δ s1 s2 statA sv1 sv2 statO" using m unfolding match_def by auto
have "(¬ isSecO s2 ∧ Δ ∞ s1 s2' statA sv1 sv2 statO) ∨
(eqSec sv2 s2 ∧ ¬ isIntV sv2 ∧ match2_1 Δ s1 s2 s2' statA sv1 sv2 statO) ∨
(¬ isSecV sv1 ∧ eqSec sv2 s2 ∧ Van.eqAct sv1 sv2 ∧ match2_12 Δ s1 s2 s2' statA sv1 sv2 statO)"
using m isAO4 trn4 ok tr2'NE unfolding match2_def by auto
thus ?thesis
proof safe
assume "¬ isSecO s2" and Δ: "Δ ∞ s1 s2' statA sv1 sv2 statO"
hence S4: "Opt.S tr2' = Opt.S tr2" unfolding tr2 by auto
obtain trv1 trv2 where ψ: "ψ s1 tr1 s2' tr2' statO sv1 trv1 sv2 trv2"
using less(1)[of tr1 tr2', OF _ Δ _ _ _ _ _ _ r3 r4', simplified]
using less.prems tr2' ok A34' tr1'NE tr2'NE unfolding tr1 tr2 Opt.completedFrom_def by (cases "isIntO s2", auto)
show ?thesis apply(rule exI[of _ trv1]) apply(rule exI[of _ trv2])
using ψ O44' S4 unfolding ψ_def
using completedFromO_lastt less.prems(6)
unfolding Opt.completedFrom_def using tr2 tr2'NE by auto
next
assume trn24: "eqSec sv2 s2" and
Atrn2: "¬ isIntV sv2" and "match2_1 Δ s1 s2 s2' statA sv1 sv2 statO"
then obtain sv2' where trn2: "validTransV (sv2,sv2')" and
Δ: "Δ ∞ s1 s2' statA sv1 sv2' statO"
unfolding match2_1_def by auto
have r2': "reachV sv2'" using r2 trn2 by (metis Van.reach.Step fst_conv snd_conv)
obtain trv1 trv2 where ψ: "ψ s1 tr1 s2' tr2' statO sv1 trv1 sv2' trv2"
using less(1)[of tr1 tr2', OF _ Δ _ _ _ _ _ _ r3 r4' r1 r2', simplified]
using less.prems tr2' ok A34' tr1'NE tr2'NE unfolding tr1 tr2 Opt.completedFrom_def by (cases "isIntO s2", auto)
show ?thesis apply(rule exI[of _ trv1]) apply(rule exI[of _ "sv2 # trv2"])
using ψ tr1'NE tr2'NE
using Van.validFromS_Cons trn2
using isAO4 ok Atrn2 eqSec_S_Cons trn24
unfolding ψ_def tr1 tr2 s13 s24 Van.completedFrom_def lastt_def by auto
next
assume sv1: "¬ isSecV sv1" and trn24: "eqSec sv2 s2" and
Atrn12: "Van.eqAct sv1 sv2" and "match2_12 Δ s1 s2 s2' statA sv1 sv2 statO"
then obtain sv1' sv2' statO' where
statO': "statO' = sstatO' statO sv1 sv2" and
trn1: "validTransV (sv1,sv1')" and
trn2: "validTransV (sv2,sv2')" and
Δ: "Δ ∞ s1 s2' statA sv1' sv2' statO'"
unfolding match2_12_def by auto
have r12': "reachV sv1'" "reachV sv2'"
using r1 trn1 r2 trn2 by (metis Van.reach.Step fst_conv snd_conv)+
obtain trv1 trv2 where ψ: "ψ s1 tr1 s2' tr2' statO' sv1' trv1 sv2' trv2"
using less(1)[of tr1 tr2', OF _ Δ _ _ _ _ _ _ r3 r4' r12', simplified]
using less.prems tr2' ok A34' tr1'NE tr2'NE unfolding tr1 tr2 Opt.completedFrom_def statO' sstatO'_def
by (cases "isIntO s2", auto)
show ?thesis apply(rule exI[of _ "sv1 # trv1"]) apply(rule exI[of _ "sv2 # trv2"])
using ψ O44' tr1'NE tr2'NE sv1
using Van.validFromS_Cons trn1 trn2
using isAO4 ok Atrn12 eqSec_S_Cons trn24
unfolding ψ_def tr2 tr1'NE Van.completedFrom_def Van.eqAct_def
statO' sstatO'_def
using Van.A.Cons_unfold tr2' trn4 by auto
qed
next
assume isAO34: "isIntO s1" "isIntO s2"
have A34': "getActO s1 = getActO s2" "Opt.A tr1' = Opt.A tr2'"
using A34 isAO34 tr1'NE tr2'NE unfolding tr1 tr2 by auto
have O33': "Opt.O tr1 = getObsO s1 # Opt.O tr1'" and
O44': "Opt.O tr2 = getObsO s2 # Opt.O tr2'"
using isAO34 tr1'NE tr2'NE unfolding tr1 s13 tr2 s24 by auto
have m: "match12 Δ s1 s2 statA sv1 sv2 statO" using m unfolding statA' match_def by auto
have trn34: "getObsO s1 = getObsO s2 ∨ statA' = Diff"
using isAO34 unfolding statA' sstatA'_def by (cases statA,auto)
have "(¬ isSecO s1 ∧ ¬ isSecO s2 ∧ (statA = statA' ∨ statO = Diff) ∧ Δ ∞ s1' s2' statA' sv1 sv2 statO)
∨
(¬ isSecO s2 ∧ eqSec sv1 s1 ∧ ¬ isIntV sv1 ∧
(statA = statA' ∨ statO = Diff) ∧
match12_1 Δ s1' s2' statA' sv1 sv2 statO)
∨
(¬ isSecO s1 ∧ eqSec sv2 s2 ∧ ¬ isIntV sv2 ∧
(statA = statA' ∨ statO = Diff) ∧
match12_2 Δ s1' s2' statA' sv1 sv2 statO)
∨
(eqSec sv1 s1 ∧ eqSec sv2 s2 ∧ Van.eqAct sv1 sv2 ∧
match12_12 Δ s1' s2' statA' sv1 sv2 statO)"
(is "?K1 ∨ ?K2 ∨ ?K3 ∨ ?K4")
using m[unfolded match12_def, rule_format, of s1' s2']
isAO34 A34' trn3 trn4 tr1'NE tr2'NE
unfolding s13 s24 trn34 statA' Opt.eqAct_def sstatA'_def by auto
thus ?thesis proof (elim disjE)
assume K1: "?K1" hence Δ: "Δ ∞ s1' s2' statA' sv1 sv2 statO" by simp
have ok': "(statA' = Diff ⟶ statO = Diff)"
using ok K1 unfolding statA' using isAO34 by auto
obtain trv1 trv2 where ψ: "ψ s1' tr1' s2' tr2' statO sv1 trv1 sv2 trv2"
using less(1)[of tr1' tr2', OF _ Δ _ _ _ _ _ _ r34' r12, simplified]
using less.prems tr1' tr2' ok' A34' isAO34 tr1'NE tr2'NE unfolding tr1 tr2 Opt.completedFrom_def by auto
show ?thesis apply(rule exI[of _ trv1]) apply(rule exI[of _ trv2])
using ψ trn34 O33' O44' K1 ok unfolding ψ_def tr1 tr2
using completedFromO_lastt less.prems(4,6)
unfolding Opt.completedFrom_def using tr1 tr2 tr1'NE tr2'NE by auto
next
assume K2: "?K2"
then obtain sv1' where
trn1: "validTransV (sv1,sv1') " and
trn13: "eqSec sv1 s1" and
Atrn1: "¬ isIntV sv1" and ok': "(statA' = statA ∨ statO = Diff)" and
Δ: "Δ ∞ s1' s2' statA' sv1' sv2 statO"
unfolding match12_1_def by auto
have r1': "reachV sv1'" using r1 trn1 by (metis Van.reach.Step fst_conv snd_conv)
obtain trv1 trv2 where ψ: "ψ s1' tr1' s2' tr2' statO sv1' trv1 sv2 trv2"
using less(1)[of tr1' tr2', OF _ Δ _ _ _ _ _ _ r34' r1' r2, simplified]
using less.prems tr1' tr2' ok' A34' tr1'NE tr2'NE unfolding tr1 tr2 Opt.completedFrom_def by auto
show ?thesis apply(rule exI[of _ "sv1 # trv1"]) apply(rule exI[of _ trv2])
using ψ O33' O44' tr1'NE tr2'NE unfolding tr1 tr2
using Van.validFromS_Cons trn1 ok
using K2 ok' Atrn1 eqSec_S_Cons trn13 trn34
unfolding statA' Van.completedFrom_def eqSec_def
using s13 tr1 tr1' tr2' trn3 trn4
by simp (smt (verit, ccfv_SIG) Opt.S.simps(2) Simple_Transition_System.lastt_Cons
Van.A.Cons_unfold Van.O.Cons_unfold ψ_def list.simps(3) status.simps(1))
next
assume K3: "?K3"
then obtain sv2' where
trn2: "validTransV (sv2,sv2')" and
trn24: "eqSec sv2 s2" and
Atrn2: "¬ isIntV sv2" and ok': "(statA' = statA ∨ statO = Diff)" and
Δ: "Δ ∞ s1' s2' statA' sv1 sv2' statO"
unfolding match12_2_def by auto
have r2': "reachV sv2'" using r2 trn2 by (metis Van.reach.Step fst_conv snd_conv)
obtain trv1 trv2 where ψ: "ψ s1' tr1' s2' tr2' statO sv1 trv1 sv2' trv2"
using less(1)[of tr1' tr2', OF _ Δ _ _ _ _ _ _ r34' r1 r2', simplified]
using less.prems tr1' tr2' ok' A34' tr1'NE tr2'NE unfolding tr1 tr2 Opt.completedFrom_def by auto
show ?thesis apply(rule exI[of _ trv1]) apply(rule exI[of _ "sv2 # trv2"])
using ψ O33' O44' tr1'NE tr2'NE unfolding ψ_def tr1 tr2
using Van.validFromS_Cons trn2 ok
using K3 ok' Atrn2 eqSec_S_Cons trn24 trn34
unfolding statA' Van.completedFrom_def
by simp (metis last.simps lastt_def list.simps(3) status.distinct(2))
next
assume K4: "?K4"
then obtain sv1' sv2' statO' where 0:
"statO' = sstatO' statO sv1 sv2"
"validTransV (sv1,sv1') "
"eqSec sv1 s1"
"validTransV (sv2,sv2')"
"eqSec sv2 s2"
"Van.eqAct sv1 sv2"
and ok': "statA' = Diff ⟶ statO' = Diff" and Δ: "Δ ∞ s1' s2' statA' sv1' sv2' statO'"
unfolding match12_12_def by auto
have r12': "reachV sv1'" "reachV sv2'" using r1 r2 0
by (metis Van.reach.Step fst_conv snd_conv)+
obtain trv1 trv2 where ψ: "ψ s1' tr1' s2' tr2' statO' sv1' trv1 sv2' trv2"
using less(1)[of tr1' tr2', OF _ Δ _ _ _ _ _ _ r34' r12', simplified]
using less.prems tr1' tr2' ok' A34' tr1'NE tr2'NE unfolding tr1 tr2 Opt.completedFrom_def by auto
show ?thesis apply(rule exI[of _ "sv1 # trv1"]) apply(rule exI[of _ "sv2 # trv2"])
using trn34
using ψ O33' O44' isAO34 tr1'NE tr2'NE unfolding ψ_def tr1 tr2
using Van.validFromS_Cons 0
using K4 eqSec_S_Cons
unfolding statA' Van.eqAct_def Van.completedFrom_def match12_12_def sstatO'_def
by (smt (z3) Simple_Transition_System.lastt_Cons Van.A.Cons_unfold Van.O.Cons_unfold
completedFromO_lastt f3 f34 lastt_Nil less.prems(4) less.prems(6) list.inject s13
s24 status.simps(1) tr1 tr1' tr2 tr2' trn3 trn4 updStat.simps(1) updStat.simps(3))
qed
qed
qed
qed
qed
theorem unwind_rsecure:
assumes init: "initCond Δ"
and unwind: "unwindCond Δ"
shows rsecure
apply (rule rsecure_strong)
apply (elim conjE)
subgoal for s1 tr1 s2 tr2
using init unfolding initCond_def
apply (erule_tac allE[of _ s1])
apply (elim allE[of _ s2] conjE)
apply (elim impE[of ‹istateO s1 ∧ istateO s2›] exE conjE)
subgoal by clarify
subgoal for sv1 sv2
using unwind apply (drule_tac unwindCond_ex_ψ, blast+)
subgoal by (rule Transition_System.reach.Istate)
subgoal by (rule Transition_System.reach.Istate)
subgoal by (rule Transition_System.reach.Istate)
subgoal by (rule Transition_System.reach.Istate)
apply (elim exE)
subgoal for trv1 trv2
apply (rule exI[of _ sv1], rule exI[of _ trv1], rule exI[of _ sv2], rule exI[of _ trv2])
by clarify
.
.
.
subsection ‹ Compositional unwinding ›
text ‹ We allow networks of unwinding relations that unwind into each other,
which offer a compositional alternative to monolithic unwinding. ›
definition unwindIntoCond ::
"(enat ⇒ 'stateO ⇒ 'stateO ⇒ status ⇒ 'stateV ⇒ 'stateV ⇒ status ⇒ bool) ⇒
(enat ⇒ 'stateO ⇒ 'stateO ⇒ status ⇒ 'stateV ⇒ 'stateV ⇒ status ⇒ bool)
⇒ bool"
where
"unwindIntoCond Δ Δ' ≡ ∀w s1 s2 statA sv1 sv2 statO.
reachO s1 ∧ reachO s2 ∧ reachV sv1 ∧ reachV sv2 ∧
Δ w s1 s2 statA sv1 sv2 statO ⟶
(finalO s1 ⟷ finalO s2) ∧ (finalV sv1 ⟷ finalO s1) ∧ (finalV sv2 ⟷ finalO s2)
∧
(statA = Eq ⟶ (isIntO s1 ⟷ isIntO s2))
∧
((∃v<w. proact Δ' v s1 s2 statA sv1 sv2 statO)
∨
match Δ' s1 s2 statA sv1 sv2 statO)"
lemma unwindIntoCond_simpleI:
assumes
"⋀w s1 s2 statA sv1 sv2 statO.
reachO s1 ⟹ reachO s2 ⟹ reachV sv1 ⟹ reachV sv2 ⟹
Δ w s1 s2 statA sv1 sv2 statO
⟹
(finalO s1 ⟷ finalO s2) ∧ (finalV sv1 ⟷ finalO s1) ∧ (finalV sv2 ⟷ finalO s2)"
and
"⋀w s1 s2 statA sv1 sv2 statO.
reachO s1 ⟹ reachO s2 ⟹ reachV sv1 ⟹ reachV sv2 ⟹
Δ w s1 s2 statA sv1 sv2 statO ⟹
statA = Eq
⟹
isIntO s1 ⟷ isIntO s2"
"⋀w s1 s2 statA sv1 sv2 statO.
reachO s1 ⟹ reachO s2 ⟹ reachV sv1 ⟹ reachV sv2 ⟹
Δ w s1 s2 statA sv1 sv2 statO
⟹
match Δ' s1 s2 statA sv1 sv2 statO"
shows "unwindIntoCond Δ Δ'"
using assms unfolding unwindIntoCond_def by auto
lemma unwindIntoCond_simpleI2:
assumes
"⋀w s1 s2 statA sv1 sv2 statO.
reachO s1 ⟹ reachO s2 ⟹ reachV sv1 ⟹ reachV sv2 ⟹
Δ w s1 s2 statA sv1 sv2 statO
⟹
(finalO s1 ⟷ finalO s2) ∧ (finalV sv1 ⟷ finalO s1) ∧ (finalV sv2 ⟷ finalO s2)"
and
"⋀w s1 s2 statA sv1 sv2 statO.
reachO s1 ⟹ reachO s2 ⟹ reachV sv1 ⟹ reachV sv2 ⟹
Δ w s1 s2 statA sv1 sv2 statO ⟹
statA = Eq
⟹
isIntO s1 ⟷ isIntO s2"
and
"⋀w s1 s2 statA sv1 sv2 statO.
reachO s1 ⟹ reachO s2 ⟹ reachV sv1 ⟹ reachV sv2 ⟹
Δ w s1 s2 statA sv1 sv2 statO
⟹
(∃v<w. proact Δ' v s1 s2 statA sv1 sv2 statO)"
shows "unwindIntoCond Δ Δ'"
using assms unfolding unwindIntoCond_def by auto
lemma unwindIntoCond_simpleIB:
assumes
"⋀w s1 s2 statA sv1 sv2 statO.
reachO s1 ⟹ reachO s2 ⟹ reachV sv1 ⟹ reachV sv2 ⟹
Δ w s1 s2 statA sv1 sv2 statO
⟹
(finalO s1 ⟷ finalO s2) ∧ (finalV sv1 ⟷ finalO s1) ∧ (finalV sv2 ⟷ finalO s2)"
and
"⋀w s1 s2 statA sv1 sv2 statO.
reachO s1 ⟹ reachO s2 ⟹ reachV sv1 ⟹ reachV sv2 ⟹
Δ w s1 s2 statA sv1 sv2 statO ⟹
statA = Eq
⟹
isIntO s1 ⟷ isIntO s2"
and
"⋀w s1 s2 statA sv1 sv2 statO.
reachO s1 ⟹ reachO s2 ⟹ reachV sv1 ⟹ reachV sv2 ⟹
Δ w s1 s2 statA sv1 sv2 statO
⟹
(∃v<w. proact Δ' v s1 s2 statA sv1 sv2 statO) ∨ match Δ' s1 s2 statA sv1 sv2 statO"
shows "unwindIntoCond Δ Δ'"
using assms unfolding unwindIntoCond_def by auto
theorem distrib_unwind_rsecure:
assumes m: "0 < m" and nxt: "⋀i. i < (m::nat) ⟹ nxt i ⊆ {0..<m}"
and init: "initCond (Δs 0)"
and step: "⋀i. i < m ⟹
unwindIntoCond (Δs i) (λw s1 s2 statA sv1 sv2 statO.
∃j ∈ nxt i. Δs j w s1 s2 statA sv1 sv2 statO)"
shows rsecure
proof-
define Δ where D: "Δ ≡ λw s1 s2 statA sv1 sv2 statO. ∃i < m. Δs i w s1 s2 statA sv1 sv2 statO"
have i: "initCond Δ"
using init m unfolding initCond_def D by meson
have c: "unwindCond Δ" unfolding unwindCond_def apply(intro allI impI allI)
apply(subst (asm) D) apply (elim exE conjE)
subgoal for w s1 s2 statA sv1 sv2 statO i
apply(frule step) unfolding unwindIntoCond_def
apply(erule allE[of _ w])
apply(erule allE[of _ s1]) apply(erule allE[of _ s2]) apply(erule allE[of _ statA])
apply(erule allE[of _ sv1]) apply(erule allE[of _ sv2]) apply(erule allE[of _ statO])
apply simp apply(elim conjE)
apply(erule disjE)
subgoal apply(rule disjI1)
subgoal apply(elim exE conjE) subgoal for v
apply(rule exI[of _ v], simp)
apply(rule proact_mono[of "λw s1 s2 statA sv1 sv2 statO. ∃j∈nxt i. Δs j w s1 s2 statA sv1 sv2 statO"])
subgoal unfolding le_fun_def D by simp (meson atLeastLessThan_iff nxt subsetD)
subgoal . . . .
subgoal apply(rule disjI2)
apply(rule match_mono[of "λw s1 s2 statA sv1 sv2 statO. ∃j∈nxt i. Δs j w s1 s2 statA sv1 sv2 statO"])
subgoal unfolding le_fun_def D by simp (meson atLeastLessThan_iff nxt subsetD)
subgoal . . . .
show ?thesis using unwind_rsecure[OF i c] .
qed
corollary linear_unwind_rsecure:
assumes init: "initCond (Δs 0)"
and step: "(⋀i. i < m ⟹
unwindIntoCond (Δs i) (λw s1 s2 statA sv1 sv2 statO.
Δs i w s1 s2 statA sv1 sv2 statO ∨
Δs (Suc i) w s1 s2 statA sv1 sv2 statO))"
and finish: "unwindIntoCond (Δs m) (Δs m)"
shows rsecure
apply(rule distrib_unwind_rsecure[of "Suc m" "λi. if i<m then {i,Suc i} else {i}" Δs, OF _ _ init])
using step finish
by (auto simp: less_Suc_eq_le)
definition oor where
"oor Δ Δ⇩2 ≡ λw s1 s2 statA sv1 sv2 statO.
Δ w s1 s2 statA sv1 sv2 statO ∨ Δ⇩2 w s1 s2 statA sv1 sv2 statO"
lemma oorI1:
"Δ w s1 s2 statA sv1 sv2 statO ⟹ oor Δ Δ⇩2 w s1 s2 statA sv1 sv2 statO"
unfolding oor_def by simp
lemma oorI2:
"Δ⇩2 w s1 s2 statA sv1 sv2 statO ⟹ oor Δ Δ⇩2 w s1 s2 statA sv1 sv2 statO"
unfolding oor_def by simp
definition oor3 where
"oor3 Δ Δ⇩2 Δ⇩3 ≡ λw s1 s2 statA sv1 sv2 statO.
Δ w s1 s2 statA sv1 sv2 statO ∨ Δ⇩2 w s1 s2 statA sv1 sv2 statO ∨
Δ⇩3 w s1 s2 statA sv1 sv2 statO"
lemma oor3I1:
"Δ w s1 s2 statA sv1 sv2 statO ⟹ oor3 Δ Δ⇩2 Δ⇩3 w s1 s2 statA sv1 sv2 statO"
unfolding oor3_def by simp
lemma oor3I2:
"Δ⇩2 w s1 s2 statA sv1 sv2 statO ⟹ oor3 Δ Δ⇩2 Δ⇩3 w s1 s2 statA sv1 sv2 statO"
unfolding oor3_def by simp
lemma oor3I3:
"Δ⇩3 w s1 s2 statA sv1 sv2 statO ⟹ oor3 Δ Δ⇩2 Δ⇩3 w s1 s2 statA sv1 sv2 statO"
unfolding oor3_def by simp
definition oor4 where
"oor4 Δ Δ⇩2 Δ⇩3 Δ⇩4 ≡ λw s1 s2 statA sv1 sv2 statO.
Δ w s1 s2 statA sv1 sv2 statO ∨ Δ⇩2 w s1 s2 statA sv1 sv2 statO ∨
Δ⇩3 w s1 s2 statA sv1 sv2 statO ∨ Δ⇩4 w s1 s2 statA sv1 sv2 statO"
lemma oor4I1:
"Δ w s1 s2 statA sv1 sv2 statO ⟹ oor4 Δ Δ⇩2 Δ⇩3 Δ⇩4 w s1 s2 statA sv1 sv2 statO"
unfolding oor4_def by simp
lemma oor4I2:
"Δ⇩2 w s1 s2 statA sv1 sv2 statO ⟹ oor4 Δ Δ⇩2 Δ⇩3 Δ⇩4 w s1 s2 statA sv1 sv2 statO"
unfolding oor4_def by simp
lemma oor4I3:
"Δ⇩3 w s1 s2 statA sv1 sv2 statO ⟹ oor4 Δ Δ⇩2 Δ⇩3 Δ⇩4 w s1 s2 statA sv1 sv2 statO"
unfolding oor4_def by simp
lemma oor4I4:
"Δ⇩4 w s1 s2 statA sv1 sv2 statO ⟹ oor4 Δ Δ⇩2 Δ⇩3 Δ⇩4 w s1 s2 statA sv1 sv2 statO"
unfolding oor4_def by simp
definition oor5 where
"oor5 Δ Δ⇩2 Δ⇩3 Δ⇩4 Δ⇩5 ≡ λw s1 s2 statA sv1 sv2 statO.
Δ w s1 s2 statA sv1 sv2 statO ∨ Δ⇩2 w s1 s2 statA sv1 sv2 statO ∨
Δ⇩3 w s1 s2 statA sv1 sv2 statO ∨ Δ⇩4 w s1 s2 statA sv1 sv2 statO ∨
Δ⇩5 w s1 s2 statA sv1 sv2 statO"
lemma oor5I1:
"Δ w s1 s2 statA sv1 sv2 statO ⟹ oor5 Δ Δ⇩2 Δ⇩3 Δ⇩4 Δ⇩5 w s1 s2 statA sv1 sv2 statO"
unfolding oor5_def by simp
lemma oor5I2:
"Δ⇩2 w s1 s2 statA sv1 sv2 statO ⟹ oor5 Δ Δ⇩2 Δ⇩3 Δ⇩4 Δ⇩5 w s1 s2 statA sv1 sv2 statO"
unfolding oor5_def by simp
lemma oor5I3:
"Δ⇩3 w s1 s2 statA sv1 sv2 statO ⟹ oor5 Δ Δ⇩2 Δ⇩3 Δ⇩4 Δ⇩5 w s1 s2 statA sv1 sv2 statO"
unfolding oor5_def by simp
lemma oor5I4:
"Δ⇩4 w s1 s2 statA sv1 sv2 statO ⟹ oor5 Δ Δ⇩2 Δ⇩3 Δ⇩4 Δ⇩5 w s1 s2 statA sv1 sv2 statO"
unfolding oor5_def by simp
lemma oor5I5:
"Δ⇩5 w s1 s2 statA sv1 sv2 statO ⟹ oor5 Δ Δ⇩2 Δ⇩3 Δ⇩4 Δ⇩5 w s1 s2 statA sv1 sv2 statO"
unfolding oor5_def by simp
definition oor6 where
"oor6 Δ Δ⇩2 Δ⇩3 Δ⇩4 Δ⇩5 Δ⇩6 ≡ λw s1 s2 statA sv1 sv2 statO.
Δ w s1 s2 statA sv1 sv2 statO ∨ Δ⇩2 w s1 s2 statA sv1 sv2 statO ∨
Δ⇩3 w s1 s2 statA sv1 sv2 statO ∨ Δ⇩4 w s1 s2 statA sv1 sv2 statO ∨
Δ⇩5 w s1 s2 statA sv1 sv2 statO ∨ Δ⇩6 w s1 s2 statA sv1 sv2 statO"
lemma oor6I1:
"Δ w s1 s2 statA sv1 sv2 statO ⟹ oor6 Δ Δ⇩2 Δ⇩3 Δ⇩4 Δ⇩5 Δ⇩6 w s1 s2 statA sv1 sv2 statO"
unfolding oor6_def by simp
lemma oor6I2:
"Δ⇩2 w s1 s2 statA sv1 sv2 statO ⟹ oor6 Δ Δ⇩2 Δ⇩3 Δ⇩4 Δ⇩5 Δ⇩6 w s1 s2 statA sv1 sv2 statO"
unfolding oor6_def by simp
lemma oor6I3:
"Δ⇩3 w s1 s2 statA sv1 sv2 statO ⟹ oor6 Δ Δ⇩2 Δ⇩3 Δ⇩4 Δ⇩5 Δ⇩6 w s1 s2 statA sv1 sv2 statO"
unfolding oor6_def by simp
lemma oor6I4:
"Δ⇩4 w s1 s2 statA sv1 sv2 statO ⟹ oor6 Δ Δ⇩2 Δ⇩3 Δ⇩4 Δ⇩5 Δ⇩6 w s1 s2 statA sv1 sv2 statO"
unfolding oor6_def by simp
lemma oor6I5:
"Δ⇩5 w s1 s2 statA sv1 sv2 statO ⟹ oor6 Δ Δ⇩2 Δ⇩3 Δ⇩4 Δ⇩5 Δ⇩6 w s1 s2 statA sv1 sv2 statO"
unfolding oor6_def by simp
lemma oor6I6:
"Δ⇩6 w s1 s2 statA sv1 sv2 statO ⟹ oor6 Δ Δ⇩2 Δ⇩3 Δ⇩4 Δ⇩5 Δ⇩6 w s1 s2 statA sv1 sv2 statO"
unfolding oor6_def by simp
lemma unwind_rsecure_foo:
assumes init: "initCond Δ⇩0"
and step0: "unwindIntoCond Δ⇩0 ΔNN"
and stepNN: "unwindIntoCond ΔNN (oor5 ΔNN ΔSN ΔNS ΔSS Δnonspec)"
and stepNS: "unwindIntoCond ΔNS (oor4 ΔNN ΔSN ΔNS ΔSS)"
and stepSN: "unwindIntoCond ΔSN (oor4 ΔNN ΔSN ΔNS ΔSS)"
and stepSS: "unwindIntoCond ΔSS (oor4 ΔNN ΔSN ΔNS ΔSS)"
and stepNonspec: "unwindIntoCond Δnonspec Δnonspec"
shows rsecure
proof-
define m where m: "m ≡ (6::nat)"
define Δs where Δs: "Δs ≡ λi::nat.
if i = 0 then Δ⇩0
else if i = 1 then ΔNN
else if i = 2 then ΔSN
else if i = 3 then ΔNS
else if i = 4 then ΔSS
else Δnonspec"
define nxt where nxt: "nxt ≡ λi::nat.
if i = 0 then {1::nat}
else if i = 1 then {1,2,3,4,5}
else if i = 2 then {1,2,3,4}
else if i = 3 then {1,2,3,4}
else if i = 4 then {1,2,3,4}
else {5}"
show ?thesis apply(rule distrib_unwind_rsecure[of m nxt Δs])
subgoal unfolding m by auto
subgoal unfolding nxt m by auto
subgoal using init unfolding Δs by auto
subgoal
unfolding m nxt Δs
using step0 stepNN stepNS stepSN stepSS stepNonspec
unfolding oor4_def oor5_def by auto .
qed
lemma isIntO_match1: "isIntO s1 ⟹ match1 Δ s1 s2 statA sv1 sv2 statO"
unfolding match1_def by auto
lemma isIntO_match2: "isIntO s2 ⟹ match2 Δ s1 s2 statA sv1 sv2 statO"
unfolding match2_def by auto
lemma match1_1_oorI1:
"match1_1 Δ s1 s1' s2 statA sv1 sv2 statO ⟹
match1_1 (oor Δ Δ⇩2) s1 s1' s2 statA sv1 sv2 statO"
apply(rule match1_1_mono) unfolding le_fun_def oor_def by auto
lemma match1_1_oorI2:
"match1_1 Δ⇩2 s1 s1' s2 statA sv1 sv2 statO ⟹
match1_1 (oor Δ Δ⇩2) s1 s1' s2 statA sv1 sv2 statO"
apply(rule match1_1_mono) unfolding le_fun_def oor_def by auto
lemma match1_oorI1:
"match1 Δ s1 s2 statA sv1 sv2 statO ⟹
match1 (oor Δ Δ⇩2) s1 s2 statA sv1 sv2 statO"
apply(rule match1_mono) unfolding le_fun_def oor_def by auto
lemma match1_oorI2:
"match1 Δ⇩2 s1 s2 statA sv1 sv2 statO ⟹
match1 (oor Δ Δ⇩2) s1 s2 statA sv1 sv2 statO"
apply(rule match1_mono) unfolding le_fun_def oor_def by auto
lemma match2_1_oorI1:
"match2_1 Δ s1 s2 s2' statA sv1 sv2 statO ⟹
match2_1 (oor Δ Δ⇩2) s1 s2 s2' statA sv1 sv2 statO"
apply(rule match2_1_mono) unfolding le_fun_def oor_def by auto
lemma match2_1_oorI2:
"match2_1 Δ⇩2 s1 s2 s2' statA sv1 sv2 statO ⟹
match2_1 (oor Δ Δ⇩2) s1 s2 s2' statA sv1 sv2 statO"
apply(rule match2_1_mono) unfolding le_fun_def oor_def by auto
lemma match2_oorI1:
"match2 Δ s1 s2 statA sv1 sv2 statO ⟹
match2 (oor Δ Δ⇩2) s1 s2 statA sv1 sv2 statO"
apply(rule match2_mono) unfolding le_fun_def oor_def by auto
lemma match2_oorI2:
"match2 Δ⇩2 s1 s2 statA sv1 sv2 statO ⟹
match2 (oor Δ Δ⇩2) s1 s2 statA sv1 sv2 statO"
apply(rule match2_mono) unfolding le_fun_def oor_def by auto
lemma match12_oorI1:
"match12 Δ s1 s2 statA sv1 sv2 statO ⟹
match12 (oor Δ Δ⇩2) s1 s2 statA sv1 sv2 statO"
apply(rule match12_mono) unfolding le_fun_def oor_def by auto
lemma match12_oorI2:
"match12 Δ⇩2 s1 s2 statA sv1 sv2 statO ⟹
match12 (oor Δ Δ⇩2) s1 s2 statA sv1 sv2 statO"
apply(rule match12_mono) unfolding le_fun_def oor_def by auto
lemma match12_1_oorI1:
"match12_1 Δ s1' s2' statA' sv1 sv2 statO ⟹
match12_1 (oor Δ Δ⇩2) s1' s2' statA' sv1 sv2 statO"
apply(rule match12_1_mono) unfolding le_fun_def oor_def by auto
lemma match12_1_oorI2:
"match12_1 Δ⇩2 s1' s2' statA' sv1 sv2 statO ⟹
match12_1 (oor Δ Δ⇩2) s1' s2' statA' sv1 sv2 statO"
apply(rule match12_1_mono) unfolding le_fun_def oor_def by auto
lemma match12_2_oorI1:
"match12_2 Δ s2 s2' statA' sv1 sv2 statO ⟹
match12_2 (oor Δ Δ⇩2) s2 s2' statA' sv1 sv2 statO"
apply(rule match12_2_mono) unfolding le_fun_def oor_def by auto
lemma match12_2_oorI2:
"match12_2 Δ⇩2 s2 s2' statA' sv1 sv2 statO ⟹
match12_2 (oor Δ Δ⇩2) s2 s2' statA' sv1 sv2 statO"
apply(rule match12_2_mono) unfolding le_fun_def oor_def by auto
lemma match12_12_oorI1:
"match12_12 Δ s1' s2' statA' sv1 sv2 statO ⟹
match12_12 (oor Δ Δ⇩2) s1' s2' statA' sv1 sv2 statO"
apply(rule match12_12_mono) unfolding le_fun_def oor_def by auto
lemma match12_12_oorI2:
"match12_12 Δ⇩2 s1' s2' statA' sv1 sv2 statO ⟹
match12_12 (oor Δ Δ⇩2) s1' s2' statA' sv1 sv2 statO"
apply(rule match12_12_mono) unfolding le_fun_def oor_def by auto
lemma match_oorI1:
"match Δ s1 s2 statA sv1 sv2 statO ⟹
match (oor Δ Δ⇩2) s1 s2 statA sv1 sv2 statO"
apply(rule match_mono) unfolding le_fun_def oor_def by auto
lemma match_oorI2:
"match Δ⇩2 s1 s2 statA sv1 sv2 statO ⟹
match (oor Δ Δ⇩2) s1 s2 statA sv1 sv2 statO"
apply(rule match_mono) unfolding le_fun_def oor_def by auto
lemma proact_oorI1:
"proact Δ meas s1 s2 statA sv1 sv2 statO ⟹
proact (oor Δ Δ⇩2) meas s1 s2 statA sv1 sv2 statO"
apply(rule proact_mono) unfolding le_fun_def oor_def by auto
lemma proact_oorI2:
"proact Δ⇩2 meas s1 s2 statA sv1 sv2 statO ⟹
proact (oor Δ Δ⇩2) meas s1 s2 statA sv1 sv2 statO"
apply(rule proact_mono) unfolding le_fun_def oor_def by auto
lemma move_1_oorI1:
"move_1 Δ meas s1 s2 statA sv1 sv2 statO ⟹
move_1 (oor Δ Δ⇩2) meas s1 s2 statA sv1 sv2 statO"
apply(rule move_1_mono) unfolding le_fun_def oor_def by auto
lemma move_1_oorI2:
"move_1 Δ⇩2 meas s1 s2 statA sv1 sv2 statO ⟹
move_1 (oor Δ Δ⇩2) meas s1 s2 statA sv1 sv2 statO"
apply(rule move_1_mono) unfolding le_fun_def oor_def by auto
lemma move_2_oorI1:
"move_2 Δ meas s1 s2 statA sv1 sv2 statO ⟹
move_2 (oor Δ Δ⇩2) meas s1 s2 statA sv1 sv2 statO"
apply(rule move_2_mono) unfolding le_fun_def oor_def by auto
lemma move_2_oorI2:
"move_2 Δ⇩2 meas s1 s2 statA sv1 sv2 statO ⟹
move_2 (oor Δ Δ⇩2) meas s1 s2 statA sv1 sv2 statO"
apply(rule move_2_mono) unfolding le_fun_def oor_def by auto
lemma move_12_oorI1:
"move_12 Δ meas s1 s2 statA sv1 sv2 statO ⟹
move_12 (oor Δ Δ⇩2) meas s1 s2 statA sv1 sv2 statO"
apply(rule move_12_mono) unfolding le_fun_def oor_def by auto
lemma move_12_oorI2:
"move_12 Δ⇩2 meas s1 s2 statA sv1 sv2 statO ⟹
move_12 (oor Δ Δ⇩2) meas s1 s2 statA sv1 sv2 statO"
apply(rule move_12_mono) unfolding le_fun_def oor_def by auto
end
context Relative_Security_Determ
begin
lemma match1_1_defD: "match1_1 Δ s1 s1' s2 statA sv1 sv2 statO ⟷
¬ finalV sv1 ∧ Δ ∞ s1' s2 statA (nextO sv1) sv2 statO"
unfolding match1_1_def validTrans_iff_next by simp
lemma match1_12_defD: "match1_12 Δ s1 s1' s2 statA sv1 sv2 statO ⟷
¬ finalV sv1 ∧ ¬ finalV sv2 ∧
Δ ∞ s1' s2 statA (nextO sv1) (nextO sv2) (sstatO' statO sv1 sv2)"
unfolding match1_12_def validTrans_iff_next by simp
lemmas match1_defsD = match1_def match1_1_defD match1_12_defD
lemma match2_1_defD: "match2_1 Δ s1 s2 s2' statA sv1 sv2 statO ⟷
¬ finalV sv2 ∧ Δ ∞ s1 s2' statA sv1 (nextO sv2) statO"
unfolding match2_1_def validTrans_iff_next by simp
lemma match2_12_defD: "match2_12 Δ s1 s2 s2' statA sv1 sv2 statO ⟷
¬ finalV sv1 ∧ ¬ finalV sv2 ∧ Δ ∞ s1 s2' statA (nextO sv1) (nextO sv2) (sstatO' statO sv1 sv2)"
unfolding match2_12_def validTrans_iff_next by simp
lemmas match2_defsD = match2_def match2_1_defD match2_12_defD
lemma match12_1_defD: "match12_1 Δ s1' s2' statA' sv1 sv2 statO ⟷
¬ finalV sv1 ∧ Δ ∞ s1' s2' statA' (nextO sv1) sv2 statO"
unfolding match12_1_def validTrans_iff_next by simp
lemma match12_2_defD: "match12_2 Δ s1' s2' statA' sv1 sv2 statO ⟷
¬ finalV sv2 ∧ Δ ∞ s1' s2' statA' sv1 (nextO sv2) statO"
unfolding match12_2_def validTrans_iff_next by simp
lemma match12_12_defD: "match12_12 Δ s1' s2' statA' sv1 sv2 statO ⟷
(let statO' = sstatO' statO sv1 sv2 in
¬ finalV sv1 ∧ ¬ finalV sv2 ∧
(statA' = Diff ⟶ statO' = Diff) ∧
Δ ∞ s1' s2' statA' (nextO sv1) (nextO sv2) statO')"
unfolding match12_12_def validTrans_iff_next by simp
lemmas match12_defsD = match12_def match12_1_defD match12_2_defD match12_12_defD
lemmas match_deep_defsD = match1_defsD match2_defsD match12_defsD
lemma move_1_defD: "move_1 Δ w s1 s2 statA sv1 sv2 statO ⟷
¬ finalV sv1 ∧ Δ w s1 s2 statA (nextO sv1) sv2 statO"
unfolding move_1_def validTrans_iff_next by simp
lemma move_2_defD: "move_2 Δ w s1 s2 statA sv1 sv2 statO ⟷
¬ finalV sv2 ∧ Δ w s1 s2 statA sv1 (nextO sv2) statO"
unfolding move_2_def validTrans_iff_next by simp
lemma move_12_defD: "move_12 Δ w s1 s2 statA sv1 sv2 statO ⟷
(let statO' = sstatO' statO sv1 sv2 in
¬ finalV sv1 ∧ ¬ finalV sv2 ∧
Δ w s1 s2 statA (nextO sv1) (nextO sv2) statO')"
unfolding move_12_def validTrans_iff_next by simp
lemmas proact_defsD = proact_def move_1_defD move_2_defD move_12_defD
end
end