A Temporal Logic of Security
Logic in Computer Science
2013-07-10 v2 Cryptography and Security
Abstract
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 quantification over multiple execution paths, thereby enabling HyperLTL to express information-flow security policies that LTL cannot. A model-checking algorithm for a fragment of HyperLTL is given, and the algorithm is implemented in a prototype model checker. The class of security policies expressible in HyperLTL is characterized by an arithmetic hierarchy of hyperproperties.
Cite
@article{arxiv.1306.5678,
title = {A Temporal Logic of Security},
author = {Masoud Koleini and Michael R. Clarkson and Kristopher K. Micinski},
journal= {arXiv preprint arXiv:1306.5678},
year = {2013}
}