Skip to content

Commit

Permalink
Merge pull request #142 from GaloisInc/138-endian-conversions
Browse files Browse the repository at this point in the history 
SHA3: add new API that handles bit ordering conversions
  • Loading branch information
@marsella
marsella authored Oct 10, 2024
2 parents 277dace + bfc6667 commit ce3b9a9
Show file tree
Hide file tree
Showing 13 changed files with 839 additions and 311 deletions.
208 changes: 106 additions & 102 deletions Primitive/Asymmetric/Cipher/Kyber/3.01/specification.tex
View file

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ module Primitive::Asymmetric::Cipher::ML_KEM::Specification where
import Primitive::Keyless::Hash::SHAKE::SHAKE256
import Primitive::Keyless::Hash::SHAKE::SHAKE128
import `Primitive::Keyless::Hash::SHA3::SHA3
import Primitive::Keyless::Hash::utils
import Primitive::Keyless::Hash::KeccakBitOrdering

/*
* [FIPS-203] Section 2.3.
Expand Down
5 changes: 4 additions & 1 deletion Primitive/Asymmetric/Signature/Dilithium/Final_Draft/DilithiumParameterized.cry
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,11 +2,14 @@
* This module implements FIPS204 ML-DSA Final Draft.
*
* This specification was developed in collaboration with MITRE.
*
* @copyright Galois Inc
* @author Brett Boston
*/
module DilithiumParameterized where
import Primitive::Keyless::Hash::SHAKE::SHAKE128 as SHA3 (shake128)
import Primitive::Keyless::Hash::SHAKE::SHAKE256 as SHA3 (shake256)
import Primitive::Keyless::Hash::utils as SHA3 (toBytes)
import Primitive::Keyless::Hash::KeccakBitOrdering as SHA3 (toBytes)
import Common::utils (dowhile, unzip, while)

// Parameterize the types based on the implementations, weak, medium,
Expand Down
25 changes: 13 additions & 12 deletions Primitive/Asymmetric/Signature/Dilithium/Round1/DilithiumBitVec.cry
View file
Original file line number Diff line number Diff line change
@@ -1,18 +1,19 @@
/*
This module implements the digital signature scheme Dilithium
submitted to the NIST post-quantum project.

See https://pq-crystals.org/dilithium/data/dilithium-specification.pdf

Copyright (c) 2018, Galois Inc.
www.cryptol.net
*/
* This module implements the digital signature scheme Dilithium
* submitted to the NIST post-quantum project.
*
* See https://pq-crystals.org/dilithium/data/dilithium-specification.pdf
*
* @copyright Galois Inc. 2018
* @author Ajay Kumar Eeralla
* @editor Andrew Kent
*/

module Primitive::Asymmetric::Signature::Dilithium::Round1::DilithiumBitVec where

import Primitive::Keyless::Hash::SHAKE::SHAKE128 as SHA3 (shake128)
import Primitive::Keyless::Hash::SHAKE::SHAKE256 as SHA3 (shake256)
import Primitive::Keyless::Hash::utils as SHA3 (toBytes)
import Primitive::Keyless::Hash::KeccakBitOrdering as SHA3 (toBytes)
import Common::utils
import Common::mod_arith
import Primitive::Asymmetric::Cipher::RSA
Expand Down Expand Up @@ -96,7 +97,7 @@ Gen seed = (pk, sk)
seed = 0x7c9935a0b07694aa0c6d10e4db6b1add2fd81a25ccb148032dcd739936737f2d
(pk, sk) = Gen seed
*/
/* Generate signature for message M */
/* Generate signature for message M */
Sign : {mbytes} (fin mbytes, mbytes>=1) => SecretKey -> [mbytes*8] -> (polyVec l, [k][n], poly)
Sign sk M = (final_state.z, h, nttinv final_state.c')
where
Expand Down Expand Up @@ -143,7 +144,7 @@ sign_condition sv = fail1 \/ fail2
fail1 = ((infNormPolyVec (PVtoIPV sv.z)) >= (gamma1-beta))
\/ ((infNormPolyVec sv.r0) >= (gamma2-beta))
\/ (sv.r1 != sv.w1)
fail2 = ((infNormPolyVec (PVtoIPV ct0)) >= gamma2)
fail2 = ((infNormPolyVec (PVtoIPV ct0)) >= gamma2)
\/ ( (foldl (+) 0 (map ones h)) > omega )
ct0 = map nttinv (nttVecConstMul sv.c' sv.t0')
h = MakeHintV (psubV zero ct0
Expand Down Expand Up @@ -177,7 +178,7 @@ Verify pk M (z, h, c) = crit1 && crit2 && crit3
zntt = map ntt z
t1ntt = map ntt (IPVtoPV pk.t1)
ct1ntt = nttVecConstMul (psub zero c) t1ntt
ct1ntt2d = map (\p -> map (\x -> x*(2^^d)) p) ct1ntt
ct1ntt2d = map (\p -> map (\x -> x*(2^^d)) p) ct1ntt
Az = nttMatMul A zntt
w1' = UseHintV (h, paddV Az ct1ntt2d, 2*gamma2)
zint = PVtoIPV z
Expand Down
43 changes: 22 additions & 21 deletions Primitive/Asymmetric/Signature/Dilithium/Round1/DilithiumInteger.cry
View file
Original file line number Diff line number Diff line change
@@ -1,18 +1,19 @@
/*
This module implements the digital signature scheme Dilithium
submitted to the NIST post-quantum project.

See https://pq-crystals.org/dilithium/data/dilithium-specification.pdf

Copyright (c) 2018, Galois Inc.
www.cryptol.net
*/
* This module implements the digital signature scheme Dilithium
* submitted to the NIST post-quantum project.
*
* See https://pq-crystals.org/dilithium/data/dilithium-specification.pdf
*
* @copyright Galois Inc. 2018
* @author Ajay Kumar Eeralla
* @editor Andrew Kent
*/

module Primitive::Asymmetric::Signature::Dilithium::Round1::DilithiumInteger where

import Primitive::Keyless::Hash::SHAKE::SHAKE128 as SHA3 (shake128)
import Primitive::Keyless::Hash::SHAKE::SHAKE256 as SHA3 (shake256)
import Primitive::Keyless::Hash::utils as SHA3 (toBytes)
import Primitive::Keyless::Hash::KeccakBitOrdering as SHA3 (toBytes)
import Common::utils hiding (abs)
import Primitive::Asymmetric::Signature::Dilithium::test::testDilithium
import Primitive::Asymmetric::Signature::Dilithium::test::signFinal
Expand All @@ -21,12 +22,12 @@ import Primitive::Asymmetric::Signature::Dilithium::test::test_latest

// Recommended Parameters
type q = 8380421
type n = 256
type n = 256
type k = 5
type l = 4
d = 14
wc = 60
gamma1 = ((`q : Integer) - 1) / 16
gamma1 = ((`q : Integer) - 1) / 16
gamma2 = (gamma1 / 2)
eta = 5
beta = 275
Expand All @@ -48,7 +49,7 @@ type intPolyVec dim = [dim]intPoly

// Polynomials; a superset of ring R_q referenced in specification
type poly = [n](Z q) // This is R_q, actually defines a super set of R_q
type polyVec dim = [dim]poly
type polyVec dim = [dim]poly

// Polynomials in NTT representation
type nttPoly = [n](Z q)
Expand All @@ -57,7 +58,7 @@ type nttMat dim1 dim2 = [dim1](nttVec dim2)



type PublicKey = {rho : [256], t1 : intPolyVec k}
type PublicKey = {rho : [256], t1 : intPolyVec k}
type SecretKey = {rho : [256]
, K : [256]
, tr : [384]
Expand Down Expand Up @@ -93,7 +94,7 @@ test_key_gen = (pk.rho#(pack_t1 pk.t1) == testCase0.pk)
seed = 0x7c9935a0b07694aa0c6d10e4db6b1add2fd81a25ccb148032dcd739936737f2d
(pk, sk) = Gen seed

/* Generate signature for message M */
/* Generate signature for message M */
Sign : {mbytes} (fin mbytes, mbytes>=1) => SecretKey -> [mbytes*8] -> (polyVec l, [k][n], poly)
Sign sk M = (final_state.z, h, nttinv final_state.c')
where
Expand Down Expand Up @@ -134,12 +135,12 @@ private


sign_condition : sign_var_types -> Bit
sign_condition sv = fail1 \/ fail2
sign_condition sv = fail1 \/ fail2
where
fail1 = ((infNormPolyVec (PVtoIPV sv.z)) >= (gamma1-beta))
\/ ((infNormPolyVec sv.r0) >= (gamma2-beta))
\/ (sv.r1 != sv.w1)
fail2 = ((infNormPolyVec (PVtoIPV ct0)) >= gamma2)
fail2 = ((infNormPolyVec (PVtoIPV ct0)) >= gamma2)
\/ ( (foldl (+) 0 (map ones h)) > omega )
ct0 = map nttinv (nttVecConstMul sv.c' sv.t0')
h = MakeHintV (psubV zero ct0
Expand Down Expand Up @@ -173,7 +174,7 @@ Verify pk M (z, h, c) = crit1 && crit2 && crit3
zntt = map ntt z
t1ntt = map ntt (IPVtoPV pk.t1)
ct1ntt = nttVecConstMul (psub zero c) t1ntt
ct1ntt2d = map (\p -> map (\x -> x*(2^^d)) p) ct1ntt
ct1ntt2d = map (\p -> map (\x -> x*(2^^d)) p) ct1ntt
Az = nttMatMul A zntt
w1' = UseHintV (h, paddV Az ct1ntt2d, 2*gamma2)
zint = PVtoIPV z
Expand Down Expand Up @@ -319,7 +320,7 @@ private
CRH seed = join (SHA3::toBytes (take`{48*8} (SHA3::shake256 (join (SHA3::toBytes seed)))))


