Copyright Notice:
The publication copies distributed in this site are
provided to ensure timely dissemination of scholarly and technical
work. Copyright and all rights therein are retained by authors or by
other copyright holders (as explicitly indicated). All persons copying
this information are expected to adhere
to the terms and constraints invoked by each copyright. In
most cases, these works may not be reposted without the explicit
permission of the copyright holder
Ivan Cibrario Bertolotti, Luca Durante, Riccardo Sisto, Adriano Valenzano,
Exploiting Symmetries for Testing Equivalence Verification in the SPI Calculus,
Int. Journal of Foundations of Computer Science, Vol. 17, No. 4 (August 2006), World Scientific, pp. 815-832.
©2006 World Scientific
doi: 10.1142/S0129054106004121
Abstract
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.
Back to Riccardo Sisto's publications