Abstract
In this paper we explore partial order reduction that make the task of verifying cryptographic protocols more efficient. These reduction techniques have been implemented in our tool Brutus. Although we have implemented several reduction techniques in our tool Brutus, due to space restrictions in this paper we only focus on partial order reductions. Partial order reductions have proved very useful in the domain of model checking reactive systems. These reductions are not directly applicable in our context because of additional complications caused by tracking knowledge of various agents. We present partial order reductions in the context of verifying security protocols and prove their correctness. Experimental results showing the benefits of this reduction technique are also presented.
This research is sponsored by the National Science Foundation (NSF) under Grant No. CCR-9505472 and the Defense Advanced Research Projects Agency (DARPA) under Contract No. DABT63-96-C-0071. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of NSF, DARPA, or the United States Government.
Chapter PDF
Similar content being viewed by others
References
Michael Burrows, Martín Abadi, and Roger Needham. A logic of authentication. ACM Transactions on Computer Systems, 8(1):18–36, February 1990. 503, 516
BGH+95. M. Bellare, J. Garay, R. Hauser, A. Herberg, H. Krawczyk, M. Steiner, G. Tsudik, and M. Waidner. iKP-a family of secure electronic payment protocols. In Proceedings of the 1st USENIX Workshop on Electronic Commerce, July 1995. 511, 516
G. Bella and L. C. Paulson. Using isabelle to prove properties of the kerberos authentication system. In DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997. 504
E. M. Clarke, S. Jha, and W. Marrero. Using state space exploration and a natural deduction style message derivation engine to verify security protocols. In Proceedings of the IFIP Working Conference on Programming Concepts and Methods (PROCOMET), 1998. 504, 506
Patrice Godefroid, Doron Peled, and Mark Staskauskas. Using partial order methods in the formal validation of industrial concurrent programs. In ISSTA’ 96, International Symposium on Software Testing and Analysis, pages 261–269, San Diego, California, USA, 1996. ACM Press. 504, 513
D. Kindred and J. M. Wing. Closing the idealization gap with theory generation. In DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997. 504
G. Lowe. Casper: A compiler for the analysis of security protocols. In Proceedings of the 1997 IEEE Computer Society Symposium on Research in Security and Privacy, pages 18–30, 1997. 504
C. Meadows. Language generation and verification in the NRL protocol analyzer. In Proceedings of the 9th Computer Security Foundations Workshop. IEEE Computer Society Press, 1996. 504
J. C. Mitchell, M. Mitchell, and U. Stern. Automated analysis of cryptographic protocols using murφ. In Proceedings of the 1997 IEEE Symposium on Security and Privacy. IEEE Computer Society Press, 1997. 504
R. Needham and M. Schroeder. Using encryption for authentication in large networks of computers. Communications of the ACM, 21(12):993–999, 1978. 512, 516
Doron Peled. Combining partial order reductions with on-the-fly model-checking. Journal of Formal Methods in Systems Design, 8(1):39–64, 1996. also appeared in 6th International Conference on Computer Aided Verification 1994, Stanford CA, USA, LNCS 818, Springer-Verlag, 377–390. 504, 513
A. W. Roscoe. Intensional specifications of security protocols. In 9th Computer Security Foundations Workshop, 1996. 504
B. Schneier. Applied Cryptography. John Wiley & Sons, Inc., second edition, 1996. 516
V. Shmatikov and U. Stern. Efficient finite-state analysis for large security protocols. In Proceedings of the 1998 Computer Security Foundations Workshop. IEEE Computer Society Press, June 1998. 516
A. Valmari. Stubborn sets of colored petri nets. In Proceedings of the 12th International Conference on Application and Theory of Petri Nets, pages 102–121, Gjern, Denmark, 1991. 504, 513
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Clarke, E., Jha, S., Marrero, W. (2000). Partial Order Reductions for Security Protocol Verification. In: Graf, S., Schwartzbach, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2000. Lecture Notes in Computer Science, vol 1785. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46419-0_34
Download citation
DOI: https://doi.org/10.1007/3-540-46419-0_34
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67282-1
Online ISBN: 978-3-540-46419-8
eBook Packages: Springer Book Archive