Keywords: Interactive Theorem Proving, Proof Mechanisation, Higher Order Logic, Cryptography
Units: 12/24 units
Background
Cryptography is about communication in the presence of an adversary. We will restrict our attention to one particular class of cryptographic algorithm: block cipher.
Currently in the official examples of the HOL theorem prover (HOL4), the following block ciphers are implemented: (there are also implementations of RSA and SHA-1)
- AES
- DES
- IDEA
- MARS
- RC6
- Serpent
- TEA
- Twofish
Research Questions and Tasks
This project is an opportunity for students who wants to learn the HOL4 theorem-proving system and realise an important piece of algorithms in modern cryptography. We want to extend the existing cryptography work in HOL’s examples in both the breadth and depth ways. This will include the following tasks:
- Improve the existing implementaion of block ciphers by adding proofs regarding their safety and other algebra properties.
- Mechanise more block ciphers, such as RC4 (arcfour), RC5 and Blowfish.
- Mechanise more message digest algorithms: MD5 and other variants of SHA algorithm.
- Mechanise at least one compression/decompression algorithm pair, e.g. gzip.
- (for 24 credits/units) Formalise the idea of Differential Cryptanalysis in HOL and prove the correctness of its application to DES (full and variants reduced to certain rounds), with connections to Elementary Probability Theory in HOL4.
The development should follow modern techniques and guidelines for HOL4, e.g. [HOLTutorial] and [HOL4]. Ideally, the project will be submitted to HOL4 official as part of its core theories.
NOTE: The student will get some basic training through a mini course to get familar with interactive theorem proving (ITP) techniques (and HOL4 in particular).
References
- [HOLTutorial] The HOL System LOGIC
- [HOL4] The HOL System DESCRIPTION
- [Katz] Katz, J., Lindell, Y.: Introduction to Modern Cryptography, Third Edition. CRC Press (2020).
- [Knudsen] Knudsen, L.R., Robshaw, M.J.B.: The Block Cipher Companion. Springer Publishing Company, Incorporated, Berlin, Heidelberg (2011).
Requirements:
Basic knowledge of formal logic and lambda-calculus (simple typed); some experiences with interactive theorem provers; basic knowledege of cryptography and block ciphers, etc.