---
title: "CryptoSolve: Towards a Tool for the Symbolic Analysis of Cryptographic Algorithms"
authors: [
    "Dalton Chichester",
    "Wei Du",
    "Raymond Kauffman",
    "Hai Lin",
    "Christopher Lynch",
    "Andrew M. Marshall",
    "Catherine A. Meadows",
    "Paliath Narendran",
    "Veena Ravishankar",
    "Luis Rovira",
    "Brandon Rozek"
]
publish_date: "2022/3/14"
conference: "International Workshop on Rewriting Logic and its Applications"
firstpage: 6
lastpage: 25
language: "English"
pdf_url: "http://sv.postech.ac.kr/wrla2022/assets/files/pre-proceedings-WRLA2022.pdf#page=12"
abstract: "We present a new tool for the automatic synthesis and verifi-
cation of cryptographic algorithms. Currently the tool considers symbolic
security and invertibility of recursively defined modes of operation with
an xor-operation and encryption. A cryptographic mode of operation is
an algorithm for encrypting a message of arbitrary length using a block
cipher that only encrypts messages of a single fixed length. The system
can both automatically generate modes and accept user-defined ones.
These modes can then be checked for properties such as security and
invertibility. In order to analyze the modes, the tool utilizes term rewrit-
ing and unification methods which are implemented in a core supporting
library. The state of the tool and underlying library are in an initial iter-
ation. The goal is to continue expanding the tool to consider additional
security questions and cryptosystems."
---