index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Spec
Commit message (
Expand
)
Author
Age
*
Fix changed qualified tactic name
Jason Gross
2017-01-17
*
Add ladderstep_other_assoc
Jason Gross
2017-01-07
*
Add more generic ladderstep
Jason Gross
2017-01-07
*
implement X25519
Andres Erbsen
2016-11-06
*
move B_order_l and prime_q
Andres Erbsen
2016-11-06
*
put EdDSA encoding sign bit at the MSB
Andres Erbsen
2016-11-04
*
Filled in point/scalar encoding definitions.
jadep
2016-10-10
*
Ed25519: add basepoint and prove most EdDSA preconditions
Andres Erbsen
2016-10-10
*
Spec.Ed25519: prove that Curve25519 is an elliptic curve
Andres Erbsen
2016-10-10
*
Spec.Ed25519: fix exponent field modulus
Andres Erbsen
2016-10-10
*
Moved PointEncoding out of Spec
jadep
2016-10-06
*
Fixed a lingering inappropriate use of Logic.eq
jadep
2016-10-06
*
fix 8.4 build
jadep
2016-10-03
*
A couple hotfixes; recent commits somehow broke things
jadep
2016-10-03
*
Wrote proofs necessary to fill in all point-encoding related context variable...
jadep
2016-10-03
*
Ed25519: use Global Instance
Andres Erbsen
2016-10-03
*
Spec: add ed25519
Andres Erbsen
2016-10-03
*
MxDH: do not depend on implicit import of list notations
Andres Erbsen
2016-09-26
*
add Montgomery x-coordinate Diffie-Hellman and Curve25519
Andres Erbsen
2016-09-26
*
alternative signing derivation
Andres Erbsen
2016-09-22
*
Derive EdDSA.verify from equational specification
Andres Erbsen
2016-09-16
*
ModularArithmetic: conversions between [F] and [nat]
Andres Erbsen
2016-09-16
*
Fully qualify [Require]s
Jason Gross
2016-09-08
*
remove eq_dec from Monoid
Andres Erbsen
2016-08-23
*
[cbv beta] in the beginning of Obligation Tactic for 8.5
Andres Erbsen
2016-08-08
*
[F] has its own module now
Andres Erbsen
2016-08-05
*
Refactor ModularArithmetic into Zmod, expand Decidable
Andres Erbsen
2016-08-04
*
compute on [F q]!
Andres Erbsen
2016-07-20
*
remove field_algebra
Andres Erbsen
2016-07-11
*
added proofs about addition chain exponentiation for later use in ModularBase...
jadep
2016-07-10
*
Define the spec of Weierstrass curves (#6)
Jason Gross
2016-07-03
*
scalarmult support; EdDSA.sign produces valid signatures
Andres Erbsen
2016-06-27
*
EdDSA: prove things about spec
Andres Erbsen
2016-06-25
*
EdDSA.Notations: indentation
Andres Erbsen
2016-06-22
*
Fix broken notations (hopefully)
Jason Gross
2016-06-22
*
Handle renaming of NPeano.pow to Nat.pow (#3)
Jason Gross
2016-06-22
*
EdDSA.v: resolve ambiguity based on ed25519.py
Andres Erbsen
2016-06-21
*
Whitespace change
Jason Gross
2016-06-21
*
use Local Obligation Tactic (8.5-compat)
Andres Erbsen
2016-06-21
*
remove trailing whitespace from src/
Andres Erbsen
2016-06-20
*
Remove anything incompatible with new algebraic hierarcy
Andres Erbsen
2016-06-20
*
Merge branch 'field-experiment'
Andres Erbsen
2016-06-20
|
\
|
*
port EdDSA spec
Andres Erbsen
2016-06-20
|
*
move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheorems
Andres Erbsen
2016-06-17
|
*
port edwards curve spec
Andres Erbsen
2016-06-16
*
|
Minor 8.5 changes
Jason Gross
2016-06-10
*
|
More changes for 8.5
Jason Gross
2016-06-10
|
*
before changing SRep from N to F l
Andres Erbsen
2016-05-27
|
/
*
Changed name of Encoding to CanonicalEncoding, and changed notation to match.
jadep
2016-04-29
*
Moved sign_bit definition to Spec.
jadep
2016-04-29
[next]