Probabilistic Opacity in Refinement-Based Modeling
Given a probabilistic transition system (PTS) $\cal A$ partially observed by an attacker, and an $ω$-regular predicate $φ$over the traces of $\cal A$, measuring the disclosure of the secret $φ$ in $\cal A$ means computing the probability that an attacker who observes a run of $\cal A$ can ascertain that its trace belongs to $φ$. 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 $φ$ in ${\cal S}$ as the maximal disclosure of $φ$ 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.