Converting Symmetric Cryptography to SAT Problems Using Model Checking Tools

• Pedro Carlos da S. Lara CEFET/RJ
• Felipe da R. Henriques CEFET/RJ
• Fábio B. de Oliveira LNCC

DOI: https://doi.org/10.5753/sbseg.2020.19226

Resumo

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.

Referências

Ansótegui, C., Bonet, M. L., Levy, J., and Manyà, F. (2008). Measuring the hardness of sat instances. In Proceedings of the 23rd National Conference on Artificial Intelligence Volume 1, AAAI’08, page 222–228. AAAI Press.

Biere, A., Cimatti, A., Clarke, E. M., Strichman, O., and Zhu, Y. (2003). Bounded model checking.

Bryant, R. E. (1986). Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput., 35(8):677–691.

Burch, J. R., Clarke, E. M., and Long, D. E. (1991). Symbolic model checking with partitioned transition relations. pages 49–58. North-Holland.

Clarke, E. M. and Emerson, E. A. (1982). Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logic of Programs, Workshop, pages 52–71, London, UK, UK. Springer-Verlag.

Courtois, N. and Pieprzyk, J. (2002). Cryptanalysis of block ciphers with overdefined systems of equations. volume 2002, page 44.

Courtois, N. T. (2005). General principles of algebraic attacks and new design criteria for cipher components. In Dobbertin, H., Rijmen, V., and Sowa, A., editors, Advanced Encryption Standard – AES, pages 67–83, Berlin, Heidelberg. Springer Berlin Heidelberg.

Courtois, N. T. and Meier, W. (2003). Algebraic attacks on stream ciphers with linear feedback. In Biham, E., editor, Advances in Cryptology — EUROCRYPT 2003, pages 345–359, Berlin, Heidelberg. Springer Berlin Heidelberg.

Davis, M. and Putnam, H. (1960). A computing procedure for quantification theory. J. ACM, 7(3):201–215.

Eén, N. and Sörensson, N. (2003). An extensible sat-solver. In Giunchiglia, E. and Tacchella, A., editors, SAT, volume 2919 of Lecture Notes in Computer Science, pages 502–518. Springer.

Given-Wilson, T., Jafri, N., Lanet, J. L., and Legay, A. (2017). An automated formal process for detecting fault injection vulnerabilities in binaries and case study on present. In 2017 IEEE Trustcom/BigDataSE/ICESS, pages 293–300.

Horbach, A., Bartsch, T., and Briskorn, D. (2012). Using a satsolver to schedule sports leagues. J. Scheduling, 15:117–125.

Jovanovic, P. (2010). Algebraic attacks using sat-solvers. Groups Complexity Cryptology, 2:247–259.

Kroening, D. and Tautschnig, M. (2014). CBMC – C Bounded Model Checker, pages 389–391. Springer Berlin Heidelberg, Berlin, Heidelberg.

Mohamed, M. S. E., Ding, J., Buchmann, J., and Werner, F. (2009). Algebraic attack on the mqq public key cryptosystem. In Garay, J. A., Miyaji, A., and Otsuka, A., editors, Cryptology and Network Security, pages 392–401, Berlin, Heidelberg. Springer Berlin Heidelberg.

Nudelman, E., Leyton-Brown, K., Hoos, H. H., Devkar, A., and Shoham, Y. (2004). Understanding random sat: Beyond the clauses-to-variables ratio. In Wallace, M., editor, Principles and Practice of Constraint Programming – CP 2004, pages 438–452, Berlin, Heidelberg. Springer Berlin Heidelberg.

Patarin, J. (1995). Cryptanalysis of the matsumoto and imai public key In Coppersmith, D., editor, Advances in Cryptology — scheme of eurocrypt’88. CRYPT0’ 95, pages 248–261, Berlin, Heidelberg. Springer Berlin Heidelberg.

Samer, M. and Szeider, S. (2010). Algorithms for propositional model counting. Journal of Discrete Algorithms, 8(1):50 – 64.

Samer, M. and Veith, H. (2009). Encoding treewidth into sat. In Kullmann, O., editor, Theory and Applications of Satisfiability Testing SAT 2009, pages 45–50, Berlin, Heidelberg. Springer Berlin Heidelberg.

Soos, M., Nohl, K., and Castelluccia, C. (2009). Extending SAT solvers to cryptographic problems. In Kullmann, O., editor, Theory and Applications of Satisfiability Testing SAT 2009, 12th International Conference, SAT 2009, Swansea, UK, June 30 July 3, 2009. Proceedings, volume 5584 of Lecture Notes in Computer Science, pages 244–257. Springer.

Tarjan, R. (1972). Depth first search and linear graph algorithms. SIAM JOURNAL ON COMPUTING, 1(2).