Intruder deducibility constraints with negation. Decidability and application to secured service compositions

Tigran Avanesov 1 Yannick Chevalier 2 Michael Rusinowitch 3 Mathieu Turuani 3
1 SnT - Interdisciplinary Centre for Security, Reliability and Trust [Luxembourg]
2 IRIT - Institut de recherche en informatique de Toulouse
3 PESTO - Proof techniques for security protocols
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : We consider a problem of automated orchestration of security-aware services under additional constraints. The problem of finding a mediator to compose secured services has been reduced in previous works to the problem of solving deducibility constraints similar to those employed for cryptographic protocol analysis. We extend in this paper the mediator synthesis procedure (i.e. a solution for the orchestration problem) by allowing additional non-disclosure policies that express the fact that some data is not accessible to the mediator at a given point of its execution. We present a decision procedure that answers the question whether a mediator satisfying these policies can be effectively synthesized. The approach presented in this work extends the constraint solving procedure for cryptographic protocol analysis in a significant way as to be able to handle negation of deducibility constraints. It applies to all subterm convergent theories and therefore covers several interesting theories in formal security analysis including encryption, hashing, signature and pairing; it is also expressive enough for some RBAC policies. A variant of this procedure for Dolev Yao theory has been implemented in Cl-Atse, a protocol analysis tool based on constraint solving.
Keywords : Automated verification Cryptographic protocols Formal methods Web services Orchestration Security policy Separation of duty Deducibility constraints Synthesis
Type de document :
Article dans une revue
Journal of Symbolic Computation, Elsevier, 2017, 80, pp.4 - 26. 〈10.1016/j.jsc.2016.07.008〉
Liste complète des métadonnées

Littérature citée [30 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01405851
Contributeur : Michaël Rusinowitch <>
Soumis le : jeudi 1 décembre 2016 - 09:45:49
Dernière modification le : mercredi 20 février 2019 - 11:28:02
Document(s) archivé(s) le : mardi 21 mars 2017 - 06:55:18

Fichier

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

Identifiants

Collections

UNIV-TLSE3 | INRIA | SMS | UNIV-TLSE2 | LORIA | LORIA-FM | UNIV-LORRAINE | INRIA2017

Citation

Tigran Avanesov, Yannick Chevalier, Michael Rusinowitch, Mathieu Turuani. Intruder deducibility constraints with negation. Decidability and application to secured service compositions. Journal of Symbolic Computation, Elsevier, 2017, 80, pp.4 - 26. 〈10.1016/j.jsc.2016.07.008〉. 〈hal-01405851〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

558

Téléchargements de fichiers

86

Contact


archive-ouverte@inria.fr