World Scientific
  • Search
  •   
Skip main navigation

Cookies Notification

We use cookies on this site to enhance your user experience. By continuing to browse the site, you consent to the use of our cookies. Learn More
×

System Upgrade on Tue, May 28th, 2024 at 2am (EDT)

Existing users will be able to log into the site and access content. However, E-commerce and registration of new users may not be available for up to 12 hours.
For online purchase, please visit us again. Contact us at [email protected] for any enquiries.

EXPLOITING SYMMETRIES FOR TESTING EQUIVALENCE VERIFICATION IN THE SPI CALCULUS

    https://doi.org/10.1142/S0129054106004121Cited by:0 (Source: Crossref)

    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.

    References

    • M. Abadi and A. D. Gordon, Nordic J. Comput. 5, 267 (1998). Web of ScienceGoogle Scholar
    • M. Abadi and A. D. Gordon, "A calculus for cryptographic protocols the spi calculus," SRC - Research Report 149, Digital System Research Center, 1998 . Google Scholar
    • M. Bellareet al., iKP - A family of secure electronic payment protocols, Proc. 1st USENIX Workshop on Electronic Commerce (USENIX Assoc., Berkeley, CA, 1995) pp. 157–166. Google Scholar
    • M. Boreale, R. De Nicola and R. Pugliese, SIAM J. Comput. 31, 947 (2002). Crossref, Web of ScienceGoogle Scholar
    • M. Burrows, M. Abadi and R. Needham, Proceedings of the Royal Society, Series A 426, 233 (1989). Crossref, Web of ScienceGoogle Scholar
    • I. Cibrario Bertolottiet al., A new knowledge representation strategy for cryptographic protocol analysis, Proc. Tools and Algoritms for the Construction and Analysis of Systems (TACAS 2003), Lecture Notes in Computer Science 2619 (Springer-Verlag, Berlin, 2003) pp. 284–298. Google Scholar
    • E. M.   Clarke , S.   Jha and W.   Marrero , Partial order reductions for security protocol verification , Proc. Tools and Algoritms for the construction and Analysis of systems (TACAS 2000) , Lecture Notes in Computer Science   1785 ( Springer-Verlag , Berlin , 2000 ) . Google Scholar
    • E. M. Clarke, S. Jha and W. Marrero, ACM Trans. Softw. Eng. Meth. 9, 443 (2000). Crossref, Web of ScienceGoogle Scholar
    • L. Durante, R. Sisto and A. Valenzano, ACM Trans. Softw. Eng. Meth. 12, 222 (2003). Crossref, Web of ScienceGoogle Scholar
    • M. Fiore and M. Abadi, Computing symbolic models for verifying cryptographic protocols, Proc. 14th IEEE Computer Security Foundations Workshop (CSFW 2001) (IEEE Computer Society Press, Washington, 2001) pp. 160–173. Google Scholar
    • S.   Gnesi , D.   Latella and G.   Lenzini , A BRUTUS logic for the Spi-Calculus , Proc. WITS'02 ( 2002 ) . Google Scholar
    • K.   Jensen , Coloured Petri nets: basic concepts, analysis methods and practical use ( Springer-Verlag , Berlin , 1995 ) . Google Scholar
    • G. Lowe, Breaking and fixing the Needham-Schroeder public-key protocol using FDR, Proc. Tools and Algoritms for the Construction and Analysis of Systems (TACAS 1996), Lecture Notes in Computer Science 1055 (Springer-Verlag, Berlin, 1996) pp. 147–166. Google Scholar
    • G. Lowe, Some new attacks upon security protocols, Proc. 9th IEEE Computer Security Foundations Workshop (CSFW 1996) (IEEE Computer Society Press, Washington, 1996) pp. 162–169. Google Scholar
    • G. Lowe, Casper: a compiler for the analysis of security protocols, Proc. 10th IEEE Computer Security Foundations Workshop (CSFW 1997) (IEEE Computer Society Press, Washington, 1997) pp. 18–30. Google Scholar
    • J. K. Millen, S. C. Clark and S. B. Freedman, IEEE Trans. Softw. Eng. 13, 274 (1987). Web of ScienceGoogle Scholar
    • R. Milner, J. Parrow and D. Walker, Inf. Comput. 100, 1 (1992). Crossref, Web of ScienceGoogle Scholar
    • R. Needham and M. Schroeder, Communications of the ACM 21, 993 (1978). Crossref, Web of ScienceGoogle Scholar
    • L. C. Paulson, J. Comput. Sec. 6, 85 (1998). Crossref, Web of ScienceGoogle Scholar
    • S. Schneider, IEEE Trans. Softw. Eng. 24, 741 (1998). Crossref, Web of ScienceGoogle Scholar
    • A. P. Sistla, V. Gyuris and E. A. Emerson, ACM Trans. Softw. Eng. Meth. 9, 133 (2000). Crossref, Web of ScienceGoogle Scholar
    Remember to check out the Most Cited Articles!

    Check out these Handbooks in Computer Science