M. Ayala-Rincón and Y. Santos Rego, “Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model”, JFR, vol. 6, no. 1, pp. 31–61, Jan. 2013.