Abstract
We discuss the advantages and limitations of the main proof-based approaches to the formal verification of cryptographic protocols. We show possible routes for addressing their limitations by combining them with model-checking techniques. More precisely we argue that proof-based techniques can be used for providing a general framework, model-checking techniques for mechanization and invariant techniques for bringing precise understanding of protocol strengths and weaknesses.
Chapter PDF
Similar content being viewed by others
References
J.R. Abrial. The B-method for large software specification, design and coding. In VDM'91. Springer Verlag, 1991.
P. Bieber and N. Boulahia-Cuppens. Formal development of authentication protocols. In BCS-FAGS sixth Refinement Workshop, 1994.
D. Bolignano. Formal verification of cryptographic protocols. In Proceedings of the third ACM Conference on Computer and Communication Security, 1996.
D. Bolignano. Towards the Formal Verification of Electronic Commerce Protocols. In Proceedings of the 10 th IEEE Computer Security Foundations Workshop. IEEE, June 1997.
D. Bolignano. Towards the Mechanization of Cryptographic Protocol Verification. In Proceedings of the 9th International Conference on Computer-Aided Verification (CAV'97), June 1997.
D. Bolignano. Using abstractions for automatizing and simplifying the verification of cryptographic protocols. Technical report, Dyade, 1998.
M. Burrows, M. Abadi, and R. Needham. A logic of authentication. ACM Transactions on Computer Systems, 8, 1990.
P. Syverson C. Meadows. A formal specification of requirements for payment transactions in the set protocol. In Finacial Cryptography, 1998.
P.C. Chen and V.D. Gligor. On the formal specification and verification of a multiparty session protocol. In Proceedings of the IEEE Symposium on Research in Security and Privacy, 1990.
D. Dolev and A. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, IT-29(2):198–208, 1983.
G.Leduc, O. Bonaventure, E. Koerner, L. Leonard, C. Pecheur, and D. Zanetti. Specification and verification of a ttp protocol for the conditional access to services. In Proceedings of the 12th Workshop on the Application of Formal Methods to System Development (Univ Montreal, 1996.
R.A. Kemmerer. Analyzing encryption protocols using formal verification techniques. In IEEE Journal on Selected Areas in Communications, volume 7(4), 1989.
G. Lowe. An attack on the needham-schroeder public-key protocol. In Information Processing Letters, 1995.
C. Meadows. Applying formal methods to the analysis of a key management protocol. In Journal of Computer Security, 1992.
J. K. Millen, S.C. Clark, and S.B. Freedman. The interrogator: Protocol security analysis. IEEE Transactions on Software Engineering, 13(2), 1987.
L. Paulson. The inductive approach to verifying cryptographic protocols. J. Computer Security, 1998.
E. Snekkenes. Roles in cryptographic protocols. In Proceedings of the IEEE Symposium on Research in Security and Privacy, pages 105–119. IEEE, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bolignano, D. (1998). Integrating proof-based and model-checking techniques for the formal verification of cryptographic protocols. In: Hu, A.J., Vardi, M.Y. (eds) Computer Aided Verification. CAV 1998. Lecture Notes in Computer Science, vol 1427. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028735
Download citation
DOI: https://doi.org/10.1007/BFb0028735
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64608-2
Online ISBN: 978-3-540-69339-0
eBook Packages: Springer Book Archive
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.