- 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.
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.
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@….