From 6ccce870143a57a06759d40244f934a02b482607 Mon Sep 17 00:00:00 2001 From: akshaya Date: Wed, 9 Apr 2025 23:57:59 +0200 Subject: [PATCH 1/2] RSA--Kyber Sha256withRSA -- Dilithium --- BouncyCastle-JCA/src/KeyPairGenerator.crysl | 8 ++++---- BouncyCastle-JCA/src/SecureRandom.crysl | 10 ++++++++++ BouncyCastle-JCA/src/Signature.crysl | 2 +- 3 files changed, 15 insertions(+), 5 deletions(-) diff --git a/BouncyCastle-JCA/src/KeyPairGenerator.crysl b/BouncyCastle-JCA/src/KeyPairGenerator.crysl index 163a8902..316aaa70 100644 --- a/BouncyCastle-JCA/src/KeyPairGenerator.crysl +++ b/BouncyCastle-JCA/src/KeyPairGenerator.crysl @@ -15,6 +15,7 @@ EVENTS i2: initialize(keysize, _); i3: initialize(params); i4: initialize(params, _); + i5: initialize(java.security.spec.AlgorithmParameterSpec, java.security.SecureRandom) Init := i1 | i2 | i3 | i4; k1: keyPair = generateKeyPair(); @@ -25,18 +26,17 @@ ORDER Get, Init, Gen CONSTRAINTS - algorithm in {"RSA", "DSA", "DiffieHellman", "DH", "EC", "ECDSA", "ECDH", "ECDHWITHSHA1KDF", "ECDHC", + algorithm in {"Kyber", "DSA", "DiffieHellman", "DH", "EC", "ECDSA", "ECDH", "ECDHWITHSHA1KDF", "ECDHC", "ECIES", "ElGamal", "McElieceKobaraImai", "McEliecePointcheval", "McElieceFujisaki", "McEliece", "McEliece-CCA2", "NH", "QTESLA", "Rainbow", "SPHINCS256", "XMSS", "XMSSMT"}; - algorithm in {"RSA"} => keysize in {4096, 3072}; //BSI TR-02102-1 Recommends atleast 3000bits for keys + algorithm in {"Kyber"} => keysize in {4096, 3072}; //BSI TR-02102-1 Recommends atleast 3000bits for keys algorithm in {"DSA"} => keysize in {3072}; algorithm in {"DiffieHellman", "DH"} => keysize in {3072}; algorithm in {"EC", "ECDSA", "ECDH", "ECDHWITHSHA1KDF", "ECDHC", "ECIES"} => keysize in {256}; REQUIRES - algorithm in {"RSA"} => preparedRSA[params]; - algorithm in {"DSA"} => preparedDSA[params]; + algorithm in {"Kyber"} => preparedKyber[params]; algorithm in {"DSA"} => preparedDSA[params]; algorithm in {"DiffieHellman", "DH"} => preparedDH[params]; algorithm in {"EC"} => preparedEC[params]; diff --git a/BouncyCastle-JCA/src/SecureRandom.crysl b/BouncyCastle-JCA/src/SecureRandom.crysl index 027ebee5..39fdc50f 100644 --- a/BouncyCastle-JCA/src/SecureRandom.crysl +++ b/BouncyCastle-JCA/src/SecureRandom.crysl @@ -40,6 +40,16 @@ ORDER CONSTRAINTS algorithm in {"DEFAULT", "NONCEANDIV"}; + newSecureRandom = + s.() + OR + s.(byte[]) + OR + java.security.SecureRandom.getInstance("DRBG") + OR + java.security.SecureRandom.getInstanceStrong() + + nextBytes = s.nextBytes(byte[]) REQUIRES randomized[seed]; diff --git a/BouncyCastle-JCA/src/Signature.crysl b/BouncyCastle-JCA/src/Signature.crysl index 4d72bdeb..705d9223 100644 --- a/BouncyCastle-JCA/src/Signature.crysl +++ b/BouncyCastle-JCA/src/Signature.crysl @@ -47,7 +47,7 @@ ORDER CONSTRAINTS algorithm in {"ECDDSA", "SHA256WITHECDDSA", "SHA384WITHECDDSA", "SHA512WITHECDDSA", "SHA3-256WITHECDDSA", "SHA3-384WITHECDDSA", "SHA3-512WITHECDDSA", "SHA256WITHECNR", "SHA384WITHECNR", "SHA512WITHECNR", "SHA256withECDSA", "SHA256withDSA", - "SHA384withRSA", "SHA512withRSA", "SHA256withRSA", "SHA384withDSA", "SHA512withDSA", + "SHA384withRSA", "SHA512withRSA", "Dilithium", "SHA384withDSA", "SHA512withDSA", "QTESLA"}; length[input] >= offset + len; offset >= 0; From a470d03bde994feb8a0be3e0355f76efe23ebfe0 Mon Sep 17 00:00:00 2001 From: akshaya Date: Thu, 17 Apr 2025 14:58:21 +0200 Subject: [PATCH 2/2] BSI key Length specification and DH,GCM parameter modification --- BouncyCastle-JCA/src/DHParameterSpec.crysl | 13 ++++++------- BouncyCastle-JCA/src/GCMParameterSpec.crysl | 5 ++++- BouncyCastle-JCA/src/IvParameterSpec.crysl | 1 + BouncyCastle-JCA/src/KeyAgreement.crysl | 8 ++++++-- BouncyCastle-JCA/src/KeyGenerator.crysl | 2 +- BouncyCastle-JCA/src/KeyPairGenerator.crysl | 17 +++++++++-------- .../src/RSAKeyGenParameterSpec.crysl | 2 +- BouncyCastle-JCA/src/SecureRandom.crysl | 10 +--------- BouncyCastle-JCA/src/Signature.crysl | 2 +- .../src/PaddedBufferedBlockCipher.crysl | 2 ++ .../src/KeyPairGenerator.crysl | 15 +++++++++------ .../src/RSAKeyGenParameterSpec.crysl | 2 +- Tink/src/AeadKeyTemplates.crysl | 2 +- Tink/src/MacKeyTemplates.crysl | 2 +- 14 files changed, 44 insertions(+), 39 deletions(-) diff --git a/BouncyCastle-JCA/src/DHParameterSpec.crysl b/BouncyCastle-JCA/src/DHParameterSpec.crysl index 62255957..397efb0e 100644 --- a/BouncyCastle-JCA/src/DHParameterSpec.crysl +++ b/BouncyCastle-JCA/src/DHParameterSpec.crysl @@ -1,22 +1,21 @@ SPEC javax.crypto.spec.DHParameterSpec -OBJECTS +OBJECTS java.math.BigInteger p; java.math.BigInteger g; int l; - + EVENTS c1: DHParameterSpec(p, g); c2: DHParameterSpec(p, g, l); Con := c1 | c2; - + ORDER Con CONSTRAINTS - p >= 1^2048; - g >= 1^2048; - + bitlength(p) >= 3000;// Choose an element g ∈ F∗ p withord(g) primeandq := ord(g) ≄ 2^250 + bitlength(g) >= 250; + ENSURES preparedDH[this]; - \ No newline at end of file diff --git a/BouncyCastle-JCA/src/GCMParameterSpec.crysl b/BouncyCastle-JCA/src/GCMParameterSpec.crysl index 05815af1..b4cbd121 100644 --- a/BouncyCastle-JCA/src/GCMParameterSpec.crysl +++ b/BouncyCastle-JCA/src/GCMParameterSpec.crysl @@ -5,6 +5,7 @@ OBJECTS byte[] src; int offset; int len; + byte[] iv; EVENTS c1: GCMParameterSpec(tagLen, src); @@ -15,10 +16,12 @@ ORDER Con CONSTRAINTS - tagLen in {96, 104, 112, 120, 128}; + tagLen in {96, 104, 112, 120, 128};//GCM with a length of the GCM tags of at least 96 bits should be used. length[src] >= offset + len; offset >= 0; len > 0; + length[iv] == 12; + unique[iv] // initiallization vector should not be repeated over the entire lifetime of a key REQUIRES randomized[src]; diff --git a/BouncyCastle-JCA/src/IvParameterSpec.crysl b/BouncyCastle-JCA/src/IvParameterSpec.crysl index 00ae5c04..8e5881ab 100644 --- a/BouncyCastle-JCA/src/IvParameterSpec.crysl +++ b/BouncyCastle-JCA/src/IvParameterSpec.crysl @@ -17,6 +17,7 @@ CONSTRAINTS length[iv] >= offset + len; offset >= 0; len > 0; + unique[iv] REQUIRES randomized[iv]; diff --git a/BouncyCastle-JCA/src/KeyAgreement.crysl b/BouncyCastle-JCA/src/KeyAgreement.crysl index 512efe22..94cb9c91 100644 --- a/BouncyCastle-JCA/src/KeyAgreement.crysl +++ b/BouncyCastle-JCA/src/KeyAgreement.crysl @@ -37,15 +37,19 @@ ORDER Get, Init, DoPhase, (GenSecret | GenSecretBuffer) CONSTRAINTS - algorithm in {"DH", "DiffieHellman", "NH" ,"ECDH", "ECDHC"}; + algorithm in {"DH","DiffieHellman","ECDH","NH", "ECDHC"}; + keyLength>=3000; + curveBits>= 250; symmetricKeyAlgorithm in {"AES", "HmacSHA256", "HmacSHA384", "HmacSHA512", "HMACSHA3-256", "HMACSHA3-384", "HMACSHA3-512"}; + tagLength>=96 + REQUIRES randomized[random]; generatedPrivkey[privKey]; generatedPubkey[pubKey]; - algorithm in {"DiffieHellman", "DH"} => preparedDH[params]; + algorithm in {"DiffieHellman","DH"} => preparedDH[params]; algorithm in {"ECDH", "ECDHC"} => preparedEC[params]; ENSURES diff --git a/BouncyCastle-JCA/src/KeyGenerator.crysl b/BouncyCastle-JCA/src/KeyGenerator.crysl index 67341cd4..ecdad5b2 100644 --- a/BouncyCastle-JCA/src/KeyGenerator.crysl +++ b/BouncyCastle-JCA/src/KeyGenerator.crysl @@ -32,7 +32,7 @@ CONSTRAINTS "Twofish", "Poly1305-Twofish", "XSalsa20"}; algorithm in {"AES", "Poly1305-Camellia", "Camellia", "ChaCha", "Salsa20", "SHACAL-2", "Shacal2", "Rijndael", "Serpent", "Tnepres", "ChaCha7539", "Poly1305", "Poly1305-Serpent", - "Twofish", "Poly1305-Twofish", "XSalsa20"} => keysize in {128, 192, 256}; + "Twofish", "Poly1305-Twofish", "XSalsa20"} => keysize >= 128; REQUIRES randomized[random]; diff --git a/BouncyCastle-JCA/src/KeyPairGenerator.crysl b/BouncyCastle-JCA/src/KeyPairGenerator.crysl index 316aaa70..d828b0a8 100644 --- a/BouncyCastle-JCA/src/KeyPairGenerator.crysl +++ b/BouncyCastle-JCA/src/KeyPairGenerator.crysl @@ -16,7 +16,7 @@ EVENTS i3: initialize(params); i4: initialize(params, _); i5: initialize(java.security.spec.AlgorithmParameterSpec, java.security.SecureRandom) - Init := i1 | i2 | i3 | i4; + Init := i1 | i2 | i3 | i4 | i5; k1: keyPair = generateKeyPair(); k2: keyPair = genKeyPair(); @@ -26,17 +26,18 @@ ORDER Get, Init, Gen CONSTRAINTS - algorithm in {"Kyber", "DSA", "DiffieHellman", "DH", "EC", "ECDSA", "ECDH", "ECDHWITHSHA1KDF", "ECDHC", + algorithm in {"RSA", "DSA", "DiffieHellman", "DH", "EC", "ECDSA", "ECDH", "ECDHWITHSHA1KDF", "ECDHC", "ECIES", "ElGamal", "McElieceKobaraImai", "McEliecePointcheval", "McElieceFujisaki", "McEliece", "McEliece-CCA2", "NH", "QTESLA", "Rainbow", "SPHINCS256", "XMSS", "XMSSMT"}; - algorithm in {"Kyber"} => keysize in {4096, 3072}; //BSI TR-02102-1 Recommends atleast 3000bits for keys - algorithm in {"DSA"} => keysize in {3072}; - algorithm in {"DiffieHellman", "DH"} => keysize in {3072}; - algorithm in {"EC", "ECDSA", "ECDH", "ECDHWITHSHA1KDF", "ECDHC", "ECIES"} => keysize in {256}; - + algorithm in {"RSA"} => keysize >= 3000; //BSI TR-02102-1 Recommends atleast 3000bits for keys + algorithm in {"DSA"} => keysize >= 3072; + algorithm in {"DiffieHellman", "DH"} => keysize >= 3000; + algorithm in {"EC", "ECDSA", "ECDH", "ECDHWITHSHA1KDF", "ECDHC", "ECIES"} => keysize >= 320; + algorithm in {"DSA"} && afterYear >= 2029 => false;//# DSA deprecated after 2029 + REQUIRES - algorithm in {"Kyber"} => preparedKyber[params]; algorithm in {"DSA"} => preparedDSA[params]; + algorithm in {"RSA"} => preparedRSA[params]; algorithm in {"DSA"} => preparedDSA[params]; algorithm in {"DiffieHellman", "DH"} => preparedDH[params]; algorithm in {"EC"} => preparedEC[params]; diff --git a/BouncyCastle-JCA/src/RSAKeyGenParameterSpec.crysl b/BouncyCastle-JCA/src/RSAKeyGenParameterSpec.crysl index d357e50d..3e66bf8f 100644 --- a/BouncyCastle-JCA/src/RSAKeyGenParameterSpec.crysl +++ b/BouncyCastle-JCA/src/RSAKeyGenParameterSpec.crysl @@ -12,7 +12,7 @@ ORDER Con CONSTRAINTS - keysize in {4096}; //BSI TR-02102-1 Recommends atleast 3000bits for keys + keysize >= 3000; //BSI TR-02102-1 Recommends atleast 3000bits for keys publicExponent in {65537}; ENSURES diff --git a/BouncyCastle-JCA/src/SecureRandom.crysl b/BouncyCastle-JCA/src/SecureRandom.crysl index 39fdc50f..a5e3a934 100644 --- a/BouncyCastle-JCA/src/SecureRandom.crysl +++ b/BouncyCastle-JCA/src/SecureRandom.crysl @@ -40,16 +40,8 @@ ORDER CONSTRAINTS algorithm in {"DEFAULT", "NONCEANDIV"}; - newSecureRandom = - s.() - OR - s.(byte[]) - OR - java.security.SecureRandom.getInstance("DRBG") - OR - java.security.SecureRandom.getInstanceStrong() - nextBytes = s.nextBytes(byte[]) + REQUIRES randomized[seed]; diff --git a/BouncyCastle-JCA/src/Signature.crysl b/BouncyCastle-JCA/src/Signature.crysl index 705d9223..e688984a 100644 --- a/BouncyCastle-JCA/src/Signature.crysl +++ b/BouncyCastle-JCA/src/Signature.crysl @@ -47,7 +47,7 @@ ORDER CONSTRAINTS algorithm in {"ECDDSA", "SHA256WITHECDDSA", "SHA384WITHECDDSA", "SHA512WITHECDDSA", "SHA3-256WITHECDDSA", "SHA3-384WITHECDDSA", "SHA3-512WITHECDDSA", "SHA256WITHECNR", "SHA384WITHECNR", "SHA512WITHECNR", "SHA256withECDSA", "SHA256withDSA", - "SHA384withRSA", "SHA512withRSA", "Dilithium", "SHA384withDSA", "SHA512withDSA", + "SHA384withRSA", "SHA512withRSA", "SHA256withRSA", "SHA384withDSA", "SHA512withDSA", "QTESLA"}; length[input] >= offset + len; offset >= 0; diff --git a/BouncyCastle/src/PaddedBufferedBlockCipher.crysl b/BouncyCastle/src/PaddedBufferedBlockCipher.crysl index b4e7d6b0..b6d8cee6 100644 --- a/BouncyCastle/src/PaddedBufferedBlockCipher.crysl +++ b/BouncyCastle/src/PaddedBufferedBlockCipher.crysl @@ -39,6 +39,8 @@ CONSTRAINTS plainTextOffset >= 0; plainTextLen > 0; cipherTextOffset >= 0; + + padding in {ISO, Padding58,ESP}// BSI recoomedation for padding Scheme (ISO-Padding, Padding according to [58], ESP-Padding) REQUIRES generatedRijndaelEngine[cipher]; diff --git a/JavaCryptographicArchitecture/src/KeyPairGenerator.crysl b/JavaCryptographicArchitecture/src/KeyPairGenerator.crysl index eba3b955..5c62b293 100644 --- a/JavaCryptographicArchitecture/src/KeyPairGenerator.crysl +++ b/JavaCryptographicArchitecture/src/KeyPairGenerator.crysl @@ -25,16 +25,19 @@ ORDER Get, Init, Gen CONSTRAINTS - algorithm in {"RSA", "EC", "DSA", "DiffieHellman", "DH"}; //BSI TR-02102-1 Recommends atleast 3000bits for keys - algorithm in {"RSA"} => keysize in {4096, 3072}; - algorithm in {"DSA"} => keysize in {3072}; - algorithm in {"DiffieHellman", "DH"} => keysize in {3072}; - algorithm in {"EC"} => keysize in {256}; + algorithm in {"RSA", "EC", "DSA", "DiffieHellman", "DH"}; + algorithm in {"RSA"} => keysize >=3000; + algorithm in {"DSA"} => keysize >= 3072; + algorithm in {"DiffieHellman", "DH"} => keysize >=3000; + algorithm in {"EC"} => keysize >=250; + +FORBIDDEN + algorithm =="DSA" && afterYear>=2029; REQUIRES algorithm in {"RSA"} => preparedRSA[params]; algorithm in {"DSA"} => preparedDSA[params]; - algorithm in {"DiffieHellman", "DH"} => preparedDH[params]; + algorithm in {"DiffieHellman","DH"} => preparedDH[params]; algorithm in {"EC"} => preparedEC[params]; ENSURES diff --git a/JavaCryptographicArchitecture/src/RSAKeyGenParameterSpec.crysl b/JavaCryptographicArchitecture/src/RSAKeyGenParameterSpec.crysl index ada8f2da..3e66bf8f 100644 --- a/JavaCryptographicArchitecture/src/RSAKeyGenParameterSpec.crysl +++ b/JavaCryptographicArchitecture/src/RSAKeyGenParameterSpec.crysl @@ -12,7 +12,7 @@ ORDER Con CONSTRAINTS - keysize in {3072, 4096}; //BSI TR-02102-1 Recommends atleast 3000bits for keys + keysize >= 3000; //BSI TR-02102-1 Recommends atleast 3000bits for keys publicExponent in {65537}; ENSURES diff --git a/Tink/src/AeadKeyTemplates.crysl b/Tink/src/AeadKeyTemplates.crysl index 678ad135..e26b80d2 100644 --- a/Tink/src/AeadKeyTemplates.crysl +++ b/Tink/src/AeadKeyTemplates.crysl @@ -28,7 +28,7 @@ OBJECTS int key; int iv; - com.google.crypto.tink.proto.HashType hashType; // HashType enum: (1) - SHA1, (3) - SHA256, and (4) - SHA 512. + com.google.crypto.tink.proto.HashType hashType; // HashType enum: (1) - SHA2, (3) - SHA256, and (4) - SHA 512. EVENTS aes_gcm_evt : kt = createAesGcmKeyTemplate(key); diff --git a/Tink/src/MacKeyTemplates.crysl b/Tink/src/MacKeyTemplates.crysl index c931089a..4da78418 100644 --- a/Tink/src/MacKeyTemplates.crysl +++ b/Tink/src/MacKeyTemplates.crysl @@ -22,7 +22,7 @@ OBJECTS int key; int tag; - int hashType; // HashType enum: (1) - SHA1, (3) - SHA256, and (4) - SHA 512. + int hashType; // HashType enum: (1) - SHA2, (3) - SHA256, and (4) - SHA 512. EVENTS hmac_sha256_evt : hmac_sha256 = createHmacKeyTemplate(key, tag, _);