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