Quantitative Verification of Opacity Properties in Security Systems
Cryptography and Security
2022-06-30 v1
Abstract
We delineate a methodology for the specification and verification of flow security properties expressible in the opacity framework. We propose a logic, OpacTL , for straightforwardly expressing such properties in systems that can be modelled as partially observable labelled transition systems.We develop verification techniques for analysing property opacity with respect to observation notions. Adding a probabilistic operator to the specification language enables quantitative analysis and verification. This analysis is implemented as an extension to the PRISM model checker and illustrated via a number of examples. Finally, an alternative approach to quantifying the opacity property based on entropy is sketched.
Cite
@article{arxiv.2206.14317,
title = {Quantitative Verification of Opacity Properties in Security Systems},
author = {Chunyan Mu and David Clark},
journal= {arXiv preprint arXiv:2206.14317},
year = {2022}
}