Verifying Opacity Properties in Security Systems

Chunyan Mu, David Clark

Research output: Contribution to journalArticlepeer-review

47 Downloads (Pure)


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.
Original languageEnglish
Pages (from-to)1-11
Number of pages11
JournalIEEE Transactions on Dependable and Secure Computing
Publication statusPublished - 1 Mar 2022


Dive into the research topics of 'Verifying Opacity Properties in Security Systems'. Together they form a unique fingerprint.

Cite this