Model checking agent knowledge in dynamic access control policies

DOI10.1007/978-3-642-36742-7_31zbMATH Open1381.68171arXiv1401.4730OpenAlexW159958783MaRDI QIDQ5326344FDOQ5326344

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)

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.

Full work available at URL: https://arxiv.org/abs/1401.4730

Recommendations

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

Mathematics Subject Classification ID

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

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)