A sound decision procedure for the compositionality of secrecy

The composition of processes is in general not secrecy preserving under the Dolev-Yao attacker model. In this paper, we describe an algorithmic decision procedure which determines whether the composition of secrecy preserving processes is still secrecy preserving. As a case-study we consider a variant of the TLS protocol where, even though the client and server considered separately would be viewed as preserving the secrecy of the data to be communicated, its composition to the complete protocol does not preserve that secrecy. We also show results on tool support that allows one to validate the efficiency of our algorithm for multiple compositions.