Remove duplicated versions of ECDSA and ECs

[marsella]

At time of writing there are 4 implementations of the NIST prime field elliptic curves and 3 implementations of ECDSA. This is redundant and we should remove the ones that don't meet our gold standards.

Right now the closest to gold standard are the versions added in #99 and #96. We should carefully review the other versions to see if there are useful things contained in them. If possible, we should port those things to the standard versions. If not, document what we want to keep in this issue.

• [x] Review Z-type ECDSA + curve implementations
• [x] Review integer version of ECDSA
• [x] Review the one-file standalone version of EC
• [x] Review the other EC version
• [x] Update the EC and ECDSA READMEs to reflect which versions were deleted.

[marsella]

Primitive/Asymmetric/Signature/ECDSA/ECDSA.cry + friends The Z-type ECDSA implementation has two things that are not included in the new version:

• Custom mp_mod_sqrt implementations for each curve like this for 224
• Compression and decompression algorithms plus test vectors and some related properties

I'm pretty sure everything else, including tests, properties, implementations, etc. are ported to the PFEC implementation. It's not used anywhere else in the repo.

[marsella]

Common/EC/EC_P384.cry The one-file standalone version of EC actually has some ECDSA tucked in there as well. Most of the EC operations are undefined. It uses Integers to represent field elements and scalar values. The only thing I didn't recognize were the mont_R family of functions but they don't look very complicated so if we figure out what they are I think we can rewrite them.

There is a bit of naming overlap with Signature/ecdsa.cry. This is not used anywhere else in the repo.

[marsella]

• ref_ec_mul.cry: This has scalar multiplication and twin multiplication for the prime curves from MATH-2008
• p384_field.cry: I think this implements field operations over bit vectors. I'm guessing this is superseded by the integer mod type Z p existing at all, unless it's here because it's optimized for proving stuff (bit vectors perhaps being faster to prove over compared to Z).
• p384_ec_mul.cry: This looks like multiplication and twin mult optimized to match some Java implementation. To be honest I find this pretty inscrutable without any documentation or references to compare it to, so I can't really explain what it's doing or why it's different from the other version.
• ec_point_ops.cry: add, sub, and double routines for the prime curves from MATH-2008
• p384_ec_point_ops.cry: This is just point ops with the p384 moduli passed in

These are all used among each other and in Primitive/Asymmetric/Signature/ecdsa.cry. I did not find any other uses in this repo.

[marsella]

Primitive/Asymmetric/Signature/ecdsa.cry This is the usual ECDSA implementation, plus the test vectors from MATH-2008, plus a version of signing that looks like some Java implementation.

I think the only part that's not duplicated in PFEC is the Java imperative version. I don't know what the actual Java library is, though, and there isn't an equivalence property between the reference and the imperative version.

[kiniry]

The pointers I just gave you to Joe Hendrix's prior work will point you to exactly which version of BouncyCastle he formally verified, @marsella.

[marsella]

Thanks Joe. Collecting some notes here:

• I found an article from Galois about verifying ECC.
• There's an example in the saw-script repo with a specific Java implementation and a clone (I haven't verified line-by-line but it's the same file names) of the Hendrix version of EC/ECDSA in this repo. I haven't tried running it to see if it works yet. There are several TODOs and FIXMEs in the SAW proof.
• I haven't found any documentation about verifying bouncycastle. There are some BC release versions in HACrypto but I can't tell from that repo what they were used for.