website/content/paper/2203.01.md

title	authors	date	publish_date	conference	firstpage	lastpage	language	pdf_url	abstract
CryptoSolve: Towards a Tool for the Symbolic Analysis of Cryptographic Algorithms	Dalton Chichester Wei Du Raymond Kauffman Hai Lin Christopher Lynch Andrew M. Marshall Catherine A. Meadows Paliath Narendran Veena Ravishankar Luis Rovira Brandon Rozek	2022-03-14	2022/3/14	International Workshop on Rewriting Logic and its Applications	6	25	English	http://sv.postech.ac.kr/wrla2022/assets/files/pre-proceedings-WRLA2022.pdf#page=12	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.