Converting Symmetric Cryptography to SAT Problems Using Model Checking Tools - Lara, Pedro Carlos da S.; Henriques, Felipe da R.; Oliveira, Fábio B. de (Anais do Simpósio Brasileiro de Cibersegurança (SBSeg), 2020)
Algebraic attack is a recent technique used to break symmetric cryptography including Crypto-1, which is used in smart NFC cards around the world. The main method is to convert a cryptography algorithm to a system of equations over a finite field, to translate it into a SAT problem and to use a good solver. The main advantage of converting cryptography problems into SAT is that we can use a lot of well know tools for SAT solving and test it in an instance. However, the high degree labor intensiveness on converting cryptography to SAT instances is a difficult task for advancement of research. To pursue this problem, this work presents a technique to quickly translate symmetric cryptography into SAT problems using Bounded Model Checking (BMC) tools. Computational experiments are performed, converting the RC4 and AES algorithms into a SAT problem.