Opacity for Linear Constraint Markov Chains

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
Abstract : On a partially observed system, a secret ϕ is opaque if an observer cannot ascertain that its trace belongs to ϕ. We consider specifications given as Constraint Markov Chains (CMC), which are underspec-ified Markov chains where probabilities on edges are required to belong to some set. The nondeterminism is resolved by a scheduler, and opacity on this model is defined as a worst case measure over all implementations obtained by scheduling. This measures the information obtained by a passive observer when the system is controlled by the smartest sched-uler in coalition with the observer. When restricting to the subclass of Linear CMC, we compute (or approximate) this measure and prove that refinement of a specification can only improve opacity.
Document type :
Liste complète des métadonnées

Cited literature [24 references]  Display  Hide  Download

Contributor : Béatrice Bérard <>
Submitted on : Wednesday, October 19, 2016 - 2:36:15 PM
Last modification on : Wednesday, April 3, 2019 - 1:22:55 AM


Files produced by the author(s)


  • HAL Id : hal-01384153, version 1


Béatrice Bérard, Olga Kouchnarenko, John Mullins, Mathieu Sassolas. Opacity for Linear Constraint Markov Chains. [Research Report] LIP6 UMR 7606 UPMC Sorbonne Universités, France; Univ. de Franche-Comté; Ecole Polytechnique de Montréal; LACL, Université Paris-Est. 2016. ⟨hal-01384153⟩



Record views


Files downloads