Verifying Opacity Properties in Security Systems

Chunyan Mu* (Corresponding Author), David Clark

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

1 Citation (Scopus)
6 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)1450-1460
Number of pages11
JournalIEEE Transactions on Dependable and Secure Computing
Issue number2
Early online date1 Mar 2022
Publication statusPublished - 1 Mar 2022


  • opacity
  • logic
  • security
  • verification


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

Cite this