Ayala-Rincón, M., and Y. Santos Rego. “Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model”. Journal of Formalized Reasoning, vol. 6, no. 1, Jan. 2013, pp. 31-61, doi:10.6092/issn.1972-5787/3720.