Skip to content

Commit

Permalink
Added a Z type ECDSA implementation
Browse files Browse the repository at this point in the history
  • Loading branch information
Sean Weaver committed Nov 21, 2018
1 parent 7a5b50b commit b071364
Show file tree
Hide file tree
Showing 9 changed files with 633 additions and 0 deletions.
218 changes: 218 additions & 0 deletions Primitive/Asymmetric/Signature/ECDSA/ECDSA.cry
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,218 @@
module ECDSA where

import utils

sign : Z q -> Z q -> Z p -> (Z q, Z q)
sign d z k = (r, s)
where {x = x1, y = _} = ec_affinify (ec_mult k G)
r = ZtoZ x1
s = (mp_mod_inv (ZtoZ k)) * (z + r*d)

private_to_public : Z q -> ProjectivePoint p
private_to_public d = ec_mult (ZtoZ d) G

verify : Z q -> ProjectivePoint p -> (Z q, Z q) -> Bit
verify z Q (r, s) = r == ZtoZ j
where w = mp_mod_inv s
u1 = z * w
u2 = r * w
{x = x1, y = _, z = z1} = ec_twin_mult (ZtoZ u1) G (ZtoZ u2) Q
j = x1 * (mp_mod_inv z1)^^2

//Examples
G_compress R = ec_compress (ec_affinify G) == R

full_add_example : AffinePoint p -> AffinePoint p -> AffinePoint p -> Bit
full_add_example R S T =
ec_affinify (ec_full_add (ec_projectify S) (ec_projectify T)) == R

full_subtract_example : AffinePoint p -> AffinePoint p -> AffinePoint p -> Bit
full_subtract_example R S T =
ec_affinify (ec_full_sub (ec_projectify S) (ec_projectify T)) == R

double_example : AffinePoint p -> AffinePoint p -> Bit
double_example R S =
ec_affinify (ec_double (ec_projectify S)) == R

scalar_multiply_example : AffinePoint p -> AffinePoint p -> Z p -> Bit
scalar_multiply_example R S d =
ec_affinify (ec_mult d (ec_projectify S)) == R

joint_scalar_multiply_example : AffinePoint p -> AffinePoint p -> AffinePoint p -> Z p -> Z p -> Bit
joint_scalar_multiply_example R S T d e =
ec_affinify (ec_twin_mult d (ec_projectify S) e (ec_projectify T)) == R

mp_mod_sqrt_correct x = (mp_mod_sqrt (x ^^ 2)) ^^ 2 == (x ^^ 2)


parameter

type p : #
type constraint Constraints p

b : Z p

G : ProjectivePoint p

type q : #
type constraint Constraints q

mp_mod_sqrt : Z p -> Z p

private

type constraint Constraints a = (fin a, isOdd a, width a >= 4)

type AffinePoint a = {x : Z a, y : Z a}
type ProjectivePoint a = {x : Z a, y : Z a, z : Z a}

ec_projectify : {a} (Constraints a) => AffinePoint a -> ProjectivePoint a
ec_projectify S = {x = S.x, y = S.y, z = 1}

ec_affinify : {a} (Constraints a) => ProjectivePoint a -> AffinePoint a
ec_affinify S = if S.z == 0 then error "Cannot affinify the point at infinity"
else {x = lambda^^2 * S.x, y = lambda^^3 * S.y}
where
lambda = mp_mod_inv S.z

ec_compress : {r} (fin r, r >= width p + 2) => AffinePoint p -> [r]
ec_compress S = (2 + (Sy % 2)) # Sx
where Sx = ZtoBV S.x : [width p]
Sy = ZtoBV S.y : [r - width p]

