Abstract
A common framework, which can be used to analyze the two-party security protocols, is proposed in this paper. With the common framework, a common program is developed in order that any two-party security protocol can be automatically analyzed through SMV with slight modification of the common program. Finally, we illustrate the feasibility and efficiency of the common program analysis with the SSL 3.0 protocol as a case study.
This work is supported by National Natural Science Foundation of China (Grant Nos. 60102004, 60373040 and 60573048).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Panti, M., Spalazzi, L., Tacconi, S., Valent, S.: Automatic Verification of Security in Payment Protocols for Electronic Commerce. In: Proceedings of the 4th International Conference on Enterprise Information Systems (ICEIS 2002), Ciudad Real, Spain, pp. 968–974 (2002)
Lowe, G.: Towards a completeness result for model checking of security protocols. Technical Report 1998/6, Department of Mathematics and Computer Science, University of Leicester (1998), Available from http://www.mcs.le.ac.uk/~glowe/Security/Papers/completeness.ps.gz
Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)
SMV. School of Computer Science of Carnegie Mellon University (1998), Available via, http://www.cs.cmu.edu/~modelcheck/
Zhang, Y., **ao, G.: Breaking and fixing the Helsinki protocol using SMV. Elecronics Letters 35(15), 1239–1240 (1999)
Zhangn, Y., Chen, K., **ao, G.: Automated Analysis of Cryptographic Protocol Using SMV. In: Proceedings of International Workshop on Cryptographic Techniques and E-Commerce (CrypTEC 1999) (July 1999)
Mitchell, J.C., Mitchell, M., Stern, U.: Automated analysis of cryptographic protocols using Murφ. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 141–151. IEEE Computer Society Press, Los Alamitos (1997)
Zhang, Y., Liu, X.: An approach to the formal verification of the three-principal cryptographic protocols. ACM Operating Systems Review 38(1), 35–42 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhang, Y., Jia, S. (2006). Common Program Analysis of Two-Party Security Protocols Using SMV. In: Shen, H.T., Li, J., Li, M., Ni, J., Wang, W. (eds) Advanced Web and Network Technologies, and Applications. APWeb 2006. Lecture Notes in Computer Science, vol 3842. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11610496_128
Download citation
DOI: https://doi.org/10.1007/11610496_128
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-31158-4
Online ISBN: 978-3-540-32435-5
eBook Packages: Computer ScienceComputer Science (R0)