hannes/hannes.robur.coop
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

link to fiat inversion paper

Browse source
This commit is contained in:
Hannes Mehnert 2021-04-27 15:30:58 +02:00
parent d913e784a7
commit ccc4d8973c
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
Posts/EC
View file

@ -37,7 +37,7 @@ In contrast, [*fiat*](https://github.com/mit-plv/fiat-crypto/) is a Coq developm
As mentioned, our initial [fiat-p256](https://github.com/mirage/fiat) binding provided ECDH for the NIST P-256 curve. Also, BoringSSL uses fiat for ECDH, and developed the code for group operations and cryptographic protocol on top of it. As mentioned, our initial [fiat-p256](https://github.com/mirage/fiat) binding provided ECDH for the NIST P-256 curve. Also, BoringSSL uses fiat for ECDH, and developed the code for group operations and cryptographic protocol on top of it.
The work needed was (a) ECDSA support and (b) supporting more curves (let's focus on NIST curves). For ECDSA, the algorithm requires modular arithmetics in the field of the group order (in addition to the prime). We generate these primitives with fiat (named `npYYY_AA`) - that required [a small fix in decoding hex](https://github.com/mit-plv/fiat-crypto/commit/e31a36d5f1b20134e67ccc5339d88f0ff3cb0f86). Fiat also provides inversion [since late October 2020](https://github.com/mit-plv/fiat-crypto/pull/670) - which allowed to reduce our code base taken from BoringSSL. The ECDSA protocol was easy to implement in OCaml using the generated arithmetics. The work needed was (a) ECDSA support and (b) supporting more curves (let's focus on NIST curves). For ECDSA, the algorithm requires modular arithmetics in the field of the group order (in addition to the prime). We generate these primitives with fiat (named `npYYY_AA`) - that required [a small fix in decoding hex](https://github.com/mit-plv/fiat-crypto/commit/e31a36d5f1b20134e67ccc5339d88f0ff3cb0f86). Fiat also provides inversion [since late October 2020](https://github.com/mit-plv/fiat-crypto/pull/670), [paper](https://eprint.iacr.org/2021/549) - which allowed to reduce our code base taken from BoringSSL. The ECDSA protocol was easy to implement in OCaml using the generated arithmetics.
Addressing the issue of more curves was also easy to achieve, the C code (group operations) are macros that are instantiated for each curve - the OCaml code are functors that are applied with each curve description. Addressing the issue of more curves was also easy to achieve, the C code (group operations) are macros that are instantiated for each curve - the OCaml code are functors that are applied with each curve description.