Probabilistic Opacity in Refinement-Based Modeling

TL;DR

This paper introduces a probabilistic framework for measuring and analyzing the disclosure of secrets in systems modeled by probabilistic transition systems, especially focusing on refinement and underspecified specifications.

Contribution

It defines a new measure of secret disclosure in probabilistic systems and proves that refinement enhances opacity in such models.

Findings

Computed worst-case disclosure for a subclass of IDTMCs.

Refinement improves the opacity of implementations.

Established a formal relationship between specifications and disclosure levels.

Abstract

Given a probabilistic transition system (PTS) $\cal A$ partially observed by an attacker, and an $\omega$-regular predicate $\varphi$over the traces of $\cal A$, measuring the disclosure of the secret $\varphi$ in $\cal A$ means computing the probability that an attacker who observes a run of $\cal A$ can ascertain that its trace belongs to $\varphi$. In the context of refinement, we consider specifications given as Interval-valued Discrete Time Markov Chains (IDTMCs), which are underspecified Markov chains where probabilities on edges are only required to belong to intervals. Scheduling an IDTMC $\cal S$ produces a concrete implementation as a PTS and we define the worst case disclosure of secret $\varphi$ in ${\cal S}$ as the maximal disclosure of $\varphi$ over all PTSs thus produced. We compute this value for a subclass of IDTMCs and we prove that refinement can only improve the opacity of implementations.