Synthesizing Shortest Linear Straight-Line Programs over GF(2) for the AES using SAT ?
Carsten Fuhs · 2011
Recently, the use of SAT solving has expanded to the area of automatically synthesizing shortest linear straight-line programs from a specication (5,4). We provide corresponding application benchmarks for parts of the implementation of the S-box of the Advanced Encryption Standard.