Abstract
This paper presents a new algorithm for synthesising attacks on cryptographic protocols. The algorithm constructs attacks where the attacker interacts with the agents in the system in order to discover some set of restricted information or send a specific message to another participant in the protocol. This attacker is akin to the Dolev-Yao model of attacker but behaves in a manner that does not betray its presence in the system. The state space reduction heuristics used in the algorithm manage the growth of the state space through the use of strict typing and by only allowing protocol specifications that do not deadlock. The cryptographic protocols are specified in the spi calculus. The variant of the spi calculus used is a syntactically restricted variant which is semantically equivalent to the full spi calculus. A model checker based on this algorithm has been implemented, and the results of this model checker on common cryptographic protocols are presented. This technique can be used to quickly search for an attack on a protocol. The knowledge of the structure of such an attack will enable the protocol designers to repair the protocol.
This research is part of the IMPROVE project and is funded by Enterprise Ireland Strategic Research Grant ST/2000/94.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Diffie, W., Hellman, M.E.: New Directions in Cryptography. IEEE Transactions on Information Theory 22(6), 644–654 (1976)
Rivest, R.L., Shamir, A., Aldeman, L.M.: A method for obtaining digital signatures and public-key cryptosystems. Communications of the ACM 21(2), 120–126 (1978)
Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security 6, 85–128 (1998)
Schumann, J.: Automated Verification of Cryptograhic Protocols wiht SETHEO. In: McCune, W. (ed.) CADE 1997. LNCS, vol. 1249, pp. 87–100. Springer, Heidelberg (1997)
Paulson, L.C.: Inductive analysis of the Internet protocol TLS. ACM Transaction on Computer and System Security 2(3), 332–351 (1999)
Lowe, G.: Breaking and Fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)
Armando, A., Basin, D., Bouallagui, M., Chavalier, Y., Compagna, L., Mödersheim, S., Rusinowitch, M., Turin, M., Viganò, L., Vigneron, L.: The AVISS Security Protocol Tool. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 349–353. Springer, Heidelberg (2002)
Gnesi, S., Latella, D., Lenzini, G.: A “Brutus” logic for the Spi-Calculus. In: Proceedings of the Workshop on Issues in the Theory of Security (WITS 2002)
Mitchell, J.C., Mitchell, M., Stern, U.: Automated analysis of cryptographic protocols using Murφ. In: Proceedings of the 1997 IEEE Symposium on Security and Privacy, pp. 141–153. IEEE Computer Society Press, Los Alamitos (1997)
Goubault-Larrecq, J.: A Method for Automatic Cryptographic Protocol Verification. In: Rolim, J.D.P. (ed.) IPDPS-WS 2000. LNCS, vol. 1800, pp. 977–984. Springer, Heidelberg (2000)
Monniaux, D.: Abstracting Cryptographic Protocols with Tree Automata. In: Tsur, S. (ed.) NGITS 1999. LNCS, vol. 1649, pp. 149–163. Springer, Heidelberg (1999)
Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. In: Fourth ACM Conference on Computer and Communications Security, pp. 36–47. ACM Press, New York (1997)
Abstract Syntax Notation One (ASN.1), Specification of Basic Notation. ITU-T Rec. X.680 (2002) — ISO/IEC 8824-1:2002.
Aresenault, A., Turner, S.: Internet X.509 Public Key Infrastructure: Roadmap. Internet Draft (2002)
Milner, R.: Communicating and mobile systems: the π-calculus. Cambridge University Press, Cambridge (1999)
Sangiorgi, D., Walker, D.: The π-calculus, A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)
Dolev, D., Yao, A.C.: On the Security of Public Key Protocols. IEEE Transactions on Information Theory 29(8), 198–208 (1983)
Chevalier, Y., Vigneron, L.: Automated Unbounded Verifiaction of Security Protocols. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 324–337. Springer, Heidelberg (2002)
Fiore, M., Abadi, M.: Computing Symbolic Models for Verifying Cryptographic Protocols. In: Proceedings of the 14th Computer Security Foundations Workshop (CSFW14), pp. 160–173. IEEE Computer Society Press, Los Alamitos (2001)
Clarke, E.M., Jha, S., Marrero, W.: Using State Space Exploration and a Natural Deduction Style Message Derivation Engine to Verify Security Protocols. In: International Conference on Programmng Concepts and Methods (PROCOMET 1998), IFIP Conference Proceedings, vol. 125, Chapman & Hall, Boca Raton (1998)
Needham, R., Schroeder, M.: Using Encryption for Authentication in Large Networks of Computers. Communications of the ACM 21(12), 993–999 (1978)
Otway, D., Rees, O.: Efficient and Timely Mutual Authentication. ACM Operating System Review 21(1), 8–10 (1987)
Boyd, C., Mao, W.: On the limitations of BAN logic. In: Helleseth, T. (ed.) EUROCRYPT 1993. LNCS, vol. 765, pp. 240–247. Springer, Heidelberg (1994)
Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction To Algorithms. McGraw-Hill, New York (1990)
Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (Revised). The MIT Press, Cambridge (1997)
Cejtin, H., Jagannathana nd, S.,Weeks, S.: Flow-Directed Closure Conversion for Typed Languages. In: European Symposium on Programming (ESOP) (2000)
Lowe, G.: An attack on the Needham-Schroeder public-key authentication protocol. Information Processing Letters 56(3), 131–133 (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sinclair, D., Gray, D., Hamilton, G. (2004). Synthesising Attacks on Cryptographic Protocols. In: Wang, F. (eds) Automated Technology for Verification and Analysis. ATVA 2004. Lecture Notes in Computer Science, vol 3299. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30476-0_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-30476-0_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23610-8
Online ISBN: 978-3-540-30476-0
eBook Packages: Springer Book Archive