Verifying Opacity Properties in Security Systems

We delineate a methodology for the specification and verification of flow security properties expressible in the opacity framework. We propose a logic,
${{\sf 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.