Ayala-Rincón, M.; Santos Rego, Y. Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model. JFR 2013, 6, 31-61.