Skip to content

Commit 2ba6d43

Browse files
ansiwenansiwen
committed
mirage-crypto-ec: implementation of SECP256K1
This change implements the SECP256K1 curve (also known as the Bitcoin curve). - field primitives are generated by the fiat-crypto project[1] - point primitives are generated by the ECCKiila project[2] - Ocaml point operations are taken from NIST implementation, adapted to ECCKiila point primitives and optimized for a=0. - testvectors for ECDH and ECDSA verification from wycheproof[3] Closes: mirage#187 [1] https://github.com/mit-plv/fiat-crypto [2] https://gitlab.com/nisec/ecckiila [3] https://github.com/C2SP/wycheproof
1 parent c156b39 commit 2ba6d43

16 files changed

+28965
-4
lines changed

‎bench/speed.ml

+11
Original file line numberDiff line numberDiff line change
@@ -193,6 +193,13 @@ let ecdsa_p256 =
193193

194194
let ecdsa_p256_sig () = Mirage_crypto_ec.P256.Dsa.sign ~key:ecdsa_p256 msg_str_32
195195

196+
let ecdsa_p256k1 =
197+
Result.get_ok
198+
(Mirage_crypto_ec.P256k1.Dsa.priv_of_octets
199+
"\x08\x9f\x4f\xfc\xcc\xf9\xba\x13\xfe\xdd\x09\x42\xef\x08\xcf\x2d\x90\x9f\x32\xe2\x93\x4a\xb5\xc9\x3b\x6c\x99\xbe\x5a\x9f\xf5\x27")
200+
201+
let ecdsa_p256k1_sig () = Mirage_crypto_ec.P256k1.Dsa.sign ~key:ecdsa_p256k1 msg_str_32
202+
196203
let ecdsa_p384 =
197204
Result.get_ok
198205
(Mirage_crypto_ec.P384.Dsa.priv_of_octets
@@ -215,6 +222,7 @@ let ed25519_sig () = Mirage_crypto_ec.Ed25519.sign ~key:ed25519 msg_str
215222

216223
let ecdsas = [
217224
("P256", `P256 (ecdsa_p256, ecdsa_p256_sig ()));
225+
("P256k1", `P256k1 (ecdsa_p256k1, ecdsa_p256k1_sig ()));
218226
("P384", `P384 (ecdsa_p384, ecdsa_p384_sig ()));
219227
("P521", `P521 (ecdsa_p521, ecdsa_p521_sig ()));
220228
("Ed25519", `Ed25519 (ed25519, ed25519_sig ()));
@@ -303,6 +311,7 @@ let benchmarks = [
303311
count name
304312
(fun (_, x) -> match x with
305313
| `P256 _ -> P256.Dsa.generate () |> ignore
314+
| `P256k1 _ -> P256k1.Dsa.generate () |> ignore
306315
| `P384 _ -> P384.Dsa.generate () |> ignore
307316
| `P521 _ -> P521.Dsa.generate () |> ignore
308317
| `Ed25519 _ -> Ed25519.generate () |> ignore
@@ -313,6 +322,7 @@ let benchmarks = [
313322
let open Mirage_crypto_ec in
314323
count name (fun (_, x) -> match x with
315324
| `P256 (key, _) -> P256.Dsa.sign ~key msg_str_32
325+
| `P256k1 (key, _) -> P256k1.Dsa.sign ~key msg_str_32
316326
| `P384 (key, _) -> P384.Dsa.sign ~key msg_str_48
317327
| `P521 (key, _) -> P521.Dsa.sign ~key msg_str_65
318328
| `Ed25519 (key, _) -> Ed25519.sign ~key msg_str, ""
@@ -323,6 +333,7 @@ let benchmarks = [
323333
let open Mirage_crypto_ec in
324334
count name (fun (_, x) -> match x with
325335
| `P256 (key, signature) -> P256.Dsa.(verify ~key:(pub_of_priv key) signature msg_str_32)
336+
| `P256k1 (key, signature) -> P256k1.Dsa.(verify ~key:(pub_of_priv key) signature msg_str_32)
326337
| `P384 (key, signature) -> P384.Dsa.(verify ~key:(pub_of_priv key) signature msg_str_48)
327338
| `P521 (key, signature) -> P521.Dsa.(verify ~key:(pub_of_priv key) signature msg_str_65)
328339
| `Ed25519 (key, signature) -> Ed25519.(verify ~key:(pub_of_priv key) signature ~msg:msg_str)

‎ec/dune

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
(foreign_stubs
66
(language c)
77
(names p256_stubs np256_stubs p384_stubs np384_stubs p521_stubs np521_stubs
8-
curve25519_stubs)
8+
curve25519_stubs secp256k1_stubs)
99
(include_dirs ../src/native)
1010
(flags
1111
(:standard -DNDEBUG)

‎ec/mirage_crypto_ec.ml

+248
Original file line numberDiff line numberDiff line change
@@ -119,6 +119,20 @@ module type Foreign_proj = sig
119119
val scalar_mult_base_c : out_point -> string -> unit
120120
end
121121

122+
module Point_kiila = struct
123+
type point = Point of string [@@unboxed]
124+
type out_point = Point_out of bytes [@@unboxed]
125+
end
126+
127+
module type Foreign_kiila = sig
128+
include Foreign
129+
open Point_kiila
130+
131+
val scalar_mult_base_c : out_point -> string -> unit
132+
val scalar_mult_c : out_point -> string -> point -> unit
133+
val scalar_mult_add_c : out_point -> string -> string -> point -> unit
134+
end
135+
122136
module type Field_element = sig
123137
val create : unit -> out_field_element
124138
val mul : field_element -> field_element -> field_element
@@ -459,6 +473,187 @@ module Make_point (P : Parameters) (F : Foreign_proj) : Point = struct
459473

460474
end
461475

476+
(*
477+
This is an alternative Point implementation, that uses
478+
- concatenated affine coordinates as used by ECCKiila generated code, and
479+
- simplified calculations for a=0 like for the secp256k1 curve
480+
*)
481+
module Make_point_k1 (P : Parameters) (F : Foreign_kiila) : Point = struct
482+
module Fe = Make_field_element(P)(F)
483+
include Point_kiila
484+
485+
let make x y = Point (String.cat x y)
486+
let p_x (Point p) = String.sub p 0 P.fe_length
487+
let p_y (Point p) = String.sub p P.fe_length P.fe_length
488+
let out_point () = Point_out (Bytes.create (P.fe_length * 2))
489+
let out_p_to_p (Point_out p) = Point (Bytes.unsafe_to_string p)
490+
491+
let at_infinity () =
492+
let f_x = Fe.zero in
493+
let f_y = Fe.zero in
494+
make f_x f_y
495+
496+
let is_infinity (p : point) = not (Fe.nz (p_y p))
497+
498+
let is_solution_to_curve_equation =
499+
let b = Fe.from_be_octets P.b in
500+
fun ~x ~y ->
501+
let x3 = Fe.sqr x in
502+
let x3 = Fe.mul x3 x in
503+
let y2 = Fe.sqr y in
504+
let sum = Fe.add x3 b in
505+
let sum = Fe.sub sum y2 in
506+
not (Fe.nz sum)
507+
508+
let check_coordinate buf =
509+
(* ensure buf < p: *)
510+
match Eqaf.compare_be_with_len ~len:P.byte_length buf P.p >= 0 with
511+
| true -> None
512+
| exception Invalid_argument _ -> None
513+
| false -> Some (Fe.from_be_octets buf)
514+
515+
(** Convert coordinates to a finite point ensuring:
516+
- x < p
517+
- y < p
518+
- y^2 = x^3 + b
519+
*)
520+
let validate_finite_point ~x ~y =
521+
match (check_coordinate x, check_coordinate y) with
522+
| Some f_x, Some f_y ->
523+
if is_solution_to_curve_equation ~x:f_x ~y:f_y then
524+
Ok (make f_x f_y)
525+
else Error `Not_on_curve
526+
| _ -> Error `Invalid_range
527+
528+
let to_affine_raw p =
529+
if is_infinity p then
530+
None
531+
else
532+
let x = Fe.from_montgomery (p_x p) in
533+
let y = Fe.from_montgomery (p_y p) in
534+
Some (x, y)
535+
536+
let to_affine p =
537+
Option.map (fun (x, y) -> Fe.to_octets x, Fe.to_octets y)
538+
(to_affine_raw p)
539+
540+
let to_octets ~compress p =
541+
let buf =
542+
match to_affine p with
543+
| None -> String.make 1 '\000'
544+
| Some (x, y) ->
545+
let len_x = String.length x and len_y = String.length y in
546+
let res = Bytes.create (1 + len_x + len_y) in
547+
Bytes.set res 0 '\004' ;
548+
let rev_x = rev_string x and rev_y = rev_string y in
549+
Bytes.unsafe_blit_string rev_x 0 res 1 len_x ;
550+
Bytes.unsafe_blit_string rev_y 0 res (1 + len_x) len_y ;
551+
Bytes.unsafe_to_string res
552+
in
553+
if compress then
554+
let out = Bytes.create (P.byte_length + 1) in
555+
let ident =
556+
2 + (String.get_uint8 buf ((P.byte_length * 2) - 1)) land 1
557+
in
558+
Bytes.unsafe_blit_string buf 1 out 1 P.byte_length;
559+
Bytes.set_uint8 out 0 ident;
560+
Bytes.unsafe_to_string out
561+
else
562+
buf
563+
564+
let x_of_finite_point p =
565+
match to_affine p with None -> assert false | Some (x, _) -> rev_string x
566+
567+
let pow x exp =
568+
let r0 = ref Fe.one in
569+
let r1 = ref x in
570+
for i = P.byte_length * 8 - 1 downto 0 do
571+
let bit = bit_at exp i in
572+
let multiplied = Fe.mul !r0 !r1 in
573+
let r0_sqr = Fe.sqr !r0 in
574+
let r1_sqr = Fe.sqr !r1 in
575+
r0 := Fe.select bit ~then_:multiplied ~else_:r0_sqr;
576+
r1 := Fe.select bit ~then_:r1_sqr ~else_:multiplied;
577+
done;
578+
!r0
579+
580+
let decompress =
581+
(* When p = 4*k+3, as is the case of NIST-P256, there is an efficient square
582+
root algorithm to recover the y, as follows:
583+
584+
Given the compact representation of Q as x,
585+
y2 = x^3 + b (with a=0)
586+
y' = y2^((p+1)/4)
587+
y = min(y',p-y')
588+
Q=(x,y) is the canonical representation of the point
589+
*)
590+
let pident = P.pident (* (Params.p + 1) / 4*) in
591+
let b = Fe.from_be_octets P.b in
592+
let p = Fe.from_be_octets P.p in
593+
fun pk ->
594+
let x = Fe.from_be_octets (String.sub pk 1 P.byte_length) in
595+
let x3 = Fe.mul x x in
596+
let x3 = Fe.mul x3 x in (* x3 *)
597+
let sum = Fe.add x3 b in (* y^2 *)
598+
let y = pow sum pident in (* https://tools.ietf.org/id/draft-jivsov-ecc-compact-00.xml#sqrt point 4.3*)
599+
let y' = Fe.sub p y in
600+
let y = Fe.from_montgomery y in
601+
let y_struct = Fe.to_octets y in (* number must not be in montgomery domain*)
602+
let y_struct = rev_string y_struct in
603+
let y' = Fe.from_montgomery y' in
604+
let y_struct2 = Fe.to_octets y' in (* number must not be in montgomery domain*)
605+
let y_struct2 = rev_string y_struct2 in
606+
let ident = String.get_uint8 pk 0 in
607+
let signY =
608+
2 + (String.get_uint8 y_struct (P.byte_length - 2)) land 1
609+
in
610+
let res = if Int.equal signY ident then y_struct else y_struct2 in
611+
let out = Bytes.create ((P.byte_length * 2) + 1) in
612+
Bytes.set out 0 '\004';
613+
Bytes.unsafe_blit_string pk 1 out 1 P.byte_length;
614+
Bytes.unsafe_blit_string res 0 out (P.byte_length + 1) P.byte_length;
615+
Bytes.unsafe_to_string out
616+
617+
let of_octets buf =
618+
let len = P.byte_length in
619+
if String.length buf = 0 then
620+
Error `Invalid_format
621+
else
622+
let of_octets buf =
623+
let x = String.sub buf 1 len in
624+
let y = String.sub buf (1 + len) len in
625+
validate_finite_point ~x ~y
626+
in
627+
match String.get_uint8 buf 0 with
628+
| 0x00 when String.length buf = 1 ->
629+
Ok (at_infinity ())
630+
| 0x02 | 0x03 when String.length P.pident > 0 ->
631+
let decompressed = decompress buf in
632+
of_octets decompressed
633+
| 0x04 when String.length buf = 1 + len + len ->
634+
of_octets buf
635+
| 0x00 | 0x04 -> Error `Invalid_length
636+
| _ -> Error `Invalid_format
637+
638+
let scalar_mult_base (Scalar d) =
639+
let tmp = out_point () in
640+
F.scalar_mult_base_c tmp d;
641+
out_p_to_p tmp
642+
643+
let scalar_mult (Scalar s) p =
644+
let tmp = out_point () in
645+
F.scalar_mult_c tmp s p;
646+
out_p_to_p tmp
647+
648+
let scalar_mult_add (Scalar a) (Scalar b) p =
649+
let tmp = out_point () in
650+
F.scalar_mult_add_c tmp a b p;
651+
out_p_to_p tmp
652+
653+
let generator_tables () =
654+
assert false
655+
end
656+
462657
module type Scalar = sig
463658
val not_zero : string -> bool
464659
val is_in_range : string -> bool
@@ -819,6 +1014,59 @@ module P256 : Dh_dsa = struct
8191014
module Dsa = Make_dsa(Params)(Fn)(P)(S)(Digestif.SHA256)
8201015
end
8211016

1017+
1018+
module P256k1 : Dh_dsa = struct
1019+
module Params = struct
1020+
let a = "\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"
1021+
let b = "\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x07"
1022+
let g_x = "\x79\xBE\x66\x7E\xF9\xDC\xBB\xAC\x55\xA0\x62\x95\xCE\x87\x0B\x07\x02\x9B\xFC\xDB\x2D\xCE\x28\xD9\x59\xF2\x81\x5B\x16\xF8\x17\x98"
1023+
let g_y = "\x48\x3A\xDA\x77\x26\xA3\xC4\x65\x5D\xA4\xFB\xFC\x0E\x11\x08\xA8\xFD\x17\xB4\x48\xA6\x85\x54\x19\x9C\x47\xD0\x8F\xFB\x10\xD4\xB8"
1024+
let p = "\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFE\xFF\xFF\xFC\x2F"
1025+
let n = "\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFE\xBA\xAE\xDC\xE6\xAF\x48\xA0\x3B\xBF\xD2\x5E\x8C\xD0\x36\x41\x41"
1026+
let pident = "\x3F\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xBF\xFF\xFF\x0C" |> rev_string (* (Params.p + 1) / 4*)
1027+
let byte_length = 32
1028+
let bit_length = 256
1029+
let fe_length = 32
1030+
let first_byte_bits = None
1031+
end
1032+
1033+
module Foreign = struct
1034+
include Point_kiila
1035+
external mul : out_field_element -> field_element -> field_element -> unit = "mc_secp256k1_mul" [@@noalloc]
1036+
external sub : out_field_element -> field_element -> field_element -> unit = "mc_secp256k1_sub" [@@noalloc]
1037+
external add : out_field_element -> field_element -> field_element -> unit = "mc_secp256k1_add" [@@noalloc]
1038+
external to_montgomery : out_field_element -> field_element -> unit = "mc_secp256k1_to_montgomery" [@@noalloc]
1039+
external from_octets : out_field_element -> string -> unit = "mc_secp256k1_from_bytes" [@@noalloc]
1040+
external set_one : out_field_element -> unit = "mc_secp256k1_set_one" [@@noalloc]
1041+
external nz : field_element -> bool = "mc_secp256k1_nz" [@@noalloc]
1042+
external sqr : out_field_element -> field_element -> unit = "mc_secp256k1_sqr" [@@noalloc]
1043+
external from_montgomery : out_field_element -> field_element -> unit = "mc_secp256k1_from_montgomery" [@@noalloc]
1044+
external to_octets : bytes -> field_element -> unit = "mc_secp256k1_to_bytes" [@@noalloc]
1045+
external inv : out_field_element -> field_element -> unit = "mc_secp256k1_inv" [@@noalloc]
1046+
external select_c : out_field_element -> bool -> field_element -> field_element -> unit = "mc_secp256k1_select" [@@noalloc]
1047+
external scalar_mult_c : out_point -> string -> point -> unit = "mc_secp256k1_scalar_mult" [@@noalloc]
1048+
external scalar_mult_add_c : out_point -> string -> string -> point -> unit = "mc_secp256k1_scalar_mult_add" [@@noalloc]
1049+
external scalar_mult_base_c : out_point -> string -> unit = "mc_secp256k1_scalar_mult_base" [@@noalloc]
1050+
end
1051+
1052+
module Foreign_n = struct
1053+
external mul : out_field_element -> field_element -> field_element -> unit = "mc_nsecp256k1_mul" [@@noalloc]
1054+
external add : out_field_element -> field_element -> field_element -> unit = "mc_nsecp256k1_add" [@@noalloc]
1055+
external inv : out_field_element -> field_element -> unit = "mc_nsecp256k1_inv" [@@noalloc]
1056+
external one : out_field_element -> unit = "mc_nsecp256k1_one" [@@noalloc]
1057+
external from_bytes : out_field_element -> string -> unit = "mc_nsecp256k1_from_bytes" [@@noalloc]
1058+
external to_bytes : bytes -> field_element -> unit = "mc_nsecp256k1_to_bytes" [@@noalloc]
1059+
external from_montgomery : out_field_element -> field_element -> unit = "mc_nsecp256k1_from_montgomery" [@@noalloc]
1060+
external to_montgomery : out_field_element -> field_element -> unit = "mc_nsecp256k1_to_montgomery" [@@noalloc]
1061+
end
1062+
1063+
module P = Make_point_k1(Params)(Foreign)
1064+
module S = Make_scalar(Params)(P)
1065+
module Dh = Make_dh(Params)(P)(S)
1066+
module Fn = Make_Fn(Params)(Foreign_n)
1067+
module Dsa = Make_dsa(Params)(Fn)(P)(S)(Digestif.SHA256)
1068+
end
1069+
8221070
module P384 : Dh_dsa = struct
8231071
module Params = struct
8241072
let a = "\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFE\xFF\xFF\xFF\xFF\x00\x00\x00\x00\x00\x00\x00\x00\xFF\xFF\xFF\xFC"

‎ec/mirage_crypto_ec.mli

+3
Original file line numberDiff line numberDiff line change
@@ -168,6 +168,9 @@ end
168168
(** The NIST P-256 curve, also known as SECP256R1. *)
169169
module P256 : Dh_dsa
170170

171+
(** The SECP256K1 curve. *)
172+
module P256k1 : Dh_dsa
173+
171174
(** The NIST P-384 curve, also known as SECP384R1. *)
172175
module P384 : Dh_dsa
173176

‎ec/native/GNUmakefile

+28
Original file line numberDiff line numberDiff line change
@@ -132,6 +132,34 @@ curve25519_32.h:
132132
.PHONY: curve25519
133133
curve25519: curve25519_64.h curve25519_32.h
134134

135+
136+
# SECP256K1 (aka Bitcoin curve)
137+
SECP256K1="2^256 - 2^32 - 977"
138+
139+
.PHONY: secp256k1_64.h
140+
secp256k1_64.h:
141+
$(WBW_MONT) --inline secp256k1 64 $(SECP256K1) > $@
142+
143+
.PHONY: secp256k1_32.h
144+
secp256k1_32.h:
145+
$(WBW_MONT) --inline secp256k1 32 $(SECP256K1) > $@
146+
147+
# The group order N of P-256
148+
SECP256K1N="2^256 - 432420386565659656852420866394968145599"
149+
150+
.PHONY: nsecp256k1_64.h
151+
nsecp256k1_64.h:
152+
$(WBW_MONT) --inline nsecp256k1 64 $(SECP256K1N) $(N_FUNCS) > $@
153+
154+
.PHONY: nsecp256k1_32.h
155+
nsecp256k1_32.h:
156+
$(WBW_MONT) --inline nsecp256k1 32 $(SECP256K1N) $(N_FUNCS) > $@
157+
158+
.PHONY: secp256k1
159+
secp256k1: secp256k1_64.h secp256k1_32.h nsecp256k1_64.h nsecp256k1_32.h
160+
161+
###
162+
135163
.PHONY: tables
136164
tables: p256_tables p384_tables p521_tables
137165

0 commit comments

Comments
 (0)