Probabilistic Opacity in Refinement-Based Modeling - Sorbonne Université Accéder directement au contenu
Pré-Publication, Document De Travail Année : 2015

Probabilistic Opacity in Refinement-Based Modeling

Résumé

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.
Fichier principal
Vignette du fichier
OpacityOnIMDP.pdf (344.06 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

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

Identifiants

  • HAL Id : hal-01347699 , version 1

Citer

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

Partager

Gmail Facebook X LinkedIn More