diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml new file mode 100644 index 0000000..cdf0be7 --- /dev/null +++ b/.github/workflows/ci.yml @@ -0,0 +1,36 @@ +name: crypto-specs + +on: + workflow_dispatch: + push: + +env: + OPAMROOT: /home/charlie/.opam + OPAMYES: true + OPAMJOBS: 2 + ECRJOBS: 1 + +jobs: + ec: + name: Check EasyCrypt Files + runs-on: ubuntu-20.04 + container: + image: ghcr.io/easycrypt/ec-build-box + strategy: + fail-fast: false + steps: + - uses: actions/checkout@v4 + - uses: actions/checkout@v4 + with: + repository: jasmin-lang/jasmin + ref: refs/heads/main + path: jasmin + - name: Compile & Install EasyCrypt + run: | + opam pin --dev-repo add -n easycrypt https://github.com/EasyCrypt/easycrypt.git + opam install -v easycrypt + - name: Detect SMT provers + run: | + opam config exec -- easycrypt why3config + - name: Compile Project + run: opam exec -- make check diff --git a/Makefile b/Makefile index e29f0c8..c9eb31f 100644 --- a/Makefile +++ b/Makefile @@ -2,6 +2,7 @@ # -------------------------------------------------------------------- ECCONF := config/tests.config +JOBS ?= 1 CHECKS ?= specs # -------------------------------------------------------------------- @@ -10,7 +11,7 @@ CHECKS ?= specs default: check check: - easycrypt runtest $(ECCONF) $(CHECKS) + easycrypt runtest -jobs $(JOBS) $(ECCONF) $(CHECKS) clean_eco: - find kyber768 -name '*.eco' -exec rm '{}' ';' + find . -name '*.eco' -exec rm '{}' ';' diff --git a/config/tests.config b/config/tests.config index 9b021f6..bc65690 100644 --- a/config/tests.config +++ b/config/tests.config @@ -1,6 +1,5 @@ [default] bin = easycrypt -args = -timeout 30 -R ml-kem -I Jasmin:jasmin/eclib -I common -I mlkem [test-specs] -okdirs = common ml-kem/ ml-kem/properties fips202 fips202/properties +okdirs = !common !fips202 !ml-kem diff --git a/easycrypt.project b/easycrypt.project index f0da78b..d4aa491 100644 --- a/easycrypt.project +++ b/easycrypt.project @@ -5,8 +5,7 @@ provers = Alt-Ergo@2.4 provers = CVC4@1.8 provers = Z3@4.8 +rdirs = Jasmin:jasmin/eclib rdirs = common -idirs = fips202 -idirs = fips202/properties -idirs = ml-kem -idirs = ml-kem/properties +rdirs = fips202 +rdirs = ml-kem diff --git a/fips202/.dir-locals.el b/fips202/.dir-locals.el deleted file mode 100644 index 50bf302..0000000 --- a/fips202/.dir-locals.el +++ /dev/null @@ -1,12 +0,0 @@ -((easycrypt-mode . - ((eval . - (cl-flet ((pre (s) (concat (locate-dominating-file buffer-file-name ".dir-locals.el") s))) - (setq easycrypt-load-path `(,(pre "."))) - (setq easycrypt-prog-args `("-emacs", "-pp-width", "120", - "-R", (pre "../common") - "-R", (pre "./properties") - ) - ) - ) - )) -)) diff --git a/fips202/Makefile b/fips202/Makefile deleted file mode 100644 index a0ae901..0000000 --- a/fips202/Makefile +++ /dev/null @@ -1,17 +0,0 @@ -EASYCRYPT = easycrypt -EC_PARAMS = -I ../common - -.PHONY: clean typecheck - -typecheck: - $(EASYCRYPT) $(EC_PARAMS) FIPS202_Keccakf1600.ec - $(EASYCRYPT) $(EC_PARAMS) FIPS202_SHA3.ec - -# $(EASYCRYPT) $(EC_PARAMS) ../common/EclibExtra.ec -# $(EASYCRYPT) $(EC_PARAMS) ../common/JWordList.ec -# $(EASYCRYPT) $(EC_PARAMS) properties/Keccakf1600_Spec.ec -# $(EASYCRYPT) $(EC_PARAMS) properties/Keccak1600_Spec.ec -# $(EASYCRYPT) $(EC_PARAMS) properties/Example.ec - -clean: - -rm *.eco diff --git a/fips202/TODO b/fips202/TODO deleted file mode 100644 index e69de29..0000000 diff --git a/fips202/properties/Example.ec b/fips202/properties/Example.ec deleted file mode 100644 index f0d66bd..0000000 --- a/fips202/properties/Example.ec +++ /dev/null @@ -1,96 +0,0 @@ -(* General EC imports *) -require import AllCore List. -from Jasmin require import JModel. -require import Array25 Array32 Array64 Array128 Array168 Array256 Array960 Array1152. - - -require import Keccak1600_Spec. - - -(* XXX: Link to specs of Keccak functions *) -op SHA3_256_32_32 (m: W8.t Array32.t): W8.t Array32.t = - Array32.of_list W8.zero (SHA3_256 (to_list m)). - -(* XXX: Writing input type as "product" is probably terrible for domain separation checking *) -op SHA3_256_1088_32 (m: W8.t Array960.t * W8.t Array128.t): W8.t Array32.t = - Array32.of_list W8.zero (SHA3_256 (to_list m.`1 ++ to_list m.`2)). -(* XXX: same here *) -op SHA3_256_1184_32 (m: W8.t Array1152.t * W8.t Array32.t): W8.t Array32.t = - Array32.of_list W8.zero (SHA3_256 (to_list m.`1 ++ to_list m.`2)). - -op SHA3_512_32_64 (m: W8.t Array32.t): W8.t Array32.t * W8.t Array32.t = - let bs = SHA3_512 (to_list m) - in (Array32.of_list W8.zero (take 32 bs), Array32.of_list W8.zero (drop 32 bs)). -(* XXX: same here *) -op SHA3_512_64_64 (m1 m2: W8.t Array32.t): W8.t Array32.t * W8.t Array32.t = - let bs = SHA3_512 (to_list m1 ++ to_list m2) - in (Array32.of_list W8.zero (take 32 bs), Array32.of_list W8.zero (drop 32 bs)). - - -(* Option I: expose state... *) -op SHAKE128_ABSORB_34 (m: W8.t Array32.t, mi mj: W8.t): W64.t Array25.t = - keccak1600_absorb_op 21 (W8.of_int 31) (to_list m ++ [mi;mj]). -op SHAKE128_SQUEEZE_168 (st: W64.t Array25.t): W64.t Array25.t * W8.t Array168.t = - let st' = KECCAK_F1600 st - in (st', Array168.of_list W8.zero (state_squeeze st' 168)). - -(* Option II: exploit relation between outputs of different lengths *) -(** [SHAKE128_i(m,i)] returns the last 168 bytes of [SHAKE128(m,i*168)] (that is, the ith block) *) -op SHAKE128_i (m: W8.t Array32.t, mi mj: W8.t, cnt: int): W8.t Array168.t = - Array168.of_list W8.zero (drop (168*(cnt-1)) (SHAKE128 (to_list m ++ [mi;mj]) (168*cnt))). - - -(* XXX: same here *) -op SHAKE256_64_32 (m1 m2: W8.t Array32.t): W8.t Array32.t = - Array32.of_list W8.zero (SHAKE256 (to_list m1 ++ to_list m2) 32). -op SHAKE256_33_128 (m: W8.t Array32.t, mj: W8.t): W8.t Array128.t = - Array128.of_list W8.zero (SHAKE256 (to_list m ++ [mj]) 128). - - - -op G_coins = SHA3_512_32_64. -op G_mhpk = SHA3_512_64_64. - -op H_msg = SHA3_256_32_32. -op H_pk = SHA3_256_1184_32. -op H_ct = SHA3_256_1088_32. - -op KDF = SHAKE256_64_32. - -op PRF = SHAKE256_33_128. - - -module type XOF_t = { - proc init(rho : W8.t Array32.t, i j : int) : unit - proc next_bytes() : W8.t Array168.t -}. - -(* Option I *) -module XOF_I : XOF_t = { - var state : W64.t Array25.t - proc init(rho : W8.t Array32.t, i j : int) : unit = { - state <- SHAKE128_ABSORB_34 rho (W8.of_int i) (W8.of_int j); - } - - proc next_bytes() : W8.t Array168.t = { - var buf; - (state,buf) <- SHAKE128_SQUEEZE_168 state; - return buf; - } -}. - -(* Option II *) -module XOF_II : XOF_t = { - var cnt : int - var msg: W8.t list - proc init(rho : W8.t Array32.t, i j : int) : unit = { - cnt <- 0; - msg <- (to_list rho) ++ [W8.of_int i; W8.of_int j]; - } - proc next_bytes() : W8.t Array168.t = { - var buf; - cnt <- cnt + 1; - buf <- SHAKE128_i msg cnt; - return Array168.of_list W8.zero buf; - } -}. diff --git a/fips202/properties/Makefile b/fips202/properties/Makefile deleted file mode 100644 index 5e703ed..0000000 --- a/fips202/properties/Makefile +++ /dev/null @@ -1,12 +0,0 @@ -EASYCRYPT = easycrypt -EC_PARAMS = -I ../../common -I ../ - -.PHONY: clean check - -check: - $(EASYCRYPT) $(EC_PARAMS) Keccakf1600_Spec.ec - $(EASYCRYPT) $(EC_PARAMS) Keccak1600_Spec.ec - $(EASYCRYPT) $(EC_PARAMS) Example.ec - -clean: - -rm *.eco diff --git a/kyber768/.dir-locals.el b/kyber768/.dir-locals.el deleted file mode 100644 index 3b00719..0000000 --- a/kyber768/.dir-locals.el +++ /dev/null @@ -1,4 +0,0 @@ -((easycrypt-mode . - ((eval . - (cl-flet ((pre (s) (concat (locate-dominating-file buffer-file-name ".dir-locals.el") s))) - (setq easycrypt-load-path `(,(pre ".") ,(pre "../common"), (pre "../../common"), (pre "../../../common")))))))) diff --git a/kyber768/Makefile b/kyber768/Makefile deleted file mode 100644 index dd37fe2..0000000 --- a/kyber768/Makefile +++ /dev/null @@ -1,17 +0,0 @@ -EASYCRYPT = easycrypt -EC_PARAMS = -I ../common -I ../fips202 - -.PHONY: clean typecheck - -typecheck: - $(EASYCRYPT) $(EC_PARAMS) GFq.ec - $(EASYCRYPT) $(EC_PARAMS) Rq.ec - $(EASYCRYPT) $(EC_PARAMS) Symmetric.ec - $(EASYCRYPT) $(EC_PARAMS) Sampling.ec - $(EASYCRYPT) $(EC_PARAMS) VecMat.ec - $(EASYCRYPT) $(EC_PARAMS) Serialization.ec - $(EASYCRYPT) $(EC_PARAMS) InnerPKE.ec - $(EASYCRYPT) $(EC_PARAMS) Kyber.ec - -clean: - -rm *.eco diff --git a/kyber768/properties/.dir-locals.el b/kyber768/properties/.dir-locals.el deleted file mode 100644 index 6e5faa9..0000000 --- a/kyber768/properties/.dir-locals.el +++ /dev/null @@ -1,4 +0,0 @@ -((easycrypt-mode . - ((eval . - (cl-flet ((pre (s) (concat (locate-dominating-file buffer-file-name ".dir-locals.el") s))) - (setq easycrypt-load-path `(,(pre ".") ,(pre "../"), (pre "../../common"), (pre "../../../proof/security")))))))) diff --git a/kyber768/properties/Correctness.ec b/kyber768/properties/Correctness.ec index 5fc0d60..57ec891 100644 --- a/kyber768/properties/Correctness.ec +++ b/kyber768/properties/Correctness.ec @@ -48,7 +48,7 @@ by smt(rg_asint). (* Compress-error bound *) op Bq d = round (q%r / (2^(d+1))%r). -lemma nosmt Bq_le_half d: +lemma Bq_le_half d: 0 < d => (q%r / (2^(d+1))%r) <= (q-1)%r/2%r. proof. @@ -60,7 +60,7 @@ rewrite (RField.mulrC (2%r)) invrM;1,2:by smt(lt_pow expr_gt0). by rewrite RField.mulrC (RField.mulrA (q%r)) (RField.mulrC (q%r)) !RField.mulrA /#. qed. -lemma nosmt dvdzN_q_2d (d: int): +lemma dvdzN_q_2d (d: int): 0 < d => q %% 2^d <> 0. proof. @@ -73,7 +73,7 @@ move: (IH HHd); apply contra. by rewrite -!dvdzE /#. qed. -lemma nosmt Bq_noties d: +lemma Bq_noties d: 0 < d => 2^d < q => frac (q%r / (2 ^ (d + 1))%r) <> inv 2%r. @@ -88,24 +88,24 @@ rewrite !mulrA divrr //= frac_div_eq0. by apply dvdzN_q_2d. qed. -lemma nosmt Bq1E: Bq 1 = 832 +lemma Bq1E: Bq 1 = 832 by rewrite /Bq /= round_divz 1:// qE. -lemma nosmt Bq4E: Bq 4 = 104 +lemma Bq4E: Bq 4 = 104 by rewrite /Bq /= round_divz 1:// qE. (* Compression and decompression are used as operations between polynomials over coeff, but we first define the basic operations over coefficients. *) -lemma nosmt comp_bound d x: +lemma comp_bound d x: 0 < d => 2^d < q => x * (2 ^ d)%r / q%r - inv 2%r < (comp d x)%r <= x * (2 ^ d)%r / q%r + inv 2%r. proof. smt(round_bound). qed. -lemma nosmt comp_asint_bound d x: +lemma comp_asint_bound d x: 0 < d => 2^d < q => (asint x)%r * (2 ^ d)%r - q%r / 2%r < q%r * (comp d (asint x)%r)%r @@ -126,7 +126,7 @@ apply (RealOrder.ler_lt_trans ((asint x)%r*(2^d)%r/q%r+ inv 2%r)); first smt(com by rewrite RealOrder.ltr_add2r RealOrder.ltr_pmul2r 1:/# RealOrder.ltr_pmul2r; smt(expr_gt0 rg_asint). qed. -lemma nosmt comp_over d x: +lemma comp_over d x: 0 < d => 2^d < q => comp d (asint x)%r = 2^d @@ -141,7 +141,7 @@ rewrite RealOrder.ler_subl_addl -RealOrder.ler_subl_addr ler_pdivl_mulr. by rewrite exprD_nneg 1..2:/# /= fromintM /#. qed. -lemma nosmt compress0L d x: +lemma compress0L d x: 0 < d => 2^d < q => q%r - q%r / (2^(d+1))%r <= (asint x)%r => @@ -153,7 +153,7 @@ have ->: comp d (asint x)%r = 2^d. by rewrite modzz. qed. -lemma nosmt compress_small d x: +lemma compress_small d x: 0 < d => 2^d < q => (asint x)%r < q%r - q%r / (2^(d+1))%r => @@ -167,7 +167,7 @@ have ?: comp d (asint x)%r <> 2^d by rewrite comp_over // /#. smt(comp_asint_range). qed. -lemma nosmt compress1_is0 x: +lemma compress1_is0 x: compress 1 x = 0 <=> absZq x <= Bq 1. proof. have L: forall y m, 0 <= y <= m => y %% m = 0 <=> y=0 \/ y=m. diff --git a/kyber768/properties/KyberLib.ec b/kyber768/properties/KyberLib.ec index 01c0513..a82d2de 100644 --- a/kyber768/properties/KyberLib.ec +++ b/kyber768/properties/KyberLib.ec @@ -16,11 +16,11 @@ rewrite (floorE (x+floor y)) //. smt(floor_bound). qed. -lemma nosmt le_floorE n x: +lemma le_floorE n x: (n <= floor x) = (n%r <= x) by smt(floor_bound). -lemma nosmt floor_ltE x n: +lemma floor_ltE x n: (floor x < n) = (x < n%r) by smt(floor_bound). @@ -137,16 +137,16 @@ lemma round_bound x: x - inv(2%r) < (round x)%r <= x + inv(2%r) by smt(floor_bound). -lemma nosmt le_roundE n x: +lemma le_roundE n x: (n <= round x) = (n%r <= x + inv 2%r) by smt(le_floorE). -lemma nosmt round_ltE x n: +lemma round_ltE x n: (round x < n) = (x + inv 2%r < n%r) by smt(floor_ltE). -lemma nosmt roundN x: +lemma roundN x: frac x <> inv 2%r => round (-x) = -round x. proof. move => H. diff --git a/ml-kem/properties/Correctness.ec b/ml-kem/properties/Correctness.ec index 1f9a04f..a395896 100644 --- a/ml-kem/properties/Correctness.ec +++ b/ml-kem/properties/Correctness.ec @@ -48,7 +48,7 @@ by smt(rg_asint). (* Compress-error bound *) op Bq d = round (q%r / (2^(d+1))%r). -lemma nosmt Bq_le_half d: +lemma Bq_le_half d: 0 < d => (q%r / (2^(d+1))%r) <= (q-1)%r/2%r. proof. @@ -60,7 +60,7 @@ rewrite (RField.mulrC (2%r)) invrM;1,2:by smt(lt_pow expr_gt0). by rewrite RField.mulrC (RField.mulrA (q%r)) (RField.mulrC (q%r)) !RField.mulrA /#. qed. -lemma nosmt dvdzN_q_2d (d: int): +lemma dvdzN_q_2d (d: int): 0 < d => q %% 2^d <> 0. proof. @@ -73,7 +73,7 @@ move: (IH HHd); apply contra. by rewrite -!dvdzE /#. qed. -lemma nosmt Bq_noties d: +lemma Bq_noties d: 0 < d => 2^d < q => frac (q%r / (2 ^ (d + 1))%r) <> inv 2%r. @@ -88,24 +88,24 @@ rewrite !mulrA divrr //= frac_div_eq0. by apply dvdzN_q_2d. qed. -lemma nosmt Bq1E: Bq 1 = 832 +lemma Bq1E: Bq 1 = 832 by rewrite /Bq /= round_divz 1:// qE. -lemma nosmt Bq4E: Bq 4 = 104 +lemma Bq4E: Bq 4 = 104 by rewrite /Bq /= round_divz 1:// qE. (* Compression and decompression are used as operations between polynomials over coeff, but we first define the basic operations over coefficients. *) -lemma nosmt comp_bound d x: +lemma comp_bound d x: 0 < d => 2^d < q => x * (2 ^ d)%r / q%r - inv 2%r < (comp d x)%r <= x * (2 ^ d)%r / q%r + inv 2%r. proof. smt(round_bound). qed. -lemma nosmt comp_asint_bound d x: +lemma comp_asint_bound d x: 0 < d => 2^d < q => (asint x)%r * (2 ^ d)%r - q%r / 2%r < q%r * (comp d (asint x)%r)%r @@ -126,7 +126,7 @@ apply (RealOrder.ler_lt_trans ((asint x)%r*(2^d)%r/q%r+ inv 2%r)); first smt(com by rewrite RealOrder.ltr_add2r RealOrder.ltr_pmul2r 1:/# RealOrder.ltr_pmul2r; smt(expr_gt0 rg_asint). qed. -lemma nosmt comp_over d x: +lemma comp_over d x: 0 < d => 2^d < q => comp d (asint x)%r = 2^d @@ -141,7 +141,7 @@ rewrite RealOrder.ler_subl_addl -RealOrder.ler_subl_addr ler_pdivl_mulr. by rewrite exprD_nneg 1..2:/# /= fromintM /#. qed. -lemma nosmt compress0L d x: +lemma compress0L d x: 0 < d => 2^d < q => q%r - q%r / (2^(d+1))%r <= (asint x)%r => @@ -153,7 +153,7 @@ have ->: comp d (asint x)%r = 2^d. by rewrite modzz. qed. -lemma nosmt compress_small d x: +lemma compress_small d x: 0 < d => 2^d < q => (asint x)%r < q%r - q%r / (2^(d+1))%r => @@ -167,7 +167,7 @@ have ?: comp d (asint x)%r <> 2^d by rewrite comp_over // /#. smt(comp_asint_range). qed. -lemma nosmt compress1_is0 x: +lemma compress1_is0 x: compress 1 x = 0 <=> absZq x <= Bq 1. proof. have L: forall y m, 0 <= y <= m => y %% m = 0 <=> y=0 \/ y=m. diff --git a/ml-kem/properties/MLKEMLib.ec b/ml-kem/properties/MLKEMLib.ec index fc6164e..e2b4eb8 100644 --- a/ml-kem/properties/MLKEMLib.ec +++ b/ml-kem/properties/MLKEMLib.ec @@ -16,11 +16,11 @@ rewrite (floorE (x+floor y)) //. smt(floor_bound). qed. -lemma nosmt le_floorE n x: +lemma le_floorE n x: (n <= floor x) = (n%r <= x) by smt(floor_bound). -lemma nosmt floor_ltE x n: +lemma floor_ltE x n: (floor x < n) = (x < n%r) by smt(floor_bound). @@ -138,16 +138,16 @@ lemma round_bound x: x - inv(2%r) < (round x)%r <= x + inv(2%r) by smt(floor_bound). -lemma nosmt le_roundE n x: +lemma le_roundE n x: (n <= round x) = (n%r <= x + inv 2%r) by smt(le_floorE). -lemma nosmt round_ltE x n: +lemma round_ltE x n: (round x < n) = (x + inv 2%r < n%r) by smt(floor_ltE). -lemma nosmt roundN x: +lemma roundN x: frac x <> inv 2%r => round (-x) = -round x. proof. move => H. diff --git a/xmss/.dir-locals.el b/xmss/.dir-locals.el deleted file mode 100644 index 3b00719..0000000 --- a/xmss/.dir-locals.el +++ /dev/null @@ -1,4 +0,0 @@ -((easycrypt-mode . - ((eval . - (cl-flet ((pre (s) (concat (locate-dominating-file buffer-file-name ".dir-locals.el") s))) - (setq easycrypt-load-path `(,(pre ".") ,(pre "../common"), (pre "../../common"), (pre "../../../common")))))))) diff --git a/xmss/Makefile b/xmss/Makefile deleted file mode 100644 index 771f14e..0000000 --- a/xmss/Makefile +++ /dev/null @@ -1,11 +0,0 @@ -EASYCRYPT = easycrypt -EC_PARAMS = -I ../common - -.PHONY: clean typecheck - -typecheck: - $(EASYCRYPT) $(EC_PARAMS) Notation.ec - $(EASYCRYPT) $(EC_PARAMS) Primitives.ec - -clean: - -rm *.eco