@@ -582,6 +582,28 @@ module CryptographyBase<LocationSig Location, InputSig<Location> Input> {
582582 }
583583 }
584584
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+
585607 bindingset [ type]
586608 predicate symmetric_cipher_to_name_and_structure (
587609 TSymmetricCipherType type , string name , CipherStructureType s
@@ -790,6 +812,10 @@ module CryptographyBase<LocationSig Location, InputSig<Location> Input> {
790812 * If a specific key size is unknown, this predicate should be implemented as `none()`.
791813 *
792814 * 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`.
793819 */
794820 abstract string getKeySizeFixed ( ) ;
795821
@@ -2178,7 +2204,14 @@ module CryptographyBase<LocationSig Location, InputSig<Location> Input> {
21782204 /**
21792205 * Gets the key size variant of this algorithm in bits, e.g., 128 for "AES-128".
21802206 */
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+ }
21822215
21832216 /**
21842217 * Gets the key size generic source node.
0 commit comments