Five Ways Windows Authentication Breaks: A Machine-Checked Tour -- and Why Finding Nothing New Is the Point
A Tamarin and Dolev-Yao tour of 23 Windows authentication protocols: five recurring failure patterns, what a prover can prove, and the boundary it cannot cross.