Cryptographic Constructions in the Type Theory of Agda
Agda Other
Pull request Compare This branch is 704 commits ahead of np:master.
Latest commit 9b76349 Aug 8, 2015 @np np ZK.JSChecker.Proof: Fix imports
Permalink
Failed to load latest commit information.
Attack Mainly renamings and re-org around the notion of Pubkey-encryption May 1, 2015
Composition with/out-K (some modules might break) Jul 10, 2013
Control Various minor updates/fixes Apr 13, 2015
Crypto Lamport: +extract-signkey +extract-signkey-correct Jul 7, 2015
ECC Extract ECC/ecc as Algebra.DoubleAndAdd in agda-nplib Jun 22, 2015
FiniteField ZK.JSChecker: Re-org, update and improve Jun 16, 2015
FunUniverse circuit May 2, 2015
Game Mainly renamings and re-org around the notion of Pubkey-encryption May 1, 2015
Language/Simple More fixes Apr 13, 2015
Solver Solver.Linear: experiment with a new parser implem May 10, 2015
ZK ZK.JSChecker.Proof: Fix imports Aug 8, 2015
alea More fixes Apr 13, 2015
bijection-syntax bijection-syntax: fix May 2, 2015
circuits More fixes Apr 13, 2015
experimental renaming Jul 4, 2015
gup A big bag of changes which stayed too long uncommitted... Feb 5, 2015
misc A big bag of changes which stayed too long uncommitted... Feb 5, 2015
poster A big bag of changes which stayed too long uncommitted... Feb 5, 2015
test-election-2 JSChecker: some progress, still experimental Apr 27, 2015
.dockerignore More .dockerignore patterns Apr 14, 2015
.gitattributes A big bag of changes which stayed too long uncommitted... Feb 5, 2015
.gitignore Add ZK.PartialHeliosVerifier which runs on real data! Feb 10, 2015
Dockerfile Dockerfile: success Apr 14, 2015
Helios.agda A big bag of changes which stayed too long uncommitted... Feb 5, 2015
LICENSE LICENSE Sep 22, 2014
Negligible.agda Negligible: some renamings to follows nplib, the name was almost pref… Mar 23, 2015
README Added Gitter link May 7, 2015
README.agda Move Cipher.* to Crypto.Cipher.* May 2, 2015
SynGrp.agda SynGrp: updated but not used anymore so far Jul 4, 2015
adder.agda adder: use mapAccum Jul 16, 2013
agda-pkg.conf agda-pkg: add a missing dep Apr 13, 2015
crypto-agda.agda crypto-agda: disable the import of the forking-lemma Jun 16, 2015
cycle-id.agda cycle-id.agda Feb 26, 2015
cycle.agda Changes in cycle.agda and cycle3.agda Feb 26, 2015
cycle3.agda Changes in cycle.agda and cycle3.agda Feb 26, 2015
cyclic10.agda cyclic10.agda Apr 22, 2015
forking-lemma.agda forking-lemma: minor progress May 27, 2015
hash-param.agda bijection-syntax: rework May 2, 2015
probas.agda forking-lemma: minor progress May 27, 2015
rewind-on-success.agda rewind-on-success May 2, 2015
runjs.sh ZK.JSChecker: Re-org, update and improve Jun 16, 2015
sha1.agda sha1... May 2, 2015
verifier-input-to-single-chaum-proofs.jq Tests Apr 23, 2015

README

The HTML highlighted version (not necessarily up to date):
  * http://crypto-agda.github.io/crypto-agda/html/README.html

  Otherwise, a good starting point is README.agda

This development is based on two other sub-projects:
  * https://github.com/crypto-agda/protocols

    Dependent protocols for communication

  * https://github.com/crypto-agda/explore

    Big operators as exploration functions in Agda

  * https://github.com/crypto-agda/agda-nplib

    An extension of Agda standard library

Join the chat at https://gitter.im/crypto-agda/crypto-agda