http://iet.metastore.ingenta.com
1887

CryptoSAT: a tool for SAT-based cryptanalysis

CryptoSAT: a tool for SAT-based cryptanalysis

For access to this article, please select a purchase option:

Buy article PDF
£12.50
(plus tax if applicable)
Buy Knowledge Pack
10 articles for £75.00
(plus taxes if applicable)

IET members benefit from discounts to all IET publications and free access to E&T Magazine. If you are an IET member, log in to your account and the discounts will automatically be applied.

Learn more about IET membership 

Recommend Title Publication to library

You must fill out fields marked with: *

Librarian details
Name:*
Email:*
Your details
Name:*
Email:*
Department:*
Why are you recommending this title?
Select reason:
 
 
 
 
 
IET Information Security — Recommend this title to your library

Thank you

Your recommendation has been sent to your librarian.

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.

References

    1. 1)
      • 1. Massacci, F., Marraro, L.: ‘Logical cryptanalysis as a SAT problem’, J. Autom. Reason., 2000, 24, (1–2), pp. 165203.
    2. 2)
      • 2. Ihaka, R., Gentleman, R.: ‘A language for data analysis and graphics’, J. Comput. Graph. Stat., 1996, 5, (3), pp. 299314.
    3. 3)
      • 3. Ripley, B.D.: ‘The R project in statistical computing. MSOR connections’, Newsl. LTSN Maths, Stats OR Netw., 2001, 1, (1), pp. 2325.
    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)
      • 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. 102115.
    6. 6)
      • 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. 377382.
    7. 7)
      • 7. Jovanović, D., Janičić, P.: ‘Logical analysis of hash functions’. Frontiers of Combining Systems, Vienna, Austria, September 19–21, 2005 (LNCS, 3717), pp. 200215.
    8. 8)
      • 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.
    9. 9)
      • 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. 131144.
    10. 10)
      • 10. Janičić, P.: ‘Uniform reduction to SAT’, Logical Methods Comput. Sci., 2010, 8, (3), pp. 139.
    11. 11)
      • 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.
    12. 12)
      • 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.
    13. 13)
      • 13. Morawiecki, P., Srebrny, M.: ‘A SAT-based preimage analysis of reduced Keccak hash functions’, Inf. Process. Lett., 2013, 113, (10–11), pp. 392397.
    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. 5667.
    15. 15)
      • 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.
    16. 16)
      • 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. 161185.
    17. 17)
      • 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.
    18. 18)
      • 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. 306324.
    19. 19)
      • 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. 371387.
    20. 20)
      • 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. 379394.
    21. 21)
      • 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. 2436.
    22. 22)
      • 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. 128157.
    23. 23)
      • 23. Lafitte, F., Markowitch, O., Van Heule, D.: ‘SAT based analysis of LTE stream cipher ZUC’, J. Inf. Sec. Appl., 2015, 22, (C), pp. 5465.
    24. 24)
      • 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. 363366.
    25. 25)
      • 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.
    26. 26)
      • 26. Soos, M.: CryptoMiniSat 2.5.0. SAT Race competitive event booklet, July 2010.
    27. 27)
      • 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.
    28. 28)
      • 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/.
    29. 29)
      • 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. 125.
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
This is a required field
Please enter a valid email address