There are two kinds of implementation of our model: 
* Matrix_if_then_else.py: follows the principle introduced in Sect. 4.1.
* Matrix.py: follows Theorem 2.
For MISTY1 and CAMELLIA, only Matrix_if_then_else.py is executed, because there are many matrices used in the main function. For the other ciphers, both Matrix.py and Matrix_if_then_else.py are required to be executed.

This code is to find the 4-round key-dependent distinguisher for AES introduced in Section 5.1.
AES_4_round_keydependent.py is the main function. The command to run it is ($ is the prompt of bash):

The output can be saved as a CVC file AES_4.cvc by the redirection command

When the CVC file is obtained, you can run it by

The default solver minisat is used to solve the foundamental SAT problems.
If you have installed the cryptominisat, you can also manually call cryptominisat by

Cryptominisat supports parallelism, so you can use --threads n to decide how many threads are required to solve your problem.
For our experiments, we recommend that n should be at least 4.
After running it, two possible results might be returned:
* Valid,
* Invalid.
When input a CVC file ended with a statement "QUERY FALSE" to the solver, actually we ask the solver a question like 
"No solutions to the model with constraints listed in the CVC file, right?" 
"Valid" means there is no solution to the model.
"Invalid" means there is at least one solution to the model.
As is well known in division property, "no solution" i.e. "Valid" here, is a good news because it means some balanced bits are found. 

Similar with AES_4_round_keydependent

In Camellia_base.py, we list the model of camellia.
In Camellia.py, you can change the inVec to decide which bit should be active and how many rounds you want to check.