Automated security proof of SQUARE, LED and CLEFIA using the MILP technique

  • Gabriel Cardoso de Carvalho UFF
  • Tertuliano Souza Neto ABIN
  • Thiago do Rêgo Sousa ABIN


Provable security in cryptography is extremely relevant nowadays, since it is regarded as the basis for the proposal of new ciphers. In that sense, the designers of new ciphers have to find ways to prove that the proposed cipher is secure against the most pertinent forms of attack. Being safe against differential and linear cryptanalysis is still considered the bare minimum standard for any new cipher. In the last decade, a great deal of attention has been given to automated ways of proving the security of ciphers against both forms of attacks, the original one being generating mixed linear integer programs that model the given cipher in such a way that, by solving it, we are able to know the minimum number of rounds necessary for the cipher to be secure. In this paper, we apply this technique in the well known block ciphers LED, SQUARE and CLEFIA, and compare the results with the original security claims.


Bestuzheva, K., Besançon, M., Chen, W.-K., Chmiela, A., Donkiewicz, T., van Doornmalen, J., Eifler, L., Gaul, O., Gamrath, G., Gleixner, A., Gottwald, L., Graczyk, C., Halbig, K., Hoen, A., Hojny, C., van der Hulst, R., Koch, T., Lübbecke, M., Maher, S. J., Matter, F., Mühmer, E., Müller, B., Pfetsch, M. E., Rehfeldt, D., Schlein, S., Schlösser, F., Serrano, F., Shinano, Y., Sofranac, B., Turner, M., Vigerske, S., Wegscheider, F., Wellner, P., Weninger, D., and Witzig, J. (2021). The SCIP Optimization Suite 8.0. Technical report, Optimization Online.

Bogdanov, A. (2011). On unbalanced feistel networks with contracting mds diffusion. Des. Codes Cryptography, (59(1-3)):35–58.

Bogdanov, A., Knudsen, L. R., Leander, G., Paar, C., Poschmann, A., Robshaw, M. J. B., Seurin, Y., and Vikkelsoe, C. (2007). Present: An ultra-lightweight block cipher. In Paillier, P. and Verbauwhede, I., editors, Cryptographic Hardware and Embedded Systems CHES 2007, pages 450–466, Berlin, Heidelberg. Springer Berlin Heidelberg.

Daemen, J. (1995). Cipher and hash function design strategies based on linear and differential cryptanalysis. PhD thesis, Doctoral Dissertation, March 1995, KU Leuven.

Daemen, J., Knudsen, L., and Rijmen, V. (1997). The block cipher square. In Fast Software Encryption: 4th International Workshop, FSE’97 Haifa, Israel, January 20– 22 1997 Proceedings 4, pages 149–165. Springer.

Daemen, J. and Rijmen, V. (2002). The design of Rijndael, volume 2. Springer.

Derbez, P. and Lambin, B. (2022). Fast milp models for division property. IACR Transactions on Symmetric Cryptology, pages 289–321.

Dobraunig, C., Eichlseder, M., and Mendel, F. (2016). Square attack on 7-round kiasu-bc. In Applied Cryptography and Network Security: 14th International Conference, ACNS 2016, Guildford, UK, June 19-22, 2016. Proceedings 14, pages 500–517. Springer.

Fu, K., Wang, M., Guo, Y., Sun, S., and Hu, L. (2016). Milp-based automatic search algorithms for differential and linear trails for speck. In Fast Software Encryption: 23rd International Conference, FSE 2016, Bochum, Germany, March 20-23, 2016, Revised Selected Papers 23, pages 268–288. Springer.

Guo, J., Peyrin, T., Poschmann, A., and Robshaw, M. (2011). The led block cipher. In Cryptographic Hardware and Embedded Systems–CHES 2011: 13th International Workshop, Nara, Japan, September 28–October 1, 2011. Proceedings 13, pages 326– 341. Springer.

Hadipour, H., Nageler, M., and Eichlseder, M. (2022). Throwing boomerangs into feistel structures: Application to clefia, warp, lblock, lblock-s and twine. Cryptology ePrint Archive.

Karthika, S. and Singh, K. (2023). Cryptanalysis of stream cipher lizard using division property and milp based cube attack. Discrete Applied Mathematics, 325:63–78.

Katagi, M. and Moriai, S. (2011). The 128-bit blockcipher clefia. Technical report.

Mironov, I. and Zhang, L. (2006). Applications of sat solvers to cryptanalysis of hash functions. In Theory and Applications of Satisfiability Testing-SAT 2006: 9th International Conference, Seattle, WA, USA, August 12-15, 2006. Proceedings 9, pages 102–115. Springer.

Mouha, N., Wang, Q., Gu, D., and Preneel, B. (2011). Differential and linear cryptanalysis using mixed-integer linear programming. In International Conference on Information Security and Cryptology, pages 57–76. Springer.

Pal, D., Chandratreya, V. P., and Chowdhury, D. R. (2023). Efficient algorithms for modeling sboxes using milp. arXiv preprint arXiv:2306.02642.

Sun, S., Hu, L., Wang, P., Qiao, K., Ma, X., and Song, L. (2014). Automatic security evaluation and (related-key) differential characteristic search: application to simon, present, lblock, des (l) and other bit-oriented block ciphers. In Advances in Cryptology–ASIACRYPT 2014: 20th International Conference on the Theory and Application of Cryptology and Information Security, Kaoshiung, Taiwan, ROC, December 7-11, 2014. Proceedings, Part I 20, pages 158–178. Springer.

Wardhana, D. and Indarjani, S. (2019). Square attack on 4 round midori64. In AIP Conference Proceedings, volume 2168. AIP Publishing.

Watanabe, D. and Kaneko, T. (2007). A construction of light weight panama-like keystream generator. IEICE Technical Report.

Xiang, Z., Zhang, W., Bao, Z., and Lin, D. (2016). Applying milp method to searching integral distinguishers based on division property for 6 lightweight block ciphers. In Advances in Cryptology–ASIACRYPT 2016: 22nd International Conference on the Theory and Application of Cryptology and Information Security, Hanoi, Vietnam, December 4-8, 2016, Proceedings, Part I 22, pages 648–678. Springer.

Zhao, H., Han, G., Wang, L., and Wang, W. (2020). Milp-based differential cryptanalysis on round-reduced midori64. IEEE Access, 8:95888–95896.

Zhou, C., Zhang, W., Ding, T., and Xiang, Z. (2019). Improving the milp-based security evaluation algorithm against differential/linear cryptanalysis using a divide-and-conquer approach. Cryptology ePrint Archive.
CARVALHO, Gabriel Cardoso de; SOUZA NETO, Tertuliano; SOUSA, Thiago do Rêgo. Automated security proof of SQUARE, LED and CLEFIA using the MILP technique. In: SIMPÓSIO BRASILEIRO DE SEGURANÇA DA INFORMAÇÃO E DE SISTEMAS COMPUTACIONAIS (SBSEG), 23. , 2023, Juiz de Fora/MG. Anais [...]. Porto Alegre: Sociedade Brasileira de Computação, 2023 . p. 445-455. DOI: