Intruder Deducibility Constraints with Negation. Decidability and Application to Secured Service Compositions
The problem of finding a mediator to compose secured services has been reduced in users' former work to the problem of solving deducibility constraints similar to those employed for cryptographic protocol analysis. The authors extend in this paper the mediator synthesis procedure by a construction for expressing that some data is not accessible to the mediator. Then, they 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, their 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.