Quantitative Verification of Opacity Properties in Security Systems

TL;DR

This paper introduces a new logic and verification techniques for analyzing and quantifying opacity properties in security systems, extending existing tools with probabilistic and entropy-based methods.

Contribution

It presents OpacTL, a logic for specifying opacity, along with verification techniques and an extension to PRISM for quantitative analysis of security properties.

Findings

Implementation in PRISM demonstrates practical applicability.

Probabilistic operator enables quantitative opacity analysis.

Entropy-based approach offers an alternative quantification method.

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.