cryptosolvers / cryptosolve

Generate and Verify Cryptographic Modes of Operation using Symbolic Methods

CryptoSolve

This is a tool that generates and verifies cryptographic modes of operation using symbolic methods.

Install

To get started you should make sure that your environment is setup.

Clone the repository

git clone https://github.com/cryptosolvers/cryptosolve
cd CryptoSolve

Create a virtual environment

python3 -m venv senv

Set your terminal session to use that environment

source senv/bin/activate

Install moe package

./install_packages.sh

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.

Usage

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

Libraries Included

CryptoSolve is built upon several libraries that can be used standalone for other areas in Unification and automated reasoning.

MOE

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.

Algebra

A term algebra library that defines a term recursively. Contains useful operations on terms such as substitution, and interfaces into sympy and general strings.

Rewrite

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.

Unification

This module contains unification over terms modulo several popular theories. Currently AC Unification, Boolean Unification, EAC Unification, Syntactic Unification, and others are defined.

Theories

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.