Skip to content

Conversation

@Akshayaquinnox
Copy link

No description provided.

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

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...

length[src] >= offset + len;
offset >= 0;
len > 0;
length[iv] == 12;
Copy link
Contributor

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?

offset >= 0;
len > 0;
length[iv] == 12;
unique[iv] // initiallization vector should not be repeated over the entire lifetime of a key
Copy link
Contributor

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

length[iv] >= offset + len;
offset >= 0;
len > 0;
unique[iv]
Copy link
Contributor

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

curveBits>= 250;
symmetricKeyAlgorithm in {"AES", "HmacSHA256", "HmacSHA384", "HmacSHA512",
"HMACSHA3-256", "HMACSHA3-384", "HMACSHA3-512"};
tagLength>=96
Copy link
Contributor

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


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

Choose a reason for hiding this comment

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

Keep explicit key sizes

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

Choose a reason for hiding this comment

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

padding is never defined

algorithm in {"RSA"} => keysize >=3000;
algorithm in {"DSA"} => keysize >= 3072;
algorithm in {"DiffieHellman", "DH"} => keysize >=3000;
algorithm in {"EC"} => keysize >=250;
Copy link
Contributor

Choose a reason for hiding this comment

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

Keep exlicit key sizes

algorithm in {"EC"} => keysize >=250;

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

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


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

Choose a reason for hiding this comment

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

Keep explicit key sizes

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants