2023/09/18 by Matvey Soloviev, Soloviev, Matvey, Musard Balliu +3 · 4 citations
Computer Science · Social Sciences · #68Q60 #Access Control and Trust #Cryptography and Security (cs.CR) #D.4.6 #FOS: Computer and information sciences #I.2.4 #Information and Cyber Security #Logic in Computer Science (cs.LO) #Multi-Agent Systems and Negotiation #Multiagent Systems (cs.MA)
paper · pdf · doi:10.48550/arxiv.2309.09542
openalex publication_date 2023/09/18 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We introduce a framework for reasoning about the security of computer systems using modal logic. This framework is sufficiently expressive to capture a variety of known security properties, while also being intuitive and independent of syntactic details and enforcement mechanisms. We show how to use our formalism to represent various progress- and termination-(in)sensitive variants of confidentiality, integrity, robust declassification and transparent endorsement, and prove equivalence to standard definitions. The intuitive nature and closeness to semantic reality of our approach allows us to make explicit several hidden assumptions of these definitions, and identify potential issues and subtleties with them, while also holding the promise of formulating cleaner versions and future extension to entirely novel properties.