Functional Correctness Proofs of Encryption Algorithms

This is the homepage of the paper Functional Correctness Proofs of Encryption Algorithms, authored by Jianjun Duan, Joe Hurd, Guodong Li, Scott Owens, Konrad Slind, and Junxing Zhang. The paper has been presented at LPAR 2005. Here's the bibtex reference:

@InProceedings{ciphers:lpar05,
  author =       {J. Duan and J. Hurd and G. Li and S. Owens and K. Slind and J. Zhang},
  title =        {Functional Correctness Proofs of Encryption Algorithms},
  booktitle =    {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2005)},
  month =        {December},
  year =         2005,
  editor =       {G. Sutcliffe and A. Voronkov},
  series =       {Lecture Notes in Artificial Intelligence},
  volume =       3835,
  publisher =    {Springer-Verlag}
 }

Here are Postscript and PDF versions of the paper.

A number of formalizations in the HOL-4 implementation of higher order logic are discussed in the paper. We have collected them here, for your viewing pleasure!

These are a snapshot of the current development; the latest and most up-to-date version is at the Crypto examples directory in the HOL-4 sources. To formally check the proofs, one would download the HOL-4 sources from the CVS repository, build the HOL-4 system (see Chapter 1 of the tutorial for instructions), and run the proof scripts in the above directories.

Konrad Slind (on behalf of the other authors).