Quantitative Verification of Opacity Properties in Security Systems

Chunyan Mu, David Clark

We delineate a methodology for the specification and verification of flow security properties expressible in the opacity framework. We propose a logic, OpacTL , for straightforward…