Concurrent secrets with quantified suspicion - Archive ouverte HAL Access content directly
Conference Papers Year :

Concurrent secrets with quantified suspicion

(1) , (1) , (2)


A system satisfies opacity if its secret behaviors cannot be detected by any user of the system. Opacity of distributed systems was originally set as a boolean predicate before being quantified as measures in a probabilistic setting. This paper considers a different quantitative approach that measures the efforts that a malicious user has to make to detect a secret. This effort is measured as a distance w.r.t a regular profile specifying a normal behavior. This leads to several notions of quantitative opacity. When attackers are passive that is, when they just observe the system, quantitative opacity is brought back to a language inclusion problem, and is PSPACE-complete. When attackers are active, that is, interact with the system in order to detect secret behaviors within a finite depth observation, quantitative opacity turns to be a two-player finite-state quantitative game of partial observation. A winning strategy for an attacker is a sequence of interactions with the system leading to a secret detection without exceeding some profile deviation measure threshold. In this active setting, the complexity of opacity is EXPTIME-complete.
Fichier principal
Vignette du fichier
HMMSuspicious.pdf (426.23 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-01757949 , version 1 (04-04-2018)


  • HAL Id : hal-01757949 , version 1


Loïc Hélouët, Hervé Marchand, John Mullins. Concurrent secrets with quantified suspicion. ACSD' 2018 - 18th International Conference on Application of Concurrency to System Design, Jun 2018, Bratislava, Slovakia. pp.1-15. ⟨hal-01757949⟩
185 View
147 Download


Gmail Facebook Twitter LinkedIn More