ExpandA : [256] -> [k][l]nttPoly
ExpandA : [256] -> [k][l]nttPoly
ExpandA rho = [ [elt i j | j <- [0..(l-1)] ] | i <- [0..(k-1)] ]
where
elt i j = matrixPoly rho i j
Expand Down Expand Up @@ -446,7 +447,7 @@ private
then [ elt ]#(randomsInRange createElt upperCrit randomTail)
else randomsInRange createElt upperCrit randomTail
where
elt = createElt (take`{a} randoms)
elt = createElt (take`{a} randoms)
randomTail = drop`{a} randoms

randomsInRanges : {a,m} (fin a,fin m, m>=1) => ([a]-> [a]) -> [m][a] -> [inf] -> [inf][a]
Expand All @@ -455,7 +456,7 @@ private
then [ elt ]#(randomsInRanges createElt uppersRotate randomTail)
else randomsInRanges createElt uppers randomTail
where
elt = createElt (take`{a} randoms)
elt = createElt (take`{a} randoms)
randomTail = drop`{a} randoms
uppersRotate = uppers <<< 1

Expand All @@ -473,7 +474,7 @@ private
then [ elts@1 ]#(randomsInRangeDouble createElt upper randomTail)
else randomsInRangeDouble createElt upper randomTail
where
elts = createElt (take`{2*a} randoms)
elts = createElt (take`{2*a} randoms)
randomTail = drop`{2*a} randoms*/
// Correction and checked with the C code
randomsInRangeDouble createElt upper randoms =
Expand Down
Loading

0 comments on commit ce3b9a9

Please sign in to comment.