Avanesov, Tigran and Chevalier, Yannick and Rusinowitch, Michaël and Turuani, Mathieu
Intruder deducibility constraints with negation. Decidability and application to secured service compositions.
(2017)
Journal of Symbolic Computation, 80 (1). 4-26. ISSN 0747-7171
|
(Document in English)
PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader 1MB |
Official URL: https://doi.org/10.1016/j.jsc.2016.07.008
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.
Item Type: | Article |
---|---|
Audience (journal): | International peer-reviewed journal |
Uncontrolled Keywords: | |
Institution: | French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE) Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE) French research institutions > Institut National de la Recherche en Informatique et en Automatique - INRIA (FRANCE) Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE) Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE) Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE) Other partners > University of Luxembourg (LUXEMBOURG) |
Laboratory name: | |
Funders: | AVANTSSAR, 2008–2010, grant number 216471 - NESSoS, 2010–2014, grant number 256980 |
Statistics: | download |
Deposited On: | 18 Apr 2019 13:00 |
Repository Staff Only: item control page