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.