2013/06/24 by Koleini, Masoud, Clarkson, Michael R., Micinski, Kristopher K.
#Cryptography and Security (cs.CR) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.1306.5678
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.