aboutsummaryrefslogtreecommitdiff
path: root/src/Galois/EdDSA.v
Commit message (Expand)AuthorAge
* Finish seperating our specs: remove old non-specified codeGravatar Andres Erbsen2016-02-15
* PointFOrmats,EdDSA: remove redundant axiomsGravatar Andres Erbsen2016-01-16
* simple refactor of makefile; commentsGravatar varomodt2016-01-09
* PointFormats/EdDSA: scoping tweaks in PointFormats, small changes of phrasing...Gravatar Jade Philipoom2016-01-05
* Code-reviewing EdDSAGravatar Adam Chlipala2015-12-29
* PointFormats: wrote and proved equivalent a double-and-add implementation of ...Gravatar Jade Philipoom2015-12-20
* EdDSA: prettification of proofs; parameter l is now a nat instead of a Prime.Gravatar Jade Philipoom2015-12-17
* EdDSA: Proved verify_valid_passes and rewrote spec in terms of encoding typec...Gravatar Jade Philipoom2015-12-17
* rename fields for encodingsGravatar Andres Erbsen2015-12-15
* EdDSA: point encoding is a parameterGravatar Andres Erbsen2015-12-15
* PointFormats: all Edwards25519 points are onCurveGravatar Andres Erbsen2015-12-15
* another pass over the eddsa specGravatar Andres Erbsen2015-12-15
* EdDSA: mostly-complete spec and preliminary structure.Gravatar Jade Philipoom2015-12-12
* More improved structure for EdDSA and PointFormats.Gravatar Jade Philipoom2015-12-10
* Rewrote PointFormats to be parameterized by modulus; reformatting of EdDSA.Gravatar Jade Philipoom2015-12-09
* EdDSA: Added PointFormatsSpec module type (possibly temporary). Transcribed p...Gravatar Jade Philipoom2015-12-07
* Transcribed EdDSA parameters from [https://eprint.iacr.org/2015/677.pdf].Gravatar Jade Philipoom2015-12-07