On investigating the cryptographic properties of AES and small scale variations.
More...
Go to the source code of this file.
Detailed Description
On investigating the cryptographic properties of AES and small scale variations.
 Todo:
 Create submodule

These plans need their own submodule.
 Todo:
 Cryptographic properties of AES

Given a correct translation of the AES into a SAT problem, represented by the predicate "AES(P,K,C)" where P, K, and C are lists of 128 variables, several questions regarding certain cryptographic properties of the AES can be formulated as SAT problems.

Does AES have two distinct keys which maps the same plaintext block to the same ciphertext block?

This can be translated as "AES(P,K1,C) and AES(P,K2,C) and
NEQ(K1,K2)" where "NEQ" specifies that K1 differs form K2 in at least one bit.

Does AES have any key which acts as the identity on one or all plaintext blocks?

This can be translated as "AES(P,K,P)".

This can also be expanded trivially to find keys where AES algorithm acts as the identity on "k" or more plaintext blocks (for reasonable k) by simply considering "AES(P1,K,P1) and AES(P2,K,P2) and ... and
AES(Pk,K,Pk) and NEQ(P1,P2,...,Pk)" where here "NEQ" specifies that every argument differs in at least one variable from every other.

This may also be made more damaging to the AES by considering specifically plaintexts of a particular form (plaintext blocks representing particular common ASCII sequences).

We should also consider the use of QBF translations here.

Does AES have any key which is the inverse of any other for some plaintext/ciphertext pair?

Considering only a single piece of plaintext (that there are two keys K1 and K2 for which AES with that K1 maps some plaintext P to ciphertext C and AES with K2 maps C to P) can be translated simply as "AES(P,K1,C) and AES(C,K2,P)".

This can be expanded to find keys K1 and K2 where AES using K2 is the inverse of AES with K1 for at least "k" plaintext blocks in the following way: "AES(P1,K1,C1) and AES(C1,K2,P1) and ... and
AES(Pk,K(k1),Ck) and AES(Ck,Kk,Pk) and NEQ(P1,P2,...,Pk)" .

There is obviously then the question of whether there is key which acts as its own inverse for at least "k" plaintext blocks, where K1=K2 etc.

Again we should consider using QBF solvers here to translate this property for all plaintext ciphertext pairs.

Does the AES have any key for which the cipher becomes the identity with that key? See "Keys for which AES encrypts P to P".
 Todo:
 Keys for which AES encrypts P to P

Does the AES have any key for which the cipher maps plaintext P back to itself, for all P?

Is a key K and plaintext P for which AES, with that K, encrypts P to P can be translated simply as "exists P . AES(P,K,P)" and can easily be formulated as a SAT problem.

This question can then be expanded to whether there is a K such that for all P, AES, with K, encrypts P to P. That is, "for all P . AES(P,K,P)".

See output_ss_fcl_id_p in ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/Translations.mac for the implemented translation of the single plaintext cryptographic question.

What to call these two properties ("exists P . AES(P,K,P)" and "for all P . AES(P,K,P)")?

There exist K and P such that AES(P,K,P) for:

4bit AES with 1 row, 1 column, 4bit field up to 10 rounds. All solvers find K and P in < 0.1s.

16bit AES with 1 row, 1 column, 4bit field up to 4 rounds. Fastest solver for 4 rounds finds K and P in < 1s.

Do there exist K and P such that AES(P,K,P) for the 4bit trivial AES scheme (1 row, 1 column, 4bit field)?

Using the standard canonical box translation with bidirectional MixColumns translation:

Generating the instances for rounds 1 to 10:
for i : 1 thru 10 do output_ss_fcl_id_p_std(i,1,1,4,false,aes_ts_box,aes_mc_bidirectional);

Running solvers via (using cryptominisat as an example):
for i in $(seq 1 10); do cryptominisat ssaes_id_p_r${i}_c1_rw1_e4_f0.cnf  awk " { print \"[$i/10] \" \$0 }"; done

All instances were found satisfiable in <0.1s using very few conflicts (<50).

Comparing the solvers for finding an example of an identity mapping key for 10 rounds:

march_pl (node_count: 2).

minisat2.2.0 (conflicts: 3).

OKsolver_2002 (nodes: 5).

precosat570.1 (conflicts: 5).

picosat913 (conflicts: 12).

precosat236 (conflicts: 12).

cryptominisat (conflicts: 13).

minisat2 (conflicts: 45).

glucose (conflicts: 67).

satz:
[10/10] **** The instance is satisfiable. *****
[10/10] NB_MONO= 0, NB_UNIT= 24035, NB_BRANCHE= 403, NB_BACK= 197
[10/10] Program terminated in 0.000 seconds.
[10/10] satz215 v 0.000 403 197 64768 763 1 568 3436 200 3028 0
march_pl or minisat2.2.0 seems best here but the instance is trivially solved and so there isn't much difference between solvers.

Do there exist K and P such that AES(P,K,P) for the 16bit trivial AES scheme (2 row, 2 column, 4bit field)?

Using the standard canonical box translation with bidirectional MixColumns translation:

Generating the instances for rounds 1 to 10:
for i : 1 thru 10 do output_ss_fcl_id_p_std(i,1,1,4,false,aes_ts_box,aes_mc_bidirectional);

Running solvers via (using cryptominisat as an example):
for i in $(seq 1 10); do cryptominisat ssaes_id_p_r${i}_c1_rw1_e4_f0.cnf  awk " { print \"[$i/10] \" \$0 }"; done

All instances up to round 10 were found satisfiable.

Experiments still running for rounds > 4 for some solvers. See "For 10 rounds" below.

Comparing the solvers for finding an example of an identity mapping key for 4 rounds:

cryptominisat (time: 0.53s, conflicts: 6889).

precosat236 (time: 1.1s, conflicts: 15684).

minisat2.2.0 (time: 1.95s, conflicts: 26539).

glucose (time: 2.59s, conflicts: 23614).

precosat570.1 (time: 20.4s, conflicts: 139328).

OKsolver_2002 (time: 57.1s, nodes: 2007).

picosat913 (time: 68.5s, conflicts: 866125).

minisat2 (time: 85.72, conflicts: 118350).
cryptominisat seems best here.

For 10 rounds:

minisat2.2.0 (time: 11s, conflicts: 48883).

cryptominisat (time: 42s, conflicts: 143094).

precosat570.1 (time: 51s, conflicts:155752).

precosat236 (time: 143s, conflicts: 446841).

glucose (time: 253s, conflicts: 551680).


DONE The single plaintext translation of this question into a SAT problem should be implemented in the Maxima system.
Definition in file CryptographicProperties.hpp.