A mathematical model and metrics to evaluate the security strength of a logic-locked circuit against a satisfiability (SAT) based attack are proposed. A probabilistic model is developed to capture the variation in the SAT-attack search path length and report the SAT resilience as an expected computational complexity. An estimator of the expected complexity, assuming an equally likely branching probability, is proposed. The model and the estimator allow for the derivation of a closed-form estimate, and characterization of the key search space without experimental bias toward SAT-attack implementation or circuit topology.