EXPLOITING SYMMETRIES FOR TESTING EQUIVALENCE VERIFICATION IN THE SPI CALCULUS
Ivan Cibrario Bertolotti, Luca Durante, Riccardo Sisto, Adriano Valenzano · International Journal of Foundations of Computer Science · 2006
Testing equivalence is a quite powerful way of expressing security properties of cryptographic protocols, but its formal verification is a difficult task, because it is based on universal quantification over contexts. A technique based on state exploration to address this verification problem has previously been presented; it relies on an environment-sensitive labelled transition system (ES-LTS) and on symbolic term representation. This paper shows that such a technique can be enhanced by exploiting symmetries found in the ES-LTS structure. Experimental results show that the proposed enhancement can substantially reduce the size of the ES-LTS and that the technique as a whole compares favorably with respect to related work.