Skip to Main content Skip to Navigation
New interface
Reports (Research report)

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

Tigran Avanesov 1, 2 Yannick Chevalier 2, 3 Michaël Rusinowitch 4 Mathieu Turuani 4 
2 IRIT-LILaC - Logique, Interaction, Langue et Calcul
IRIT - Institut de recherche en informatique de Toulouse
4 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 : The problem of finding a mediator to compose secured services has been reduced in our former work to the problem of solving deducibility constraints similar to those employed for cryptographic protocol analysis. We extend in this paper the mediator synthesis procedure by a construction for expressing that some data is not accessible to the mediator. Then we give a decision procedure for verifying that a mediator satisfying this non-disclosure policy can be effectively synthesized. This procedure has been implemented in CL-AtSe, our protocol analysis tool. The procedure extends constraint solving for cryptographic protocol analysis in a significative way as it is able to handle negative deducibility constraints without restriction. In particular it applies to all subterm convergent theories and therefore covers several interesting theories in formal security analysis including encryption, hashing, signature and pairing.
Complete list of metadata

Cited literature [20 references]  Display  Hide  Download
Contributor : Tigran Avanesov Connect in order to contact the contributor
Submitted on : Wednesday, July 18, 2012 - 5:00:40 PM
Last modification on : Wednesday, October 26, 2022 - 8:14:11 AM
Long-term archiving on: : Friday, December 16, 2016 - 12:53:32 AM


Files produced by the author(s)


  • HAL Id : hal-00719011, version 1
  • ARXIV : 1207.4871


Tigran Avanesov, Yannick Chevalier, Michaël Rusinowitch, Mathieu Turuani. Intruder deducibility constraints with negation. Decidability and application to secured service compositions.. [Research Report] RR-8017, INRIA. 2012. ⟨hal-00719011⟩



Record views


Files downloads