A sound decision procedure for the compositionality of secrecy
ESSoS'12: Proceedings of the 4th international conference on Engineering Secure Software and Systems(2012)
Abstract
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.
MoreTranslated text
Key words
multiple composition,sound decision procedure,tls protocol,tool support,algorithmic decision procedure,dolev-yao attacker model,complete protocol
AI Read Science
Must-Reading Tree
Example
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined