Preserving Opacity on Interval Markov Chains under Simulation

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