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

TL;DR

This paper introduces a decision procedure for deducibility constraints with negation, enabling effective synthesis of mediators that enforce non-disclosure policies in secure service compositions, extending cryptographic protocol analysis tools.

Contribution

It extends existing constraint solving methods by allowing negative deducibility constraints, applicable to a wide range of security theories, and implements this in the CL-AtSe tool.

Findings

Effective decision procedure for negative deducibility constraints.

Applicable to encryption, hashing, signature, and pairing theories.

Successfully integrated into protocol analysis for secure service composition.

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.