Towards Formal Linear Cryptanalysis using HOL4

Linear cryptanalysis (LC), first introduced by Matsui, is one of the most widely used techniques for judging the security of symmetric-key cryptosystems. Traditionally, LC is performed using computer programs that are based on some fundamental probabilistic algorithms and lemmas, which have been validated using paper-and-pencil proof methods. In order to raise the confidence level of LC results, we propose to formally verify its foundational probabilistic algorithms and lemmas in the higher-orderlogic theorem prover HOL4. This kind of infrastructure would also facilitate reasoning about LC properties within the HOL4 theorem prover. As a first step towards the proposed direction, this paper presents the formalization of two foundations of LC, which were initially proposed in Matsui’s seminal paper. Firstly, we formally verify the Piling-up Lemma, which allows us to compute the probability of a block cipher’s linear approximation, given the probabilities of linear approximations of its individual modules. Secondly, we provide a formal probabilistic analysis of Matsui’s algorithm for deciphering information about the unknown bits of a cipher key. In order to illustrate the practical effectiveness and utilization of our formalization, we formally reason about a couple of LC properties.