Abstract
We propose a class of protocol transformations, which can be used to (1) develop (families of) security protocols by refinement and (2) abstract existing protocols to increase the efficiency of verification tools. We prove the soundness of these transformations with respect to an expressive security property specification language covering secrecy and authentication properties. Our work clarifies and significantly extends the scope of earlier work in this area. We illustrate the usefulness of our approach on a family of key establishment protocols.
This work is partially supported by the EU FP7-ICT-2009.1.4 Project No. 256980, NESSoS: Network of Excellence on Engineering Secure Future Internet Software Services and Systems.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Arapinis, M.: Sécurité des protocoles cryptographiques: décidabilité et résultats de réduction. PhD thesis, Université Paris-Est (November 2008)
Arapinis, M., Duflot, M.: Bounding Messages for Free in Security Protocols. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 376–387. Springer, Heidelberg (2007)
Armando, A., Compagna, L.: SAT-based model-checking for security protocols analysis. International Journal of Information Security 7(1), 3–32 (2008)
Bieber, P., Boulahia-Cuppens, N.: Formal development of authentication protocols. In: Sixth BCS-FACS Refinement Workshop (1994)
Cervesato, I., Meadows, C., Pavlovic, D.: An encapsulated authentication logic for reasoning about key distribution protocols. In: CSFW 2005: Proceedings of the 18th IEEE Workshop on Computer Security Foundations, Washington, DC, USA, pp. 48–61 (2005)
Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: Abstraction and refinement in protocol derivation. In: Proc. 17th IEEE Computer Security Foundations Workshop, CSFW (2004)
Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: A derivation system and compositionl logic for security protocols. Journal of Computer Security 13, 423–482 (2005)
Guttman, J.D.: Transformations between Cryptographic Protocols. In: Degano, P., Viganò, L. (eds.) ARSPA-WITS 2009. LNCS, vol. 5511, pp. 107–123. Springer, Heidelberg (2009)
Guttman, J.D.: Security Goals and Protocol Transformations. In: Mödersheim, S., Palamidessi, C. (eds.) TOSCA 2011. LNCS, vol. 6993, pp. 130–147. Springer, Heidelberg (2012)
Heather, J., Lowe, G., Schneider, S.: How to prevent type flaw attacks on security protocols. Journal of Computer Security 11(2), 217–244 (2003)
Hui, M.L., Lowe, G.: Fault-preserving simplifying transformations for security protocols. Journal of Computer Security 9(1/2), 3–46 (2001)
Li, Y., Yang, W., Huang, C.-W.: Preventing type flaw attacks on security protocols with a simplified tagging scheme. In: Waldron, J. (ed.) ISICT. ACM International Conference Proceeding Series, vol. 90, pp. 244–249. Trinity College Dublin (2004)
Meadows, C.A.: Analyzing the Needham-Schroeder Public-Key Protocol: A Comparison of Two Approaches. In: Bertino, E., Kurth, H., Martella, G., Montolivo, E. (eds.) ESORICS 1996. LNCS, vol. 1146, pp. 351–364. Springer, Heidelberg (1996)
Meier, S., Cremers, C.J.F., Basin, D.A.: Strong invariants for the efficient construction of machine-checked protocol security proofs. In: Proc. 23th IEEE Computer Security Foundations Symposium, CSF, pp. 231–245 (2010)
Nguyen, B.T., Sprenger, C.: Sound security protocol transformations. Technical Report 781, Department of Computer Science, ETH Zurich (2012)
Pavlovic, D., Meadows, C.: Deriving Secrecy in Key Establishment Protocols. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol. 4189, pp. 384–403. Springer, Heidelberg (2006)
Sprenger, C., Basin, D.: Refining key establishment. In: Proc. 25th IEEE Computer Security Foundations Symposium, CSF, pp. 230–246 (2012)
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nguyen, B.T., Sprenger, C. (2013). Sound Security Protocol Transformations. In: Basin, D., Mitchell, J.C. (eds) Principles of Security and Trust. POST 2013. Lecture Notes in Computer Science, vol 7796. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-36830-1_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-36830-1_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-36829-5
Online ISBN: 978-3-642-36830-1
eBook Packages: Computer ScienceComputer Science (R0)