Many industrial ciphers—including those in today’s access control and NFC applications—use algebraically insecure cryptographic functions that can be broken using SAT solvers in an automated process.
Low-complexity ciphers used in a wide range of applications ranging from public transport payment to luxury car immobilizers were developed in the 80’s and 90’s. The proprietary ciphers typically stayed secret during their design and deployment thereby foregoing independent peer review. SAT solver programs, a specific flavor of equations solvers, can measure the complexity of such ciphers and often extract the secret keys from sniffed transactions. SAT solvers implement a ‘smart’ brute force in which only promising branches of the solution tree are tried.
The analysis process involves conversion of a cryptographic cipher into simple system of equations of CNF form and solving this system of equations to derive a secret key. Using SAT solving technology we can break low-complexity cipher such as Crypto-1 used in Mifare Classic cards in under 20 seconds on a desktop computer. A brute-force attack on Crypto-1’s 48bit key would take weeks on comparable hardware or significant investments into specialized FPGA hardware. This allows real-time attacks against access control and payment systems.
Most other cryptographic ciphers of low complexity or key lengths below 64 bits are vulnerable to this type of attack. The capabilities of SAT solvers summarize years of theoretical and practical computer science research and make them easily accessible for cryptographic analysis and optimization exercises with large output spaces.
Resistance to SAT-solver based attacks can easily be achieved by testing new cryptographic primitives in their design phase with open source SAT solvers. When using a “divide and conquer” strategy, SAT solvers can provide a measure for cryptographic hardness even when they cannot break a given function.
We understand, of course, that hardly any new cryptographic primitives are needed given the wide versatility of AES, SHA, ECC, TEA, and other established functions. Therefore, the primary use of SAT solvers in cryptography is the analysis of old proprietary ciphers.
These references provide ready-made SAT solvers and tutorials for some cryptographic functions that can easily be extended for analysis of new primitives:
