Your browser does not support JavaScript!
http://iet.metastore.ingenta.com
1887

access icon free CryptoSAT: a tool for SAT-based cryptanalysis

© The Institution of Engineering and Technology
Received 20/04/2017, Accepted 21/03/2018, Revised 16/01/2018, Published 04/04/2018

The security of symmetric key primitives comes from their exposure to public scrutiny in the context of competitions such as Advanced Encryption Standard, Secure Hash Algorithm 3, or currently CAESAR. However, due to the increasing number of primitives subjected to these competitions, the quality of the scrutiny relies on the availability of automated tools. Although SAT solvers have already proved useful for the automated analysis of these primitives, there is a lack of practical software tools for this purpose. This study describes a framework that aims to make SAT-based analyses accessible to cryptographers. The framework is implemented in a free open-source tool called CryptoSAT which is available in the public domain.

Inspec keywords: cryptography; software tools; computability; public domain software

Other keywords: SAT solvers; public domain; advanced encryption standard; symmetric key primitives; automated tools; free open-source tool; competitions; public scrutiny; SAT-based cryptanalysis; CAESAR; CryptoSAT; secure hash algorithm-3; automated analysis; SAT-based analysis

Subjects: Data security; Programming support; Cryptography; Formal logic

References

    1. 1)
      • 2. Ihaka, R., Gentleman, R.: ‘A language for data analysis and graphics’, J. Comput. Graph. Stat., 1996, 5, (3), pp. 299–314.
    2. 2)
      • 26. Soos, M.: CryptoMiniSat 2.5.0. SAT Race competitive event booklet, July 2010.
    3. 3)
      • 17. Mouha, N., Preneel, B.: ‘Towards finding optimal differential characteristics for ARX: application to Salsa20’. Report 2013/328, Cryptology ePrint Archive, 2013. Available at http://eprint.iacr.org/2013/328.
    4. 4)
      • 4. Legendre, F., Dequen, G., Rajecki, M.: ‘Logical reasoning to detect weaknesses about SHA-1 and MD4/5’. Report 2014/239, Cryptology ePrint Archive, 2014. Available athttp://eprint.iacr.org/2014/239.
    5. 5)
      • 16. Kölbl, S., Leander, G., Tiessen, T.: ‘Observations on the SIMON block cipher family’. Advances in Cryptology - CRYPTO 2015 – 35th Annual Cryptology Conf. Proc., Part I, Santa Barbara, CA, USA, 16–20 August 2015 (LNCS, 9215), pp. 161–185.
    6. 6)
      • 1. Massacci, F., Marraro, L.: ‘Logical cryptanalysis as a SAT problem’, J. Autom. Reason., 2000, 24, (1–2), pp. 165–203.
    7. 7)
      • 3. Ripley, B.D.: ‘The R project in statistical computing. MSOR connections’, Newsl. LTSN Maths, Stats OR Netw., 2001, 1, (1), pp. 23–25.
    8. 8)
      • 21. Liu, Y., De Witte, G., Ranea, A., et al: ‘Rotational-XOR cryptanalysis of reduced-round SPECK’, IACR Trans. Symmetric Cryptol., 2017, 2017, (3), pp. 24–36.
    9. 9)
      • 19. Dobraunig, C., Eichlseder, M., Mendel, F., et al: ‘Cryptanalysis of Ascon’. Topics in Cryptology – CT-RSA 2015, The Cryptographer's Track at the RSA Conf. 2015, Proc., San Francisco, CA, USA, April 20–24 2015 (LNCS, 9048), pp. 371–387.
    10. 10)
      • 18. Aumasson, J.P., Jovanovic, P., Neves, S.: ‘Analysis of NORX: investigating differential and rotational properties’. Progress in Cryptology – LATINCRYPT 2014 – Third Int. Conf. on Cryptology and Information Security in Latin America, Florianópolis, Brazil, 17–19 September 2014 (LNCS, 8895) Revised Selected Papers, pp. 306–324.
    11. 11)
      • 13. Morawiecki, P., Srebrny, M.: ‘A SAT-based preimage analysis of reduced Keccak hash functions’, Inf. Process. Lett., 2013, 113, (10–11), pp. 392–397.
    12. 12)
      • 7. Jovanović, D., Janičić, P.: ‘Logical analysis of hash functions’. Frontiers of Combining Systems, Vienna, Austria, September 19–21, 2005 (LNCS, 3717), pp. 200–215.
    13. 13)
      • 22. Sun, L., Wang, W., Wang, M.: ‘Automatic search of bit-based division property for ARX ciphers’. Advances in Cryptology – ASIACRYPT 2017 – 23rd Int. Conf. on the Theory and Applications of Cryptology and Information Security, Proc., Part I, Hong Kong, China, 3–7 December 2017, (LNCS, 10624), pp. 128–157.
    14. 14)
      • 14. Homsirikamol, E., Morawiecki, P., Rogawski, M., et al: ‘Security margin evaluation of SHA-3 contest finalists through SAT-based attacks’. Computer Information Systems and Industrial Management, Venice, Italy, September 26–28, 2012 (LNCS, 7564), pp. 56–67.
    15. 15)
      • 6. De, D., Kumarasubramanian, A., Venkatesan, R.: ‘Inversion attacks on secure hash functions using SAT solvers’. Theory and Applications of Satisfiability Testing – SAT 2007, Lisbon, Portugal, May 28–31, 2007 (LNCS, 4501), pp. 377–382.
    16. 16)
      • 8. Bard, G.V., Courtois, N.T., Jefferson, C.: ‘Efficient methods for conversion and solution of sparse systems of low-degree multivariate polynomials over GF(2) via SAT-solvers’. Report 2007/024, Cryptology ePrint Archive, 2007. Available at http://eprint.iacr.org/2007/024.
    17. 17)
      • 28. Lafitte, F.: ‘Cryptosat: SAT-based attacks on cryptographic algorithms’, 2016. R package version 0.2.1. Available at https://qualsec.ulb.ac.be/people/frederic-lafitte/cryptosat/.
    18. 18)
      • 5. Mironov, I., Zhang, L.: ‘Applications of SAT solvers to cryptanalysis of hash functions’. Theory and Applications of Satisfiability Testing – SAT 2006, Seattle, WA, USA, August 12–15, 2006 (LNCS, 4121), pp. 102–115.
    19. 19)
      • 27. König, T., Jünemann, K., Burger, M.: RUnit – A Unit Test Framework for R, 2007. Vignette of the package RUnit. Available at https://cran.r-project.org/web/packages/RUnit/vignettes/RUnit.pdf.
    20. 20)
      • 24. Wheeler, D.J., Needham, R.M.: ‘TEA, a tiny encryption algorithm’. Fast Software Encryption: Second Int. Workshop Proc., Leuven, Belgium, 14–16 December 1994 (LNCS, 1008), pp. 363–366.
    21. 21)
      • 9. Soos, M.: ‘Grain of salt - an automated way to test stream ciphers through SAT solvers’. ECRYPT Workshop on Tools for Cryptanalysis, ECRYPT, Royal Holloway, University of London, Egham, UK, 22–23 June 2010, pp. 131–144.
    22. 22)
      • 23. Lafitte, F., Markowitch, O., Van Heule, D.: ‘SAT based analysis of LTE stream cipher ZUC’, J. Inf. Sec. Appl., 2015, 22, (C), pp. 54–65.
    23. 23)
      • 12. Morawiecki, P., Srebrny, M.: ‘A SAT-based preimage analysis of reduced KECCAK hash functions’. Report 2010/285, Cryptology ePrint Archive, 2010. Available athttp://eprint.iacr.org/2010/285.
    24. 24)
      • 10. Janičić, P.: ‘Uniform reduction to SAT’, Logical Methods Comput. Sci., 2010, 8, (3), pp. 1–39.
    25. 25)
      • 15. Otpuschennikov, I., Semenov, A., Kochemazov, S.: ‘Transalg: a tool for translating procedural descriptions of discrete functions to SAT (tool paper). CoRR, abs/1405.1544, 2014.
    26. 26)
      • 25. Bengtsson, H.: ‘The R.oo package – object-oriented programming with references using standard R code’. Proc. 3rd Int. Workshop on Distributed Statistical Computing (DSC 2003), Vienna, Austria, March 2003.
    27. 27)
      • 11. Kircanski, A.: ‘Analysis of boomerang differential trails via a SAT-based constraint solver URSA’. Report 2014/563, Cryptology ePrint Archive, 2014. Available athttp://eprint.iacr.org/2014/563.
    28. 28)
      • 29. Lafitte, F., Nakahara, J., Van Heule, D.: ‘Applications of SAT solvers in cryptanalysis: finding weak keys and preimages’, J. Satisfiability, Boolean Modeling Computation, 2014, 9, (1), pp. 1–25.
    29. 29)
      • 20. Song, L., Huang, Z., Yang, Q.: ‘Automatic differential analysis of ARX block ciphers with application to SPECK and LEA’. Information Security and Privacy - 21st Australasian Conf., ACISP 2016, Proc., Part II, Melbourne, VIC, Australia, 4–6 July 2016 (LNCS, 9723), pp. 379–394.
http://iet.metastore.ingenta.com/content/journals/10.1049/iet-ifs.2017.0176
Loading

Related content

content/journals/10.1049/iet-ifs.2017.0176
pub_keyword,iet_inspecKeyword,pub_concept
6
6
Loading
Print this page
This is a required field
Please enter a valid email address