Merge branch 'wmaster'

Merge PR

Common/utils.cry

@@ -0,0 +1,50 @@
+module Common::utils where
+
+while : {a} (a -> Bit) -> (a -> a) -> a -> a
+while condition body initial_state =
+  if(condition initial_state) then while condition body (body initial_state)
+  else initial_state
+
+dowhile : {a} (a -> Bit) -> (a -> a) -> a -> a
+dowhile condition body initial_state =
+  if(condition next_state) then while condition body next_state else next_state
+  where next_state = body initial_state
+
+ZtoBV : {p, a} (fin p, p >= 1, fin a) => Z p -> [a]
+ZtoBV x = (fromInteger (fromZ x))
+
+BVtoZ : {p, a} (fin p, p >= 1, fin a) => [a] -> Z p
+BVtoZ x = (fromInteger (toInteger x))
+
+ZtoZ : {p, q} (fin p, fin q, p >= 1, q >= 1) => Z p -> Z q
+ZtoZ x = (fromInteger (fromZ x))
+
+isEven : Integer -> Bit
+isEven x = ~((fromInteger x) : [1]) ! 0
+
+mul2 x = x + x
+mul3 x = x + mul2 x
+mul4 x = mul2(mul2 x)
+mul8 x = mul2(mul4 x)
+
+type constraint isOdd a = (a / 2) * 2 == a - 1
+
+half : {p} (fin p, p >= 3, isOdd p) => Z p -> Z p
+half x = if isEven (fromZ x) then x/2 else (fromInteger ((fromZ x + `p) / 2))
+
+mp_mod_inv : {a} (fin a, a >= 1) => Z a -> Z a
+mp_mod_inv c = if c == 0 then error "Zero does not have a multiplicative inverse"
+               else fromInteger (if u'' == 1 then x1'' else x2'')
+  where
+    innercond (a, x) = isEven a
+    innerbody (a, x) = (a / 2, if isEven x then x / 2 else (x + `a) / 2)
+
+    outtercond (u, v, x1, x2) = (u != 1) /\ (v != 1)
+    outterbody (u, v, x1, x2) = if(u' >= v') then (u' - v', v', x1' - x2' % `a, x2')
+                                             else (u', v' - u', x1', x2' - x1' % `a)
+      where
+        (u', x1') = while innercond innerbody (u, x1)
+        (v', x2') = while innercond innerbody (v, x2)
+
+    (u'', _, x1'', x2'') = while outtercond outterbody (fromZ c, `a, 1, 0)
+

Primitive/Asymmetric/Signature/ECDSA/ECDSA.cry

@@ -0,0 +1,218 @@
+module Primitive::Asymmetric::Signature::ECDSA::ECDSA where
+
+import Common::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]) ]