Probabilistic Disclosure: Maximisation vs. Minimisation

Béatrice Bérard 1, 2 Serge Haddad 3, 1 Engel Lefaucheux 4, 1
2 MoVe - Modélisation et Vérification
LIP6 - Laboratoire d'Informatique de Paris 6
3 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
4 SUMO - SUpervision of large MOdular and distributed systems
Inria Rennes – Bretagne Atlantique , IRISA_D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : We consider opacity questions where an observation function provides to an external attacker a view of the states along executions and secret executions are those visiting some state from a fixed subset. Disclosure occurs when the observer can deduce from a finite observation that the execution is secret, the ε-disclosure variant corresponding to the execution being secret with probability greater than 1 − ε. In a probabilistic and non deterministic setting, where an internal agent can choose between actions, there are two points of view, depending on the status of this agent: the successive choices can either help the attacker trying to disclose the secret, if the system has been corrupted, or they can prevent disclosure as much as possible if these choices are part of the system design. In the former situation, corresponding to a worst case, the disclosure value is the supremum over the strategies of the probability to disclose the secret (maximisation), whereas in the latter case, the disclosure is the infimum (minimisation). We address quantitative problems (comparing the optimal value with a threshold) and qualitative ones (when the threshold is zero or one) related to both forms of disclosure for a fixed or finite horizon. For all problems, we characterise their decidability status and their complexity. We discover a surprising asymmetry: on the one hand optimal strategies may be chosen among deterministic ones in maximisation problems, while it is not the case for minimisation. On the other hand, for the questions addressed here, more minimisation problems than maximisation ones are decidable.
Type de document :
Communication dans un congrès
FSTTCS 2017, Dec 2017, Kanpur, India. 〈10.4230/LIPIcs.FSTTXS.2017〉
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01618955
Contributeur : Engel Lefaucheux <>
Soumis le : mercredi 18 octobre 2017 - 17:29:45
Dernière modification le : vendredi 31 août 2018 - 09:25:57
Document(s) archivé(s) le : vendredi 19 janvier 2018 - 14:17:43

Fichier

fsttcs-main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Béatrice Bérard, Serge Haddad, Engel Lefaucheux. Probabilistic Disclosure: Maximisation vs. Minimisation . FSTTCS 2017, Dec 2017, Kanpur, India. 〈10.4230/LIPIcs.FSTTXS.2017〉. 〈hal-01618955〉

Partager

Métriques

Consultations de la notice

378

Téléchargements de fichiers

52