fiatp256

library fiat_p256

module Fiat_p256

Field operations
These are implemented in Field_element
, which is a binding over p256_{32,64}.h
. These are files extracted from Coq code in this repository.
This module uses Montgomery Modular Multiplication. Instead of storing a number a
, operations are done on aR
where R = 2^{256}.
It is possible to check that these files correspond to the extracted ones in the upstream repository by running dune build @check_vendors
.
These files are part of the trusted computing base. That is, using this package relies on the fact that they implemented the correct algorithms. To go further, one can rerun the extraction process from Coq sources, see #41.
Point operations
Points (see the Point
module) are stored using projective coordinates (X : Y : Z):
 Z=0 corresponds to the point at infinity
 for Z≠0, this corresponds to a point with affine coordinates (X/Z^{2}, Y/Z^{3})
Doubling and addition are implemented as C stubs in p256_stubs.c
using code that comes from BoringSSL, Google's fork of OpenSSL. Fiat code has been design in part to be included in BoringSSL, so this does not require any particular glue code.
Some operations are implemented manually, in particular:
 conversion to affine coordinates, as described above. This relies on a field inversion primitive from BoringSSL, that is exposed in
Field_element
.  point verification (bound checking and making sure that the equation is satisfied).
There is no automated way to check that the BoringSSL part is identical to that in the upstream repository (nor to update it).
Scalar multiplication
Implemented by hand using the Montgomery Powering Ladder.
Instead of branching based on key bits, constanttime selection (as defined in fiat code) is used.
The following references discuss this algorithm:
 Scalarmultiplication algorithms, Peter Schwabe, ECC 2013 Summer School
 Montgomery curves and the Montgomery ladder, Daniel J. Bernstein and Tanja Lange
Key exchange
Key exchange consists in
 validating the public key as described in RFC 8446 §4.2.8.2;
 computing scalar multiplication;
 returning the encoded x coordinate of the result.
This is implemented by hand and checked against common errors using test vectors from project Wycheproof.