Implementation

The goal of this document is to describe how the library is implemented.

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²⁵⁶.

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 re-run 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², Y/Z³)

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, constant-time selection (as defined in fiat code) is used.

The following references discuss this algorithm:

• Scalar-multiplication 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.