Towards quantitative analysis of opacity

J.W. Bryans, M. Koutny, C. Mu

    Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review

    8 Citations (Scopus)


    Opacity is a general approach for describing and unifying security properties expressed as predicates. A predicate is opaque if an observer of the system is unable to determine the satisfaction of the predicate in a given run of the system. The meaning of opacity is straightforward when considering the standard (qualitative) operational semantics, but there are a number of possible interpretations in a context where quantitative information about system evolutions is available. We propose four variants of quantitative opacity defined for probabilistic labelled transition systems, with each variant capturing a different aspect of quantifying the opacity of a predicate. Moreover, we present results showing how these four properties can be checked or approximated for specific classes of probabilistic labelled transition systems, observation functions, and system predicates.
    Original languageEnglish
    Title of host publicationTrustworthy Global Computing
    Subtitle of host publication7th International Symposium, TGC 2012, Newcastle upon Tyne, UK, Revised Selected Papers (Lecture Notes in Computer Science)
    EditorsCatuscia Palamidessi, Mark D. Ryan
    Place of PublicationHeidelberg
    Number of pages19
    Volume8191 LNCS
    ISBN (Electronic)9783642411571
    ISBN (Print)9783642411564
    Publication statusPublished - 2013
    Event7th International Symposium on Trustworthy Global Computing 2012 - Newcastle-upon-Tyne, United Kingdom
    Duration: 7 Sept 20128 Sept 2012
    Conference number: 7


    Conference7th International Symposium on Trustworthy Global Computing 2012
    Abbreviated titleTGC 2012
    Country/TerritoryUnited Kingdom
    Internet address


    • Probabilistic opacity
    • Probabilistic labelled transition systems
    • Observations


    Dive into the research topics of 'Towards quantitative analysis of opacity'. Together they form a unique fingerprint.

    Cite this