Automated security proof of SQUARE, LED and CLEFIA using the MILP technique
Gabriel Cardoso de Carvalho, Tertuliano Souza Neto, Thiago do Rêgo Sousa · 2023
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.