Theory Incomplete
section ‹Relative Security Unwinding Incompleteness example›
text ‹Demonstrating a counterexample which is secure but fails in the infinatary unwinding›
theory Incomplete
imports Unwinding
begin
no_notation bot ("⊥")
abbreviation noninform ("⊥") where "⊥ ≡ undefined"
text ‹Demonstrating a counterexample which is secure but fails in the unwinding›
datatype State = ss | ss'
type_synonym secret = "State"
fun transit::"State ⇒ State ⇒ bool"(infix "→I" 55) where
"transit s s' = (if (s = ss ∧ s' = ss') then True else False)"
lemma transit_singlv:"ss →I ss'" by auto
lemma transit_iff:"s →I s' ⟷ (s = ss ∧ s' = ss')" by auto
definition "final x ≡ ∀y. ¬ (→I) x y"
lemma final_sv'[simp]:"final ss'" unfolding final_def transit_iff by auto
lemma final_iff: "final s ⟷ s = ss'" unfolding final_def transit_iff by (auto,metis State.exhaust)
text ‹Vanilla-semantics system model›
type_synonym stateV = State
fun validTransV where "validTransV (s,s') = s →I s'"
text ‹No secrets or interaction›
fun isIntV :: "stateV ⇒ bool" where "isIntV s = False"
fun getIntV::"stateV ⇒ nat × nat" where "getIntV s = (⊥,⊥)"
definition isSecV :: "stateV ⇒ bool" where "isSecV s = False"
fun getSecV :: "stateV ⇒ secret" where "getSecV s = s"
text ‹The optimization-enhanced system model›
type_synonym stateO = State
fun validTransO where "validTransO (s,s') = s →I s'"
text ‹No interaction, only isSec at starting state›
fun isIntO :: "stateO ⇒ bool" where "isIntO s = False"
fun getIntO::"stateO ⇒ nat × nat" where "getIntO s = (⊥,⊥)"
definition isSecO :: "stateO ⇒ bool" where "isSecO s = (if s = ss then True else False)"
fun getSecO :: "stateO ⇒ secret" where "getSecO s = s"
text ‹corrState›
fun corrState :: "stateV ⇒ stateO ⇒ bool" where
"corrState cfgO cfgA = True"