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

DOI10.1016/J.JSC.2016.07.008zbMATH Open1356.68012arXiv1207.4871OpenAlexW2132938106MaRDI QIDQ507348FDOQ507348

Authors: Tigran Avanesov, Yannick Chevalier, Mathieu Turuani, Michaël Rusinowitch 

Publication date: 6 February 2017

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1207.4871

Recommendations

• Satisfiability of general intruder constraints with and without a set constructor
• A proof theoretic analysis of intruder theories
• Automata, Languages and Programming
• Hierarchical Combination of Intruder Theories
• Deducibility constraints and blind signatures

zbMATH Keywords

synthesisformal methodsautomated verificationcryptographic protocolsweb servicesorchestrationsecurity policydeducibility constraintsseparation of duty

Mathematics Subject Classification ID

Data encryption (aspects in computer science) (68P25) Cryptography (94A60) Internet topics (68M11) Authentication, digital signatures and secret sharing (94A62)

Cites Work

• Automatic recognition of tractability in inference relations
• Deciding knowledge in security protocols under equational theories
• On the security of public key protocols
• A logic of trust and reputation
• Protocol insecurity with a finite number of sessions and composed keys is NP-complete.
• Deciding security properties for cryptographic protocols. application to key cycles
• On the relative soundness of the free algebra model for public key encryption
• Trust and Norms in the Context of Computer Security: A Logical Formalization
• The CL-Atse Protocol Analyser
• Towards an Integrated Formal Analysis for Security and Trust

Cited In (2)

• Security issues in service composition
• Secure Service Orchestration

This page was built for publication: Intruder deducibility constraints with negation. Decidability and application to secured service compositions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q507348)