From ccc4d8973cf51629b47fe8d31ac63ec84bd81d30 Mon Sep 17 00:00:00 2001 From: Hannes Mehnert Date: Tue, 27 Apr 2021 15:30:58 +0200 Subject: [PATCH] link to fiat inversion paper --- Posts/EC | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Posts/EC b/Posts/EC index b8ba873..56fa70d 100644 --- a/Posts/EC +++ b/Posts/EC @@ -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. -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.