Zero-knowledge Type-checker

Papers

• Michael Backes, Martin Grochulla, Cătălin Hriţcu, and Matteo Maffei.  Achieving Security Despite Compromise Using Zero-Knowledge. In 22th IEEE Symposium on Computer Security Foundations (CSF 2009), pages 308-323, IEEE Computer Society Press, July 2009.
  •  Full version that contains all the technical details ; February 2009.

• Michael Backes, Cătălin Hriţcu, and Matteo Maffei.  Type-checking Zero-knowledge. In 15th ACM Conference on Computer and Communications Security (CCS 2008), pages 357-370, ACM Press, October 2008.
  •  Full version that additionally contains all the technical details of the type system, a brief discussion about security despite compromise, and all the proofs; November 2008.

Download Coq Proofs

Formalization and proofs by Cătălin Hriţcu. Copyright 2010-2011. All rights reserved.

•  typing-zk-coq-src-2011-11-13.tar.gz -- Coq sources only, 379 KB.
•  typing-zk-coq-obj-2011-11-13.tar.gz -- Coq sources + proof objects + (bad) generated documentation, 12.8MB.

You can find previous releases of the proofs  here.

Download Type-checker

Implementation by Stefan Lorenz, Kim Pecina, Cătălin Hriţcu, and Thorsten Tarrach.  Apache License, Version 2.0.

•  SVN snapshot;  Changes since release 0.2.0; 13th of November 2011
•  zk-typechecker-0.2.0;  Release Notes; 12th of February 2009.
•  zk-typechecker-0.1.0-ccs;  Release Notes; 2nd of December 2008.

Bug Tracker

Because of a recent spam wave you need to be logged-in to create new tickets. If you need an account or want to report a bug directly please contact catalin.hritcu@….