Skip to content

BSI Adherance #247

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 2 commits into
base: master
Choose a base branch
from
Draft

BSI Adherance #247

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
6ccce87
RSA--Kyber
Akshayaquinnox Apr 9, 2025
a470d03
BSI key Length specification and DH,GCM parameter modification
Akshayaquinnox Apr 17, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 6 additions & 7 deletions BouncyCastle-JCA/src/DHParameterSpec.crysl
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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;
Copy link
Contributor

@smeyer198 smeyer198 Apr 28, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We don't have a predefined predicate bitlength...


ENSURES
preparedDH[this];

5 changes: 4 additions & 1 deletion BouncyCastle-JCA/src/GCMParameterSpec.crysl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ OBJECTS
byte[] src;
int offset;
int len;
byte[] iv;

EVENTS
c1: GCMParameterSpec(tagLen, src);
Expand All @@ -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;
Copy link
Contributor

@smeyer198 smeyer198 Apr 28, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

iv is not used in any event, i.e. this constraint is just dead. If I understand it correctly, src is the IV where we have a length constraint. Is this constraint sufficient?

unique[iv] // initiallization vector should not be repeated over the entire lifetime of a key
Copy link
Contributor

@smeyer198 smeyer198 Apr 28, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We don't have a predefined predicate unique... It would maybe be possible to add it to the REQUIRES section, then we need a corresponding part in the ENSURES section for a class that can generate an IV


REQUIRES
randomized[src];
Expand Down
1 change: 1 addition & 0 deletions BouncyCastle-JCA/src/IvParameterSpec.crysl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ CONSTRAINTS
length[iv] >= offset + len;
offset >= 0;
len > 0;
unique[iv]
Copy link
Contributor

@smeyer198 smeyer198 Apr 28, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We don't have a predefined predicate unique... It would maybe be possible to add it to the REQUIRES section, then we need a corresponding part in the ENSURES section for a class that can generate an IV


REQUIRES
randomized[iv];
Expand Down
8 changes: 6 additions & 2 deletions BouncyCastle-JCA/src/KeyAgreement.crysl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Copy link
Contributor

@smeyer198 smeyer198 Apr 28, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

keyLength, curveBits and tagLength are not defined or used in any EVENT. Hence, these constraints are not valid



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
Expand Down
2 changes: 1 addition & 1 deletion BouncyCastle-JCA/src/KeyGenerator.crysl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Copy link
Contributor

@smeyer198 smeyer198 Apr 28, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

AFAIK, the JCA supports only key sizes of 128, 192 and 256. In all other cases, it throws an exception. Hence, we should keep the explicit key sizes


REQUIRES
randomized[random];
Expand Down
19 changes: 10 additions & 9 deletions BouncyCastle-JCA/src/KeyPairGenerator.crysl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,8 @@ EVENTS
i2: initialize(keysize, _);
i3: initialize(params);
i4: initialize(params, _);
Init := i1 | i2 | i3 | i4;
i5: initialize(java.security.spec.AlgorithmParameterSpec, java.security.SecureRandom)
Init := i1 | i2 | i3 | i4 | i5;
Copy link
Contributor

@smeyer198 smeyer198 Apr 28, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This does not work, because i5 is already covered by i4. We can update i4 to add a SecureRandom parameter instead of blank, then we would probably need an additional constraint randomized[random] too


k1: keyPair = generateKeyPair();
k2: keyPair = genKeyPair();
Expand All @@ -25,18 +26,18 @@ ORDER
Get, Init, Gen

CONSTRAINTS
algorithm in {"RSA", "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 {"RSA"} => 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;
Copy link
Contributor

@smeyer198 smeyer198 Apr 28, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

See above. We should keep explicit key sizes

algorithm in {"DSA"} && afterYear >= 2029 => false;//# DSA deprecated after 2029
Copy link
Contributor

@smeyer198 smeyer198 Apr 28, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What is afterYear?


REQUIRES
algorithm in {"RSA"} => preparedRSA[params];
algorithm in {"DSA"} => preparedDSA[params];
algorithm in {"RSA"} => preparedRSA[params]; algorithm in {"DSA"} => preparedDSA[params];
Copy link
Contributor

@smeyer198 smeyer198 Apr 28, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wrong inlining

algorithm in {"DiffieHellman", "DH"} => preparedDH[params];
algorithm in {"EC"} => preparedEC[params];

Expand Down
2 changes: 1 addition & 1 deletion BouncyCastle-JCA/src/RSAKeyGenParameterSpec.crysl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Copy link
Contributor

@smeyer198 smeyer198 Apr 28, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Keep explicit key sizes

publicExponent in {65537};

ENSURES
Expand Down
2 changes: 2 additions & 0 deletions BouncyCastle-JCA/src/SecureRandom.crysl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,8 @@ ORDER

CONSTRAINTS
algorithm in {"DEFAULT", "NONCEANDIV"};



REQUIRES
randomized[seed];
Expand Down
2 changes: 1 addition & 1 deletion BouncyCastle-JCA/src/Signature.crysl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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", "SHA256withRSA", "SHA384withDSA", "SHA512withDSA",
"QTESLA"};
length[input] >= offset + len;
offset >= 0;
Expand Down
2 changes: 2 additions & 0 deletions BouncyCastle/src/PaddedBufferedBlockCipher.crysl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Copy link
Contributor

@smeyer198 smeyer198 Apr 28, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

padding is never defined


REQUIRES
generatedRijndaelEngine[cipher];
Expand Down
15 changes: 9 additions & 6 deletions JavaCryptographicArchitecture/src/KeyPairGenerator.crysl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Copy link
Contributor

@smeyer198 smeyer198 Apr 28, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Keep exlicit key sizes


FORBIDDEN
algorithm =="DSA" && afterYear>=2029;
Copy link
Contributor

@smeyer198 smeyer198 Apr 28, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

FORBIDDEN can only hold events


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
Expand Down
2 changes: 1 addition & 1 deletion JavaCryptographicArchitecture/src/RSAKeyGenParameterSpec.crysl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Copy link
Contributor

@smeyer198 smeyer198 Apr 28, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Keep explicit key sizes

publicExponent in {65537};

ENSURES
Expand Down
2 changes: 1 addition & 1 deletion Tink/src/AeadKeyTemplates.crysl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
2 changes: 1 addition & 1 deletion Tink/src/MacKeyTemplates.crysl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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, _);
Expand Down