CryptoSolve: Towards a Tool for the Symbolic Analysis of Cryptographic Algorithms

Dalton Chichester
(University of Mary Washington)
Wei Du
(University at Albany-SUNY)
Raymond Kauffman
(University of Mary Washington)
Hai Lin
(Clarkson University)
Christopher Lynch
(Clarkson University)
Andrew M. Marshall
(University of Mary Washington)
Catherine A. Meadows
(Naval Research Laboratory)
Paliath Narendran
(University at Albany-SUNY)
Veena Ravishankar
(University of Mary Washington)
Luis Rovira
(University of Mary Washington)
Brandon Rozek
(Rensselaer Polytechnic Institute)

Recently, interest has been emerging in the application of symbolic techniques to the specification and analysis of cryptosystems. These techniques, when accompanied by suitable proofs of soundness/completeness, can be used both to identify insecure cryptosystems and prove sound ones secure. But although a number of such symbolic algorithms have been developed and implemented, they remain scattered throughout the literature. In this paper, we present a tool, CryptoSolve, which provides a common basis for specification and implementation of these algorithms, CryptoSolve includes libraries that provide the term algebras used to express symbolic cryptographic systems, as well as implementations of useful algorithms, such as unification and variant generation. In its current initial iteration, it features several algorithms for the generation and analysis of cryptographic modes of operation, which allow one to use block ciphers to encrypt messages more than one block long. The goal of our work is to continue expanding the tool in order to consider additional cryptosystems and security questions, as well as extend the symbolic libraries to increase their applicability.

In Pierre Ganty and Dario Della Monica: Proceedings of the 13th International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2022), Madrid, Spain, September 21-23, 2022, Electronic Proceedings in Theoretical Computer Science 370, pp. 147–161.
Published: 20th September 2022.

ArXived at: http://dx.doi.org/10.4204/EPTCS.370.10 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org