Skip to content

Commit 7256faa

Browse files
bdrodesropwareJB
authored andcommitted
Added modeling infrastructure
1 parent 2d44724 commit 7256faa

File tree

10 files changed

+15228
-0
lines changed

10 files changed

+15228
-0
lines changed
Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
import experimental.crypto.CryptoArtifact
2+
import experimental.crypto.CryptoAlgorithmNames
3+
4+
import experimental.crypto.modules.OpenSSL as OpenSSL
5+
Lines changed: 222 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,222 @@
1+
/**
2+
* Names of known cryptographic algorithms.
3+
* The names are standardized into upper-case, no spaces, dashes or underscores.
4+
*/
5+
6+
/**
7+
* Returns a string to represent generally unknown algorithms.
8+
* Predicate is to be used to get a consistent string representation
9+
* for unknown algorithms.
10+
*/
11+
string unknownAlgorithm() { result = "UNKNOWN" }
12+
13+
string getHashType() { result = "HASH" }
14+
string getSymmetricEncryptionType() { result = "SYMMETRIC_ENCRYPTION" }
15+
string getAsymmetricEncryptionType() { result = "ASYMMETRIC_ENCRYPTION" }
16+
string getKeyDerivationType() { result = "KEY_DERIVATION" }
17+
string getCipherBlockModeType() { result = "BLOCK_MODE" }
18+
string getSymmetricPaddingType() { result = "SYMMETRIC_PADDING" }
19+
string getAsymmetricPaddingType() { result = "ASYMMETRIC_PADDING" }
20+
string getEllipticCurveType() { result = "ELLIPTIC_CURVE" }
21+
string getSignatureType() { result = "SIGNATURE" }
22+
string getKeyExchangeType() { result = "KEY_EXCHANGE" }
23+
24+
string getAsymmetricType(){
25+
result in [getAsymmetricEncryptionType(), getSignatureType(), getKeyExchangeType(), getEllipticCurveType()]
26+
}
27+
28+
predicate isKnownType(string algType){
29+
algType in [
30+
getHashType(), getSymmetricEncryptionType(), getAsymmetricEncryptionType(), getKeyDerivationType(),
31+
getCipherBlockModeType(), getSymmetricPaddingType(), getAsymmetricPaddingType(), getEllipticCurveType(),
32+
getSignatureType(), getKeyExchangeType()
33+
]
34+
}
35+
36+
37+
predicate isKnownAlgorithm(string name) { isKnownAlgorithm(name, _) }
38+
39+
predicate isKnownAlgorithm(string name, string algType) {
40+
isHashingAlgorithm(name) and algType = "HASH"
41+
or
42+
isEncryptionAlgorithm(name, algType) and algType in ["SYMMETRIC_ENCRYPTION", "ASYMMETRIC_ENCRYPTION"]
43+
or
44+
isKeyDerivationAlgorithm(name) and algType = "KEY_DERIVATION"
45+
or
46+
isCipherBlockModeAlgorithm(name) and algType = "BLOCK_MODE"
47+
or
48+
isPaddingAlgorithm(name, algType) and algType in ["SYMMETRIC_PADDING", "ASYMMETRIC_PADDING"]
49+
or
50+
isEllipticCurveAlgorithm(name) and algType = "ELLIPTIC_CURVE"
51+
or
52+
isSignatureAlgorithm(name) and algType = "SIGNATURE"
53+
or
54+
isKeyExchangeAlgorithm(name) and algType = "KEY_EXCHANGE"
55+
}
56+
57+
/**
58+
* Holds if `name` is a known hashing algorithm in the model/library.
59+
*/
60+
predicate isHashingAlgorithm(string name) {
61+
name =
62+
[
63+
"BLAKE2", "BLAKE2B", "BLAKE2S",
64+
"SHA2", "SHA224", "SHA256", "SHA384", "SHA512", "SHA512224", "SHA512256",
65+
"SHA3", "SHA3224", "SHA3256", "SHA3384", "SHA3512", "SHAKE128", "SHAKE256", "SM3",
66+
"WHIRLPOOL", "POLY1305", "HAVEL128", "MD2", "MD4", "MD5", "PANAMA", "RIPEMD", "RIPEMD128",
67+
"RIPEMD256", "RIPEMD160", "RIPEMD320", "SHA0", "SHA1", "SHA", "MGF1","MGF1SHA1", "MDC2", "SIPHASH"
68+
]
69+
}
70+
71+
predicate isEncryptionAlgorithm(string name, string algType) {
72+
isAsymmetricEncryptionAlgorithm(name) and algType = "ASYMMETRIC_ENCRYPTION"
73+
or
74+
isSymmetricEncryptionAlgorithm(name) and algType = "SYMMETRIC_ENCRYPTION"
75+
}
76+
77+
predicate isEncryptionAlgorithm(string name) { isEncryptionAlgorithm(name, _) }
78+
79+
/**
80+
* Holds if `name` corresponds to a known symmetric encryption algorithm.
81+
*/
82+
predicate isSymmetricEncryptionAlgorithm(string name) {
83+
// NOTE: AES is meant to caputure all possible key lengths
84+
name =
85+
[
86+
"AES", "AES128", "AES192", "AES256", "ARIA", "BLOWFISH", "BF", "ECIES", "CAST", "CAST5",
87+
"CAMELLIA", "CAMELLIA128", "CAMELLIA192", "CAMELLIA256", "CHACHA", "CHACHA20",
88+
"CHACHA20POLY1305", "GOST", "GOSTR34102001", "GOSTR341094", "GOSTR341194", "GOST2814789",
89+
"GOSTR341194", "GOST2814789", "GOST28147", "GOSTR341094", "GOST89", "GOST94", "GOST34102012",
90+
"GOST34112012", "IDEA", "RABBIT",
91+
"SEED", "SM4", "DES", "DESX", "3DES", "TDES", "2DES", "DES3", "TRIPLEDES", "TDEA", "TRIPLEDEA",
92+
"ARC2", "RC2", "ARC4", "RC4", "ARCFOUR", "ARC5", "RC5", "MAGMA", "KUZNYECHIK"
93+
]
94+
}
95+
96+
/**
97+
* Holds if `name` corresponds to a known key derivation algorithm.
98+
*/
99+
predicate isKeyDerivationAlgorithm(string name) {
100+
name =
101+
[
102+
"ARGON2", "CONCATKDF", "CONCATKDFHASH", "CONCATKDFHMAC", "KBKDFCMAC", "BCRYPT", "HKDF",
103+
"HKDFEXPAND", "KBKDF", "KBKDFHMAC", "PBKDF1", "PBKDF2", "PBKDF2HMAC", "PKCS5", "SCRYPT",
104+
"X963KDF", "EVPKDF"
105+
]
106+
}
107+
108+
/**
109+
* Holds if `name` corresponds to a known cipher block mode
110+
*/
111+
predicate isCipherBlockModeAlgorithm(string name) {
112+
name = ["CBC", "GCM", "CCM", "CFB", "OFB", "CFB8", "CTR", "OPENPGP", "XTS", "EAX", "SIV", "ECB"]
113+
}
114+
115+
/**
116+
* Holds if `name` corresponds to a known padding algorithm
117+
*/
118+
predicate isPaddingAlgorithm(string name, string algType) {
119+
isSymmetricPaddingAlgorithm(name) and algType = "SYMMETRIC_PADDING"
120+
or
121+
isAsymmetricPaddingAlgorithm(name) and algType = "ASYMMETRIC_PADDING"
122+
}
123+
124+
/**
125+
* holds if `name` corresponds to a known symmetric padding algorithm
126+
*/
127+
predicate isSymmetricPaddingAlgorithm(string name) { name = ["PKCS7", "ANSIX923"] }
128+
129+
/**
130+
* Holds if `name` corresponds to a known asymmetric padding algorithm
131+
*/
132+
predicate isAsymmetricPaddingAlgorithm(string name) { name = ["OAEP", "PKCS1V15", "PSS", "KEM"] }
133+
134+
predicate isBrainpoolCurve(string curveName, int keySize) {
135+
// ALL BRAINPOOL CURVES
136+
keySize in [160, 192, 224, 256, 320, 384, 512] and
137+
(
138+
curveName = "BRAINPOOLP" + keySize.toString() + "R1"
139+
or
140+
curveName = "BRAINPOOLP" + keySize.toString() + "T1"
141+
)
142+
}
143+
144+
predicate isSecCurve(string curveName, int keySize) {
145+
// ALL SEC CURVES
146+
keySize in [112, 113, 128, 131, 160, 163, 192, 193, 224, 233, 239, 256, 283, 384, 409, 521, 571] and
147+
exists(string suff | suff in ["R1", "R2", "K1"] |
148+
curveName = "SECT" + keySize.toString() + suff or
149+
curveName = "SECP" + keySize.toString() + suff
150+
)
151+
}
152+
153+
predicate isC2Curve(string curveName, int keySize) {
154+
// ALL C2 CURVES
155+
keySize in [163, 176, 191, 208, 239, 272, 304, 359, 368, 431] and
156+
exists(string pre, string suff |
157+
pre in ["PNB", "ONB", "TNB"] and suff in ["V1", "V2", "V3", "V4", "V5", "W1", "R1"]
158+
|
159+
curveName = "C2" + pre + keySize.toString() + suff
160+
)
161+
}
162+
163+
predicate isPrimeCurve(string curveName, int keySize) {
164+
// ALL PRIME CURVES
165+
keySize in [192, 239, 256] and
166+
exists(string suff | suff in ["V1", "V2", "V3"] | curveName = "PRIME" + keySize.toString() + suff)
167+
}
168+
169+
predicate isEllipticCurveAlgorithm(string curveName) { isEllipticCurveAlgorithm(curveName, _) }
170+
171+
/**
172+
* Holds if `name` corresponds to a known elliptic curve.
173+
*/
174+
predicate isEllipticCurveAlgorithm(string curveName, int keySize) {
175+
isSecCurve(curveName, keySize)
176+
or
177+
isBrainpoolCurve(curveName, keySize)
178+
or
179+
isC2Curve(curveName, keySize)
180+
or
181+
isPrimeCurve(curveName, keySize)
182+
or
183+
curveName = "ES256" and keySize = 256
184+
or
185+
curveName = "CURVE25519" and keySize = 255
186+
or
187+
curveName = "X25519" and keySize = 255
188+
or
189+
curveName = "ED25519" and keySize = 255
190+
or
191+
curveName = "CURVE448" and keySize = 448 // TODO: need to check the key size
192+
or
193+
curveName = "ED448" and keySize = 448
194+
or
195+
curveName = "X448" and keySize = 448
196+
or
197+
curveName = "NUMSP256T1" and keySize = 256
198+
or
199+
curveName = "NUMSP384T1" and keySize = 384
200+
or
201+
curveName = "NUMSP512T1" and keySize = 512
202+
or
203+
curveName = "SM2" and keySize in [256, 512]
204+
205+
}
206+
207+
/**
208+
* Holds if `name` corresponds to a known signature algorithm.
209+
*/
210+
predicate isSignatureAlgorithm(string name) {
211+
name = ["DSA", "ECDSA", "EDDSA", "ES256", "ES256K", "ES384", "ES512", "ED25519", "ED448", "ECDSA256", "ECDSA384", "ECDSA512"]
212+
}
213+
214+
/**
215+
* Holds if `name` is a key exchange algorithm.
216+
*/
217+
predicate isKeyExchangeAlgorithm(string name) { name = ["ECDH", "DH", "DIFFIEHELLMAN", "X25519", "X448"] }
218+
219+
/**
220+
* Holds if `name` corresponds to a known asymmetric encryption.
221+
*/
222+
predicate isAsymmetricEncryptionAlgorithm(string name) { name = ["RSA"] }

0 commit comments

Comments
 (0)