Brandon Rozek

Photo of Brandon Rozek

PhD Student @ RPI studying Automated Reasoning in AI and Linux Enthusiast.

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,

Conference: International Workshop on Rewriting Logic and its Applications

Publication Date: 2022/3/14

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.

PDF Link: