Skip to content


Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?

Latest commit


Git stats


Failed to load latest commit information.
Latest commit message
Commit time


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

Screenshot of Web Tool


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

Clone the repository

git clone
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


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:

  • 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.


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.