Probabilistic Opacity in Refinement-Based Modeling

Abstract : Given a probabilistic transition system (PTS) A partially observed by an attacker, and an ω-regular predicate ϕ over the traces of A, measuring the disclosure of the secret ϕ in A means computing the probability that an attacker who observes a run of 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 S produces a concrete implementation as a PTS and we define the worst case disclosure of secret ϕ in 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.
Document type :
Preprints, Working Papers, ...
Complete list of metadatas

Cited literature [18 references]  Display  Hide  Download
Contributor : Béatrice Bérard <>
Submitted on : Thursday, July 21, 2016 - 3:40:01 PM
Last modification on : Friday, October 4, 2019 - 1:30:07 AM


Files produced by the author(s)


  • HAL Id : hal-01347699, version 1


Béatrice Bérard, Olga Kouchnarenko, John Mullins, Mathieu Sassolas. Probabilistic Opacity in Refinement-Based Modeling. 2015. ⟨hal-01347699⟩



Record views


Files downloads