Go home now Header Background Image
Submission Procedure
share: |
Follow us
Volume 20 / Issue 2

available in:   PDF (192 kB) PS (270 kB)
Similar Docs BibTeX   Write a comment
Links into Future
DOI:   10.3217/jucs-020-02-0193


Towards Formal Linear Cryptanalysis using HOL4

Osman Hasan (University of Sciences and Technology (NUST), Pakistan)

Syed Ali Khayam (University of Sciences and Technology (NUST), Pakistan)

Abstract: 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.

Keywords: cryptography, formal verification, higher-order logic, probability theory, theorem proving