Add EdDSA, EcDSA + benchmarks and some other improvments

2022-01-24 11:23:25 +01:00
parent e0ab81c99d
commit 3cee7296b2
8 changed files with 409 additions and 20 deletions
@@ -99,18 +99,28 @@ prop_scalar_mul_noclamp() ->
    equals(E, ecu_ed25519:compress(P))
  end).

-xprop_scalar_enacl() ->
-  ?FORALL(S, gen_scalar(),
+prop_arithmetics1() ->
+  ?FORALL({P1, P2, P3}, {gen_point(), gen_point(), gen_point()},
  begin
-    _P = enacl:crypto_ed25519_scalarmult_base(S),
-    true
+    Res1 = ecu_ed25519:p_add(P1, ecu_ed25519:p_add(P2, P3)),
+    Res2 = ecu_ed25519:p_add(ecu_ed25519:p_add(P1, P2), P3),
+    equal_pts(Res1, Res2)
  end).

-xprop_scalar_ecu() ->
-  ?FORALL(S, gen_scalar(),
+prop_arithmetics2() ->
+  ?FORALL({P1, P2}, {gen_point(), gen_point()},
  begin
-    _P = ecu_ed25519:scalar_mul_base(S),
-    true
+    Res1 = ecu_ed25519:p_sub(ecu_ed25519:p_add(P1, P2), P2),
+    equal_pts(P1, Res1)
+  end).
+
+prop_dbl() ->
+  ?FORALL(P, gen_point(),
+  begin
+    A = ecu_ed25519:p_add(P, P),
+    B = ecu_ed25519:p_dbl(P),
+    ?WHENFAIL(eqc:format("~p\n  /=\n~p\n", [ecu_ed25519:to_affine(A), ecu_ed25519:to_affine(B)]),
+              ecu_ed25519:pt_eq(A, B))
  end).

 even(<<B:31/bytes, _:1, B2:7>>) -> <<B/bytes, 0:1, B2:7>>.
@@ -0,0 +1,70 @@
+%%% Author      : Hans Svensson
+%%% Description :
+%%% Created     : 19 Jan 2022 by Hans Svensson
+-module(eddsa_eqc).
+
+-compile([export_all, nowarn_export_all]).
+
+-include_lib("eqc/include/eqc.hrl").
+
+%% Let's use enacl/libsodium as the oracle
+-define(N, 16#1000000000000000000000000000000014DEF9DEA2F79CD65812631A5CF5D3ED).
+
+-define(KP, #{public => <<161,254,128,151,126,253,139,99,47,29,229,140,67,224,50,78,70,156,225,182,242,171,89,114,47,163,254,192,59,35,148,234>>, secret => <<102,73,74,74,245,130,53,139,149,247,67,138,211,86,72,227,20,43,6,39,134,133,215,10,3,159,123,152,144,208,176,138,161,254,128,151,126,253,139,99,47,29,229,140,67,224,50,78,70,156,225,182,242,171,89,114,47,163,254,192,59,35,148,234>>}).
+
+
+gen_large_n() ->
+  ?LET(<<X:512>>, binary(64), 1 + (X rem (?N - 1))).
+
+gen_scalar() ->
+  ?LET(N, gen_large_n(), <<N:256/little>>).
+
+gen_point() ->
+  ?LET(S, gen_scalar(), enacl:crypto_ed25519_scalarmult_base_noclamp(S)).
+
+prop_keypair_seed() ->
+  ?FORALL(Seed, binary(32),
+  begin
+    KP1 = enacl:sign_seed_keypair(Seed),
+    KP2 = ecu_eddsa:sign_seed_keypair(Seed),
+    equals(KP1, KP2)
+  end).
+
+prop_sign() ->
+  ?FORALL({Priv, Msg}, {binary(32), binary(48)},
+  begin
+    #{secret := SK} = enacl:sign_seed_keypair(Priv),
+    Sig1 = enacl:sign(Msg, SK),
+    Sig2 = ecu_eddsa:sign(Msg, SK),
+    equals(Sig1, Sig2)
+  end).
+
+prop_sign_open() ->
+  ?FORALL({Priv, Msg}, {noshrink(binary(32)), noshrink(binary(48))},
+  begin
+    #{secret := SK, public := Pub} = enacl:sign_seed_keypair(Priv),
+    Sig = enacl:sign(Msg, SK),
+    Res1 = enacl:sign_open(Sig, Pub),
+    Res2 = ecu_eddsa:sign_open(Sig, Pub),
+    equals(Res1, Res2)
+  end).
+
+prop_sign_detached() ->
+  ?FORALL({Priv, Msg}, {binary(32), binary(48)},
+  begin
+    #{secret := SK} = enacl:sign_seed_keypair(Priv),
+    Sig1 = enacl:sign_detached(Msg, SK),
+    Sig2 = ecu_eddsa:sign_detached(Msg, SK),
+    equals(Sig1, Sig2)
+  end).
+
+prop_sign_verify_detached() ->
+  ?FORALL({Priv, Msg}, {noshrink(binary(32)), noshrink(binary(48))},
+  begin
+    #{secret := SK, public := Pub} = enacl:sign_seed_keypair(Priv),
+    Sig = enacl:sign_detached(Msg, SK),
+    Res1 = enacl:sign_verify_detached(Sig, Msg, Pub),
+    Res2 = ecu_eddsa:sign_verify_detached(Sig, Msg, Pub),
+    equals(Res1, Res2)
+  end).
+