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/cryptosolvers/cryptosolve
cd CryptoSolveCreate a virtual environment
python3 -m venv senvSet your terminal session to use that environment
source senv/bin/activateInstall moe package
./install_packages.shIf 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:
- moo_tool : Runs the command line version of the tool
- moo_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.