Preserving opacity on Interval Markov Chains under simulation

Béatrice Bérard 1 Olga Kouchnarenko 2 John Mullins 3 Mathieu Sassolas 4
1 MoVe - Modélisation et Vérification
LIP6 - Laboratoire d'Informatique de Paris 6
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
3 EPM - École Polytechnique de Montréal
4 LACL - Laboratoire d'Algorithmique Complexité et Logique
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.
Document type :
Conference papers
Complete list of metadatas
https://hal.sorbonne-universite.fr/hal-01347712
Contributor : Béatrice Bérard <>
Submitted on : Thursday, July 21, 2016 - 3:50:45 PM
Last modification on : Friday, October 4, 2019 - 1:13:25 AM

Identifiers

Collections

UPMC | CNRS | UNIV-FCOMTE | UNIV-BM | FEMTO-ST | UNIV-BM-THESE | UPEC-UPEM | INRIA | UNIV-LORRAINE | LACL | LIP6 | LORIA-FM | LORIA | SORBONNE-UNIVERSITE | SU-SCIENCES | UPEC

Citation

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⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

578

Contact

Informations

CCSD