This is a tool that generates and verifies cryptographic modes of operation using symbolic methods.
To get started you should make sure that your environment is setup.
Clone the repository
git clone https://github.com/symcollab/CryptoSolve cd CryptoSolve
Create a virtual environment
python3 -m venv senv
Set your terminal session to use that environment
Install moe package
If you encounter any permission errors, edit the file to look like the following instead,
pip install --user directoryname/
Now you can run the examples! In the future, don’t forget to
source the environment every time you open a new terminal session.
The following commands are then in your path:
- moe_tool : Runs the command line version of the tool
- moe_website : Runs the website version of the tool
CryptoSolve is built upon several libraries that can be used standalone for other areas in Unification and automated reasoning.
This module builds upon the rest of the modules defined below in order to express cryptographic modes of operation symbolically. The user can interface with this module via the web, terminal, or GUI application.
A term algebra library that defines a term recursively. Contains useful operations on terms such as substitution, and interfaces into sympy and general strings.
The rewrite library contains contains rewrite rules that can operate over the terms in the algebra library. It also can produce variants given a set of rewrite rules, and can narrow one term into another.
This module contains unification over terms modulo several popular theories. Currently AC Unification, Boolean Unification, EAC Unification, Syntactic Unification, and others are defined.
Various data structures and their properties defined as rewrite rules are defined in this module. This module can be further extended in order to define an automated theorem prover for objects such as natural numbers, booleans, and lists.
The Symcollab collaboration consist of the following people both past and present:
- Brandon Rozek (Rensselaer Polytechnic Institute)
- Hai Lin (Clarkson University)
- Wei Du (University at Albany–SUNY)
- Catherine Meadows (Naval Research Laboratory)
- Chris Lynch (Clarkson University)
- Paliath Narendran (University at Albany–SUNY)
- Veena Ravishankar (University of Mary Washington)
- Meghan Cooke (University of Mary Washington)
- Mikayla Stitts (University of Mary Washington)
- Serdar Erbatur (University of Texas at Dallas)
- Andrew Marshall (University of Mary Washington)
- Luis Rovira
- Raymond Kauffman
- Dalton Chichester
- Formal Analysis of Symbolic Authenticity
- Algorithmic Problems in the Symbolic Approach to the Verification of Automatically Synthesized Cryptosystems
- Moving the Bar on Computationally Sound Exclusive-Or