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 in the Spi Calculus,
in ATVA 2004 - 2nd Int. Symp. on Automated Technology for Verification and Analysis, Taiwan, November 2004, Springer, pp. 135-149.
©2004 Springer
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 the universal quantification over contexts. A technique based on state exploration
to address this verification problem has been previously 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