1 citations · 1 across the 4 of their papers we have counts for
5 papers
Checking Interaction-Based Declassification Policies for Android Using Symbolic Execution
Kristopher Micinski, Jonathan Fetter-Degges, Jinseong Jeon +2
Mobile apps can access a wide variety of secure information, such as contacts and location. However, current mobile platforms include only coarse access control mechanisms to prote…
Temporal Logics for Hyperproperties
Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini +3
Two new logics for verification of hyperproperties are proposed. Hyperproperties characterize security policies, such as noninterference, as a property of sets of computation paths…
A Temporal Logic of Security
Masoud Koleini, Michael R. Clarkson, Kristopher K. Micinski
A new logic for verification of security policies is proposed. The logic, HyperLTL, extends linear-time temporal logic (LTL) with connectives for explicit and simultaneous quantifi…
Belief Semantics of Authorization Logic
Andrew K. Hirsch, Michael R. Clarkson
Authorization logics have been used in the theory of computer security to reason about access control decisions. In this work, a formal belief semantics for authorization logics is…
Nexus Authorization Logic (NAL): Logical Results
Andrew K. Hirsch, Michael R. Clarkson
Nexus Authorization Logic (NAL) [Schneider et al. 2011] is a logic for reasoning about authorization in distributed systems. A revised version of NAL is given here, including revis…