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. © 2012 Springer-Verlag.
CITATION STYLE
Ochoa, M., Jürjens, J., & Warzecha, D. (2012). A sound decision procedure for the compositionality of secrecy. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7159 LNCS, pp. 97–105). https://doi.org/10.1007/978-3-642-28166-2_10
Mendeley helps you to discover research relevant for your work.