Model checking agent knowledge in dynamic access control policies

DOI10.1007/978-3-642-36742-7_31MaRDI QIDQ5326344zbMATH OpenOpenAlexFDO

Authors Masoud Koleini, Eike Ritter, M. D. Ryan

Publication date 5 August 2013

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1401.4730, http://link.springer.com/chapter/10.1007/978-3-642-36742-7_31

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: We develop a modeling technique based on interpreted systems in order to verify temporal-epistemic properties over access control policies. This approach enables us to detect information flow vulnerabilities in dynamic policies by verifying the knowledge of the agents gained by both reading and reasoning about system information. To overcome the practical limitations of state explosion in model-checking temporal-epistemic properties, we introduce a novel abstraction and refinement technique for temporal-epistemic safety properties in ACTLK (ACTL with knowledge modality K) and a class of interesting properties that does fall in this category.

Recommendations

• Information Security
• Information Security
• Specifying and Reasoning About Dynamic Access-Control Policies
• Analysis of dynamic policies
• Computer Aided Verification

Cited in

(1)

• Information Security

This page was built for publication: Model checking agent knowledge in dynamic access control policies

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5326344)