JUCS - Journal of Universal Computer Science 20(2): 193-212, doi: 10.3217/jucs-020-02-0193
Towards Formal Linear Cryptanalysis using HOL4
expand article infoOsman Hasan, Syed Ali Khayam
‡ University of Sciences and Technology (NUST), Islamabad, Pakistan
Open Access
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.
formal verification, higher-order logic, probability theory, cryptography, theorem proving