Verified Post-Quantum Cryptography

Last updated: 2022/04/26 This is both a TODO list and a record of work that I've done on this project.

Weekly Status 04/29

• Finished report draft due 04/25.
• Finished report due 04/28.
• Recorded poster presentation audio due 04/28.
• Submitted final project artifacts due 04/28. This includes the poster, 5 minute audio recording, and the final report.

Weekly Status 04/22

• Finished poster final due 04/27.
• Worked on report draft due 04/25. I'll be finishing this over the weekend.

Weekly Status 04/15

• Finished poster draft due 04/10.
• Poster presentation in class on 04/14.

Weekly Status 04/08

• Verified termination of EEA. LiquidHaskell is smarter than I thought and what I was missing is that the remainder is only decreasing when the numerator is larger than the denominator, i.e.:

  if a > b then (a % b) < b

  I added a refinement checking this to my EEA implementation and with a few other changes was able to get verification to work.
  
  I think I found a bug in either LiquidHaskell or Z3; sometimes when I run verification it takes longer than expected and if I cancel it and restart it runs quickly. I know the problem is something to do with my EEA implementation because it started after I verified it. Upgrading to the latest version of Z3 seems to resolve the issue (4.8.5 -> 4.8.15).

Weekly Status 04/01

• Implemented Niederreiter version of McEliece. This is verified using refinement types although there are a few things that could be improved, e.g. textbook EEA and GF2 reduction are not verified to terminate and avoiding division by zero is handled awkwardly instead of (ideally) being checked by the type system.
  • Goppa.hs
  • McElieceNiederreiter.hs
  • Everything else
  
  Matthias Minihold's thesis was a great help here; I was able to implement Patterson's algorithm pretty much directly from Risse's paper using the modified EEA from Minihold.
• Briefed milestone 3 slides in class on 03/29.

Weekly Status 03/25

