@@ -582,6 +582,28 @@ module CryptographyBase<LocationSig Location, InputSig<Location> Input> {
582
582
}
583
583
}
584
584
585
+ predicate fixedImplicitCipherKeySize ( TAlgorithm type , int size ) {
586
+ type = TSymmetricCipher ( DES ( ) ) and size = 56
587
+ or
588
+ type = TSymmetricCipher ( DESX ( ) ) and size = 184
589
+ or
590
+ type = TSymmetricCipher ( DoubleDES ( ) ) and size = 112
591
+ or
592
+ type = TSymmetricCipher ( TripleDES ( ) ) and size = 168
593
+ or
594
+ type = TSymmetricCipher ( CHACHA20 ( ) ) and size = 256
595
+ or
596
+ type = TSymmetricCipher ( IDEA ( ) ) and size = 128
597
+ or
598
+ type = TSymmetricCipher ( KUZNYECHIK ( ) ) and size = 256
599
+ or
600
+ type = TSymmetricCipher ( MAGMA ( ) ) and size = 256
601
+ or
602
+ type = TSymmetricCipher ( SM4 ( ) ) and size = 128
603
+ or
604
+ type = TSymmetricCipher ( SEED ( ) ) and size = 128
605
+ }
606
+
585
607
bindingset [ type]
586
608
predicate symmetric_cipher_to_name_and_structure (
587
609
TSymmetricCipherType type , string name , CipherStructureType s
@@ -790,6 +812,10 @@ module CryptographyBase<LocationSig Location, InputSig<Location> Input> {
790
812
* If a specific key size is unknown, this predicate should be implemented as `none()`.
791
813
*
792
814
* If the algorithm accepts a range of key sizes without a particular one specified, this predicate should be implemented as `none()`.
815
+ *
816
+ * NOTE: if the algorithm has a single key size, the implicit key size does not need to be modeled.
817
+ * This will be automatically inferred and applied at the node level.
818
+ * See `fixedImplicitCipherKeySize`.
793
819
*/
794
820
abstract string getKeySizeFixed ( ) ;
795
821
@@ -2178,7 +2204,14 @@ module CryptographyBase<LocationSig Location, InputSig<Location> Input> {
2178
2204
/**
2179
2205
* Gets the key size variant of this algorithm in bits, e.g., 128 for "AES-128".
2180
2206
*/
2181
- string getKeySizeFixed ( ) { result = instance .asAlg ( ) .getKeySizeFixed ( ) } // TODO: key sizes for known algorithms
2207
+ string getKeySizeFixed ( ) {
2208
+ result = instance .asAlg ( ) .getKeySizeFixed ( )
2209
+ or
2210
+ exists ( int size |
2211
+ KeyOpAlg:: fixedImplicitCipherKeySize ( instance .asAlg ( ) .getAlgorithmType ( ) , size ) and
2212
+ result = size .toString ( )
2213
+ )
2214
+ }
2182
2215
2183
2216
/**
2184
2217
* Gets the key size generic source node.
0 commit comments