ec_decompress : {a, b} (fin a, a >= width p + 2, fin b, p >= 1 + b) => [a] -> (AffinePoint p, Bit)
ec_decompress S = ({x = Rx, y = Ry}, err)
where c = BVtoZ (take S : [2])
Rx = BVtoZ (drop S : [a-2])
t0 = Rx^^3 - (mul3 Rx) + `b
t1 = mp_mod_sqrt t0
err = t1 ^^ 2 != t0
Ry = if t1 == c%2 then t1 else -t1

ec_is_point_affine : AffinePoint p -> Bit
ec_is_point_affine S = S.y ^^ 2 == t
where t = S.x ^^ 3 + b

ec_double : {a} (Constraints a) => ProjectivePoint a -> ProjectivePoint a
ec_double S =
if S.z == 0 then
{x = 1, y = 1, z = 0} /* 5: r <- (1,1,0) and return */
else
{x = r18, y = r23, z = r13}
where r7 = S.z ^^ 2 /* 7: t4 <- (t3)^2 */
r8 = S.x - r7 /* 8: t5 <- t1 - t4 */
r9 = S.x + r7 /* 9: t4 <- t1 + t4 */
r10 = r9 * r8 /* 10: t5 <- t4 * t5 */
r11 = mul3 r10 /* 11: t4 <- 3 * t5 */
r12 = S.z * S.y /* 12: t3 <- t3 * t2 */
r13 = mul2 r12 /* 13: t3 <- 2 * t3 */
r14 = S.y ^^ 2 /* 14: t2 <- (t2)^2 */
r15 = S.x * r14 /* 15: t5 <- t1 * t2 */
r16 = mul4 r15 /* 16: t5 <- 4 * t5 */
r17 = r11 ^^ 2 /* 17: t1 <- (t4)^2 */
r18 = r17 - (mul2 r16) /* 18: t1 <- t1 - 2 * t5 */
r19 = r14 ^^ 2 /* 19: t2 <- (t2)^2 */
r20 = mul8 r19 /* 20: t2 <- 8 * t2 */
r21 = r16 - r18 /* 21: t5 <- t5 - t1 */
r22 = r11 * r21 /* 22: t5 <- t4 * t5 */
r23 = r22 - r20 /* 23: t2 <- t5 - t2 */

ec_add : {a} (Constraints a) => ProjectivePoint a -> ProjectivePoint a -> ProjectivePoint a
ec_add S T =
if r13 == 0 then
if r14 == 0 then
{x = 0, y = 0, z = 0} /* 17: r <- (0,0,0) and return */
else
{x = 1, y = 1, z = 0} /* 19: r <- (1,1,0) and return */
else
{x = r32, y = r37, z = r27}
where r9 = S.z ^^ 2 /* 9: t7 <- (t3)^2 */
r10 = T.x * r9 /* 10: t4 <- t4 * t7 */
r11 = S.z * r9 /* 11: t7 <- t3 * t7 */
r12 = T.y * r11 /* 12: t5 <- t5 * t7 */
r13 = S.x - r10 /* 13: t4 <- t1 - t4 */
r14 = S.y - r12 /* 14: t5 <- t2 - t5 */

r22 = mul2 S.x - r13 /* 22: t1 <- 2*t1 - t4 */
r23 = mul2 S.y - r14 /* 23: t2 <- 2*t2 - t5 */

r27 = S.z * r13 /* 27: t3 <- t3 * t4 */
r28 = r13 ^^ 2 /* 28: t7 <- (t4)^2 */
r29 = r13 * r28 /* 29: t4 <- t4 * t7 */
r30 = r22 * r28 /* 30: t7 <- t1 * t7 */
r31 = r14 ^^ 2 /* 31: t1 <- (t5)^2 */
r32 = r31 - r30 /* 32: t1 <- t1 - t7 */
r33 = r30 - (mul2 r32) /* 33: t7 <- t7 - 2*t1 */
r34 = r14 * r33 /* 34: t5 <- t5 * t7 */
r35 = r23 * r29 /* 35: t4 <- t2 * t4 */
r36 = r34 - r35 /* 36: t2 <- t5 - t4 */
r37 = half r36 /* 37: t2 <- t2/2 */

ec_full_add : {a} (Constraints a) => ProjectivePoint a -> ProjectivePoint a -> ProjectivePoint a
ec_full_add S T =
if S.z == 0 then T
| T.z == 0 then S
| R == {x = 0, y = 0, z = 0} then ec_double S
else R
where R = ec_add S T

ec_full_sub : {a} (Constraints a) => ProjectivePoint a -> ProjectivePoint a -> ProjectivePoint a
ec_full_sub S T = R
where U = {x = T.x, y = -T.y, z = T.z}
R = ec_full_add S U

ec_mult : {a} (Constraints a) => Z a -> ProjectivePoint a -> ProjectivePoint a
ec_mult d S = if d == 0 then {x = 1, y = 1, z = 0}
| d == 1 then S
| S.z == 0 then {x = 1, y = 1, z = 0}
else Rs!1
where S' = if S.z != 1 then ec_projectify (ec_affinify S) else S
k = ZtoBV d : [width a + 2]
h = k + k + k
Rs = [{x = 1, y = 1, z = 0}] # //Here we start with 1 instead of S because we don't really know where the high-bit is
[ if hi && ~ki then ec_full_add RiDouble S
| ~hi && ki then ec_full_sub RiDouble S
else RiDouble
where RiDouble = ec_double Ri
| ki <- k | hi <- h | Ri <- Rs ]

F : [5] -> [5]
F t = if (18 <= t) && (t < 22) then 9
| (14 <= t) && (t < 18) then 10
| (22 <= t) && (t < 24) then 11
| (4 <= t) && (t < 12) then 14
else 12

ec_twin_mult : {a} (Constraints a) => Z a -> ProjectivePoint a -> Z a -> ProjectivePoint a -> ProjectivePoint a
ec_twin_mult d0 S d1 T = (states!0).0
where Sp = if S.z != 1 then ec_projectify (ec_affinify S) else S
Tp = if T.z != 1 then ec_projectify (ec_affinify T) else T
SpT = ec_full_add Sp Tp
SpTp = if SpT.z != 1 then ec_projectify (ec_affinify SpT) else SpT
SmT = ec_full_sub Sp Tp
SmTp = if SmT.z != 1 then ec_projectify (ec_affinify SmT) else SmT
e0 = ZtoBV d0 : [width a]
e1 = ZtoBV d1 : [width a]
c = [[False, False] # take e0,
[False, False] # take e1] : [2][6]
states = [({x = 1, y = 1, z = 0}, c)] #
[ (Rk', [c0', c1'])
where h0 = if c0@0 then 31 - tail c0 else tail c0
h1 = if c1@0 then 31 - tail c1 else tail c1
u0 = if h0 < (F h1) then 0 else if c0@0 then -1 else 1 : [2]
u1 = if h1 < (F h0) then 0 else if c1@0 then -1 else 1 : [2]
c0' = [(u0!=0) ^ c0@1] # drop c0 # [e0k]
c1' = [(u1!=0) ^ c1@1] # drop c1 # [e1k]
Rk' = if (u0 == -1) && (u1 == -1) then ec_full_sub RkDouble SpTp
| (u0 == -1) && (u1 == 0) then ec_full_sub RkDouble Sp
| (u0 == -1) && (u1 == 1) then ec_full_sub RkDouble SmTp
| (u0 == 0) && (u1 == -1) then ec_full_sub RkDouble Tp
| (u0 == 0) && (u1 == 1) then ec_full_add RkDouble Tp
| (u0 == 1) && (u1 == -1) then ec_full_add RkDouble SmTp
| (u0 == 1) && (u1 == 0) then ec_full_add RkDouble Sp
| (u0 == 1) && (u1 == 1) then ec_full_add RkDouble SpTp
else RkDouble
RkDouble = ec_double Rk
| (Rk, [c0, c1]) <- states
| e0k <- drop`{4} e0 # (zero : [5])
| e1k <- drop`{4} e1 # (zero : [5]) ]
Loading

0 comments on commit b071364

Please sign in to comment.