Hyperproperties were proposed as an abstract formalization of security policies, but unfortunately they lack a generic verification methodology. In an attempt to remedy this, we introduced the notion of incremental hyperproperties (IHPs), motivated by the observation that they have a clearer and more feasible verification methodology. To show that verification is indeed feasible, a decidable IHP verification methodology via games is presented and evaluated. The main advantage of the approach is that the games in combination with winning strategy evidence give valuable intuition about the security of a system and are very helpful when analyzing systems w.r.t. policy specifications. © 2013 Springer-Verlag.
CITATION STYLE
Milushev, D., & Clarke, D. (2013). Incremental hyperproperty model checking via games. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8208 LNCS, pp. 247–262). Springer Verlag. https://doi.org/10.1007/978-3-642-41488-6_17
Mendeley helps you to discover research relevant for your work.