• Found another paper on implementing McEliece in SAGE. This paper includes code as well as sample output which is nice. I copied the code from the paper into a SAGE notebook and got it working. The author implemented both algorithms with random keys and messages; unfortunately I found that the Niederreiter implementation fails for some messages and I'm not sure why.
• Went back to David Hu's Python implementation of McEliece/Niederreiter in SAGE. This uses Patterson's algorithm as described in Risse's paper. Risse doesn't adequately explain how to find alpha/beta to compute the error locator polynomial (there are two versions of the paper, one which omits it and one which has something that doesn't work). Roering's paper uses something that looks like LLL basis reduction to find alpha/beta but this is complicated.
• Implemented Patterson's algorithm using the modified EEA from Minihold's paper (i.e. the new paper mentioned earlier). This is working for both McEliece and Niederreiter and does not seem to be failing for some inputs like Minihold's full implementation was.
• Still some cleanup work for Niederreiter; need to convert from syndrome bit bector to polynomial and verify everything with refinement types.

Weekly Status 03/18

• Finished verifying polynomial/field implementation. Termination of EEA and GF2 reduction is unverified, I will revisit this later in the project. In particular I would like to verify EEA because it seems like an interesting problem; essentially I will have to show that at least one of the parameters is always decreasing such that termination can be shown inductively.
• Implemented "half"-GCD that matches the output of David Hu's Python implementation of Goppa McEliece. This is EEA except we return early when the second Bezout coefficient is of degree t/2. This should work for larger Goppa codes now whereas the unmodified EEA would return an invalid error-locator polynomial.
• Researched Niederrieter version of Mceliece. Looks straightforward based on what I've already implemented. I will create a similar file to McElieceGoppa walking through encryption/decryption with Niederrieter next.

Weekly Status 03/11

• Partially verified polynomial implementation. Determined that tracking polynomial degree in the type system was unnecessary. Current pain points are verifying that division is never called with a zero denominator and verifying that EEA terminates.

Weekly Status 03/04

• Implemented Goppa code version of McEliece. This is a toy example and NOT YET completely verified. Relevant code is available below; I included doctests in the comments so you can see what the output is after each step.
  • Number.hs (EEA from previous crypto assignment)
  • Polynomial.hs
  • GaloisField.hs
  • McElieceGoppa.hs
  • Everything else
  
  Things on my radar to verify are tracking the degree of polynomials (bounds checks) and tracking that field elements belong to the same field during operations. There is also still some optimization to do as the polynomial operations are slower than would be expected for this example. Finally, computing the generator matrix from the Goppa polynomial still needs to be done; the current example is from a book and reproduced in Sage but I would like to be able to compute everything from as few inputs as possible.
  
  The main challenge and the reason why this isn't completely verified is that I had a lot of theory to cover regarding Goppa codes and my initial approach to verifying polynomials ended up being more complicated than expected.
  
  Goppa code encoding/decoding is from several sources.
  • The current "toy" example code is from chapter 12 of The Theory Of Error Correcting Codes by Macwilliams and Sloane.
  • The decoding process is from How Sage Helps To Implement Goppa Codes And The McEliece Public Key Crypto System by Risse with specifics from Coding Theory-Based Cryptography: McEliece Cryptosystems In Sage by Roering.
  • The observation that EEA can be used to decode Goppa codes (with some caveats) is due to David J.W. HU in Code Based Cryptography in Python.
  • The observation that finding polynomial inverse can be done with EEA with an extra operation at the end is due to Juan Grados in Ejemplo Criptosistema McEliece en SAGE and Henri Cohen in chapter 3 of A Course in Computational Algebraic Number Theory.
  
  
• Wrote outline of final report.
• Briefed milestone 2 slides in class on 03/01. See extended slides for more detail.

Weekly Status 02/25

• Wrote abstract/introduction of final report. We reviewed these in class on 02/24 and they are due via drop-box submission on 02/28.
• Prototyped Goppa code decoding in SAGE following RISSE and related papers. SAGE notebook is available here.
  
  I discovered that I'm going to have to implement both finite fields and polynomial arithmetic to be able decode Goppa codes. I found a useful paper on implementing these in C++. I have started working on this.
  
  The steps to decoding a Goppa coded message are:
  1. Generate the syndrome polynomial. This requires the code-locater polynomials used when generating the Goppa code.
  2. Perform Patterson's algorithm or a variant of the EEA to find the error-locater polynomial.
  3. Plug the code-locater polynomials into the error-locater polynomial. (These correspond to the bit positions in the codeword.) If the result is zero then that bit needs to be flipped. This corrects the errors and the message to be decoded.
  
  For this milestone I will be implementing the EEA method since it is simpler. The downside to using EEA is that it can only correct up to t/2 errors compared to Patterson's method, but for the goals of the project that will suffice.

Weekly Status 02/18

• Implemented matrix inversion routine. Routine is as follows:
  1. Work on a pair of matrices, the input square matrix M and an identity matrix of the same dimensions. Do all tests on the input matrix but perform row swap/sum operations on both in tandem.
  2. Iterate through each row and column of the matrix starting in the upper-left.
  3. Find row that has 1 in the current column position and swap with it.
  4. Find other rows that have 1 in the current column position and add the current rows to those; note mod 2 so this should set all other 1s to 0, also note that we must skip the current row otherwise we'd get a null matrix!
  5. When done, check if the input matrix was transformed into an identity matrix. If it was then the other matrix (originally identity) is now our inverse; return it. Otherwise we were unable to find an inverse and return nothing.
• McEliece implementation now computes the generator matrix from the parity matrix and the inverses of the scrambler/permutation matrices instead of hardcoding them. Note that previously I had computed the parity matrix from the generator (by hand) instead; for Hamming it doesn't matter, the examples I've seen seem to start with the generator matrix, but for Goppa codes everything I've seen starts with the parity matrix instead so making that change now seemed appropriate.
• Found paper on implementing Goppa code encoding/decoding in SAGE (another system like GAP); going to attempt to port this to LiquidHaskell.

Weekly Status 02/11

• Researched Goppa codes.
  
  I reviewed some of my older crypto assignments on Galois fields. I've been reading about Goppa codes from a few different sources but still need to work through one by hand; it took me awhile to find a good source on these (see Chapter 8 in The Theory of Error-Correcting Codes); the original work is in Russian.
  
  I found a software package called GAP (Groups, Algorithms, Programming) which supports generating different types of codes and can produce generator and parity check matrices from them.
  
  I'm likely going to use a Goppa matrix generated by GAP so I can focus on Patterson's algorithm for the decryption step; I can revisit generating these later if there is time.

Weekly Status 02/04

• Implemented Hamming code version of McEliece; see the relevant code below. I included doctests in the comments so you can see what the output is after most steps.
  • Matrix.hs
  • Coding.hs
  • McElieceHamming.hs
  • Everything else
  
  This is fully verified with refinement types. I did not implement key generation yet so the example is using hardcoded values. Key generation consists of generating random matrices (easy) and calculating their inverses (hard); I will be working on this next.
  
  I was able to make good progress writing this in LiquidHaskell, but I had to implement matrix code on my own (following one of the LH tutorials). Haskell has a generic matrix package but there are no refinement types specified for it yet and creating them would be out of scope for this project. This was a consistent problem while working on this. I believe the issue was that I am working with size-aware types, so every refinement needs to preserve sizes on input/output (e.g. a function that copies a list of size N produces a list of size N). On the other hand having to reimplement this helped me learn about how refinements work.
  
  Something interesting that happened after I had written the matrix code was that I realized it needed to be mod 2, so I created a Bit type (with values 0/1) and was able to swap it in for Int to get my calculations working correctly because all of the matrix code I wrote is generic. This was pretty seamless with LH.
  
  I spent at least half my time working on refinement types to get code to compile. Errors caught by refinements included off-by-one errors and wrong matrix dimensions (i.e. I was trying to multiply something by a matrix but should have been using its transpose).
• Briefed milestone 1 slides in class on 2022/02/03.

Weekly Status 01/28

• Reviewed McEliece cryptosystem.
• Switched to Haskell with LiquidHaskell which has refinement types (main tool for verification) similar to FStar.

Weekly Status 01/21

• Setup project page with description and milestones.
• Identified initial resources and started reading about McEliece and related things.
• Setup FStar development environment in an Ubuntu VM. I initially tried to get this working in Windows, the FStar site has a download for this, but KreMLin and the OCaml backend both require OCaml and OCaml does not work very well on Windows. At this point I can compile and run the FStar examples so I should be ready to start writing code.
• Briefed project overview in class on Tuesday. See presentations on the project page for the slides.
• Revised milestones based on timeframe.

---

Up