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.
Type de document :
Communication dans un congrès
WODES 2016 - 13th International Workshop on Discrete Event Systems , May 2016, Xi'an, China. Proceedings of 13th International Workshop on Discrete Event Systems (WODES) 2016, IEEE, pp.319-324, 2016, 〈Christos G. Cassandras and Alessandro Giua and Zhiwu Li〉. 〈10.1109/WODES.2016.7497866〉
Liste complète des métadonnées
https://hal.sorbonne-universite.fr/hal-01347712
Contributeur : Béatrice Bérard <>
Soumis le : jeudi 21 juillet 2016 - 15:50:45
Dernière modification le : mardi 18 décembre 2018 - 16:38:25

Identifiants

Collections

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

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. Proceedings of 13th International Workshop on Discrete Event Systems (WODES) 2016, IEEE, pp.319-324, 2016, 〈Christos G. Cassandras and Alessandro Giua and Zhiwu Li〉. 〈10.1109/WODES.2016.7497866〉. 〈hal-01347712〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

487

Contact

support.ccsd.cnrs.fr
hal.support@ccsd.cnrs.fr
Logo CCSD