  The SAT attack has shown to be efficient against most combinational logic
encryption methods. It can be extended to attack sequential logic encryption
techniques by leveraging circuit unrolling and model checking methods. However,
with no guidance on the number of times that a circuit needs to be unrolled to
find the correct key, the attack tends to solve many time-consuming Boolean
satisfiability (SAT) and model checking problems, which can significantly
hamper its efficiency. In this paper, we introduce Fun-SAT, a functional
corruptibility-guided SAT-based attack that can significantly decrease the SAT
solving and model checking time of a SAT-based attack on sequential encryption
by efficiently estimating the minimum required number of circuit unrollings.
Fun-SAT relies on a notion of functional corruptibility for encrypted
sequential circuits and its relationship with the required number of circuit
unrollings in a SAT-based attack. Numerical results show that Fun-SAT can be,
on average, 90x faster than previous attacks against state-of-the-art
encryption methods, when both attacks successfully complete before a one-day
time-out. Moreover, Fun-SAT completes before the time-out on many more
circuits.
