Preserving opacity on Interval Markov Chains under simulation - Sorbonne Université Access content directly
Conference Papers Year : 2016

Preserving opacity on Interval Markov Chains under simulation

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 φ. 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 φ in S as the maximal disclosure of φ 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.
No file

Dates and versions

hal-01347712 , version 1 (21-07-2016)

Identifiers

Cite

Béatrice Bérard, Olga Kouchnarenko, John Mullins, Mathieu Sassolas. Preserving opacity on Interval Markov Chains under simulation. WODES 2016 - 13th International Workshop on Discrete Event Systems , May 2016, Xi'an, China. pp.319-324, ⟨10.1109/WODES.2016.7497866⟩. ⟨hal-01347712⟩
328 View
0 Download

Altmetric

Share

Gmail Facebook X LinkedIn More