Abstract
The verification of cryptographic protocol specifications is an active research topic and has received much attention from the formal verification community. By contrast, the black-box testing of actual implementations of protocols, which is, arguably, as important as verification for ensuring the correct functioning of protocols in the “real” world, is little studied. We propose an approach for checking secrecy and authenticity properties not only on protocol specifications, but also on black-box implementations. The approach is compositional and integrates ideas from verification, testing, and learning. It is illustrated on the Basic Access Control protocol implemented in biometric passports.
This work was done while the second author was visiting the university of Nijmegen.
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.
References
Burrows, M., Abadi, M., Needham, R.M.: A logic of authentication. ACM Trans. Comput. Syst. 8(1), 18–36 (1990)
Gong, L., Needham, R.M., Yahalom, R.: Reasoning about belief in cryptographic protocols. In: IEEE Symposium on Security and Privacy, pp. 234–248 (1990)
Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. Inf. Comput. 148(1), 1–70 (1999)
Lowe, G.: Casper: A compiler for the analysis of security protocols. Journal of Computer Security 6(1-2), 53–84 (1998)
Armando, A., Basin, D.A., Boichut, Y., Chevalier, Y., Compagna, L., Cuéllar, J., Drielsma, P.H., Héam, P.-C., Kouchnarenko, O., Mantovani, J., Mödersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Viganò, L., Vigneron, L.: The avispa tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281–285. Springer, Heidelberg (2005)
Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security 6(1-2), 85–128 (1998)
Hughes, J., Warnier, M.: The coinductive approach to verifying cryptographic protocols. In: Wirsing, M., Pattinson, D., Hennicker, R. (eds.) Recent Trends in Algebraic Development Techniques. LNCS, vol. 2755, pp. 268–283. Springer, Heidelberg (2003)
Gunter, E.L., Felty, A.P. (eds.): TPHOLs 1997. LNCS, vol. 1275, pp. 19–22. Springer, Heidelberg (1997)
Denker, G., Millen, J.K.: Modeling group communication protocols using multiset term rewriting. Electr. Notes Theor. Comput. Sci. 71 (2002)
Genet, T., Klay, F.: Rewriting for cryptographic protocol verification. In: McAlleste, D.A. (ed.) Automated Deduction - CADE-17. LNCS, vol. 1831, pp. 271–290. Springer, Heidelberg (2000)
Bozga, L., Lakhnech, Y., Périn, M.: Pattern-based abstraction for verifying secrecy in protocols. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol. 2619, pp. 299–314. Springer, Heidelberg (2003)
Monniaux, D.: Abstracting cryptographic protocols with tree automata. Sci. Comput. Program. 47(2-3), 177–202 (2003)
ISO/IEC 9646. Conformance Testing Methodology and Framework (1992)
Jeffrey, A.S.A., Ley-Wild, R.: Dynamic model checking of C cryptographic protocol implementations. In: Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (fcs 2006) (2006)
Goubault-Larrecq, J., Parrennes, F.: Cryptographic protocol analysis on real C code. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 363–379. Springer, Heidelberg (2005)
Bhargavan, K.: Provable implementations of security protocols. In: IEEE Symposium on Logic in Computer Science (LICS 2006), pp. 345–346 (2006)
Breunesse, C.-B., Hubbers, E., Koopman, P., Mostowski, W., Oostdijk, M., Rusu, V., de Vries, R., van Weelden, A., Schreur, R.W., Willemse, T.: Testing the dutch e-passport, Technical report, Radboud University, Nijmegen, The Netherlands (2006)
Dolev, D., Yao, A.C.: On the security of public key protocols. In: Proceedings of the IEEE 22nd Annual Symposium on Foundations of Computer Science, pp. 350–357 (1981)
Technical advisory group on Machine-Readable travel documents. Pki for machine-readable travel documents, version 1.1. Technical report, International Civil Aviation Organization (October 2004)
Lynch, N., Tuttle, M.: Introduction to IO automata. CWI Quarterly, vol. 3(2) (1999)
Carriero, N., Gelernter, D.: Linda in context. Commun. ACM 32(4), 444–458 (1989)
Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods in System Design 19(3), 291–314 (2001)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: The maude 2.0 system. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 76–87. Springer, Heidelberg (2003)
Gaudel, M.-C., James, P.R.: Testing algebraic data types and processes: A unifying theory. Formal Asp. Comput. 10(5-6), 436–451 (1998)
Angluin, D.: Inference of reversible languages. Journal of the ACM 29(3), 741–765 (1982)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Oostdijk, M., Rusu, V., Tretmans, J., de Vries, R.G., Willemse, T.A.C. (2007). Integrating Verification, Testing, and Learning for Cryptographic Protocols. In: Davies, J., Gibbons, J. (eds) Integrated Formal Methods. IFM 2007. Lecture Notes in Computer Science, vol 4591. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73210-5_28
Download citation
DOI: https://doi.org/10.1007/978-3-540-73210-5_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73209-9
Online ISBN: 978-3-540-73210-5
eBook Packages: Computer ScienceComputer Science (R0)