4003-482-01/4005-705-01 Cryptography
Research Topics
Lecture Notes

Boolean Satisfiability

• Boolean satisfiability (SAT) problem
  • Given a Boolean expression or formula . . .
  • Involving a number of Boolean variables . . .
  • Does there exist an assignment of true/false (0/1) values to the variables . . .
  • That makes the whole expression true?
  • If so, the formula is satisfiable
  • If not, the formula is unsatisfiable

• Example
  • Formula: (x + y + ~z) (~x + ~y + z) (~y + ~z)
  • Variables: x, y, z
  • Formula consists of the conjunction (AND) of clauses
  • Each clause consists of the disjunction (OR) of literals
  • Each literal is either a variable or the negation of a variable
  • Conjunctive normal form (CNF)

• Solving a SAT problem
  • If any literal in a clause is true, the clause is satisfied
  • If all literals in a clause are false, the clause is unsatisfied
  • If all clauses are satisfied, the formula is satisfied
  • If any clause is unsatisfied, the formula is unsatisfied
  • Either find a satisfying assignment, in which case the formula is satisfiable, or . . .
  • Prove that there is no satisfying assignment, in which case the formula is unsatisfiable

• Solving a SAT problem: Exhaustive search
  • Try every possible assignment
  • With N variables, requires 2^N operations
  • Example

     x  y  z | (x + y + ~z) | (~x + ~y + z) | (~y + ~z) | Formula
    ---------+--------------+---------------+-----------+---------
     0  0  0 |      1       |       1       |     1     |    1
     0  0  1 |      0       |       1       |     1     |    0
     0  1  0 |      1       |       1       |     1     |    1
     0  1  1 |      1       |       1       |     0     |    0
     1  0  0 |      1       |       1       |     1     |    1
     1  0  1 |      1       |       1       |     1     |    1
     1  1  0 |      1       |       0       |     1     |    0
     1  1  1 |      1       |       1       |     0     |    0
    

    • Solution: Satisfiable
    • Satisfying assignment: x = 0, y = 0, z = 0

• Solving a SAT problem: SAT solver
  • Uses a backtracking depth-first search through the tree of possible assignments
  • Uses sophisticated heuristics to decide which branches to search first
  • Avoids searching branches it knows will lead to conflicts (unsatisfiable clauses)
  • Learns from its mistakes
  • Example
    • Formula: (x + y + ~z) (~x + ~y + z) (~y + ~z)
    • x could be 0 or 1; try x = 0; formula becomes (y + ~z) (~y + ~z)
    • y could be 0 or 1; try y = 0; formula becomes (~z)
    • z must be 0
    • Solution: Satisfiable
    • Satisfying assignment: x = 0, y = 0, z = 0

• Example of an unsatisfiable formula:
  (a + b) (~a + c + e) (a + ~b) (~b + d + ~f) (~a + b) (a + ~d + f) (~a + ~b) (~c + e + ~f)

• Biennial SAT Competition: http://www.satcompetition.org/

SAT Solver Attack on a Block Cipher

• The PRESENT block cipher reduced to one round
  

• Expressing a two-input exclusive-or gate as a CNF formula
  • Truth table:

     x  y  z | z == (x ⊕ y)
    ---------+--------------
     0  0  0 |      1
     0  0  1 |      0
     0  1  0 |      0
     0  1  1 |      1
     1  0  0 |      0
     1  0  1 |      1
     1  1  0 |      1
     1  1  1 |      0
    

  • CNF formula: (x + y + ~z) (x + ~y + z) (~x + y + z) (~x + ~y + ~z)

• Expressing a key recovery attack as a SAT problem
  • Given a known plaintext and a known ciphertext, encrypted through one-round PRESENT with some unknown key
  • Add variables for plaintext bits, ciphertext bits, and key bits
  • Add variables for all round subkey bits and all internal state bits
  • Add clauses for exclusive-or gates in key addition layer
  • Add clauses for S-boxes
  • Add clauses for key schedule operations
  • Assert values for the known plaintext bit variables
  • Assert values for the known ciphertext bit variables
  • Hand the formula to a SAT solver
  • Look at the values of the key bit variables in the satisfying assignment

• Example: One-round PRESENT
  • $ cryptominisat formula01.cnf > formula01.out
  • Variable numbers 1 through 80 are the key bits, least significant first
  • Recovered key: 0001 1010 0110 0100 1001 0101 0101 1101 0010 0100 0101 0001 0111 1011 0000 0101 1110 0001 0110 1100 = 1A64955D24517B05E16C
  • Original key: A5E6DC4AB66CE4693132
  • 14 conflicts (much less than 2⁸⁰)
  • 0.01 seconds CPU time

• Example: Two-round PRESENT
  • $ cryptominisat formula02.cnf > formula02.out
  • Variable numbers 1 through 80 are the key bits, least significant first
  • Recovered key: 1110 1010 0111 0001 0110 1100 0011 1011 1110 1110 1100 1011 0000 0111 0000 0100 0010 0100 0010 0011 = EA716C3BEECB07042423
  • Original key: 30F5EC4595B8BA9CFDB4
  • 3687 conflicts (much less than 2⁸⁰)
  • 0.10 seconds CPU time

• Example: Three-round PRESENT
  • $ cryptominisat formula03.cnf > formula03.out
  • Variable numbers 1 through 80 are the key bits, least significant first
  • Recovered key: 0010 0000 1111 0110 0110 0010 0011 1101 1000 0111 1011 1010 1101 1101 1000 0101 1100 1101 0011 1101 = 20F6623D87BADD85CD3D
  • Original key: 04CD6DCD22ED253F6640
  • 611074 conflicts (much less than 2⁸⁰)
  • 114.55 seconds CPU time

• Research questions
  • How many rounds of PRESENT can we solve before the SAT solver takes longer than a brute force search?
  • What happens if we have two known plaintexts/ciphertexts instead of just one?
  • What about key recovery attacks on other block ciphers?
  • What about key recovery attacks on MACs?
  • What about collision or preimage attacks on hash functions?
  • Can we develop high-performance parallel SAT solvers?
  • Can we develop high-performance GPU parallel SAT solvers?

Statistical Tests on Cryptographic Algorithms

• Test of PRESENT ciphertext popcount: http://www.cs.rit.edu/~ark/lectures/cuda01/

• NIST's statistical test suite: http://csrc.nist.gov/publications/nistpubs/800-22-rev1a/SP800-22rev1a.pdf

• Prof. Kaminsky's Parallel Crypto web page: http://www.cs.rit.edu/~ark/parallelcrypto/

• Research questions
  • How random are reduced-round versions of a cryptographic algorithm?
  • How many rounds are needed before a cryptographic algorithm becomes random?
  • How random are PRESENT, Trivium, AES, SHA-1, SHA-2, SHA-3, all the nonwinning SHA-3 candidates, SipHash, etc., etc.?
  • What other statistical test methodologies might prove useful?
  • Can we come up with Bayesian statistical tests instead of frequentist statistical tests?

Cryptography • 4003-482-01/4005-705-01 • Spring Quarter 2013

Course Page

Alan Kaminsky • Department of Computer Science • Rochester Institute of Technology • 4486 + 2220 = 6706

Home Page

Copyright © 2013 Alan Kaminsky. All rights reserved. Last updated 06-Feb-2013. Please send comments to ark­@­cs.rit.edu.