Formal proof of correctness of different ciphers.
Currently for learning purposes.
Forked from https://github.com/JoeyLupo/cryptolib
$ git clone https://github.com/oxarbitrage/cryptolib
$ cd cryptolib
$ leanproject build
-
elgamal.lean - contains the formal specification of the ElGamal public key encryption protocol, and the formal proofs of correctness
-
pke.lean - provides formal definitions for correctness and semantic security of a public key encryption scheme
-
tactics.lean - provides the
bindskip
andbindconst
tactics to help prove equivalences between pmfs -
to_mathlib.lean - includes general lemmas for inclusion into mathlib
-
uniform.lean - defines the uniform distribution over a finite group as a pmf, including the special case of Z_q, the integers modulo q, and provides two useful lemmas regarding uniform probabilities
-
rsa.lean - contains proof of correctness of the RSA public key encryption protocol
-
substitution.lean - contains basic formalization and proof of correctness of different substitution ciphers
-
stream.lean - contains basic formalization and proof of correctness of stream ciphers
-
block.lean - contains basic formalization and proof of correctness of block ciphers
-
feistel.lean - Proof of correctness for feitsel ciphers
-
dlp.lean - Formalization of the discrete logarithm problem
-
galois.lean - Bitwise arithmetic in GF(2^n)
-
otp.lean - One-Time Pad correctness
-
lfsr.lean - Implement a very basic Linear-Feedback Shift Register that can be used as a random number generator.
-
modes.lean - Formalize some modes of operations for block ciphers.
-
salsa20/ - Attempt to formalize salsa20 from the spec. WORK HAS MOVED TO https://github.com/oxarbitrage/salsa20/