Abstract
Cryptographic protocols are useful for engineering trust in transactions. There are several languages for describing these protocols, but these tend to capture the communications from the perspective of an individual role. In contrast, traditional protocol descriptions as found in a state of nature tend to employ a whole-protocol description, resulting in an impedance mismatch.
In this paper we present two results to address this gap between human descriptions and deployable specifications. The first is an end-point projection technique that consumes an explicit whole-protocol description and generates specifications that capture the behavior of each participant role. In practice, however, many whole-protocol descriptions contain idiomatic forms of implicit specification. We therefore present our second result, a transformation that identifies and eliminates these implicit patterns, thereby preparing protocols for end-point projection.
Concretely, our tools consume protocols written in our whole-protocol language, wppl, and generate role descriptions in the cryptographic protocol programming language, cppl. We have formalized and established properties of the transformations using the Coq proof assistant. We have validated our transformations by applying them successfully to most of the protocols in the spore repository.
Keywords
- Information Asymmetry
- Security Protocol
- Cryptographic Protocol
- Denotational Semantic
- Cryptographic Primitive
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.
Download to read the full chapter text
Chapter PDF
References
Abadi, M.: Security protocols and their properties. In: Foundations of Secure Computation (2000)
Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. Information and Computation 148(1), 1–70 (1999)
Armando, A., Basin, D.A., Bouallagui, M., Chevalier, Y., Compagna, L., Mödersheim, S., Rusinowitch, M., Turuani, M., Viganò, L., Vigneron, L.: The AVISS security protocol analysis tool. In: Computer Aided Verification (2002)
Bodei, C., Buchholtz, M., Degano, P., Nielson, F., Nielson, H.R.: Automatic validation of protocol narration. In: Computer Security Foundations Workshop (2003)
Bodei, C., Buchholtz, M., Degano, P., Nielson, F., Nielson, H.R.: Static validation of security protocols. Journal of Computer Security 13(3), 347–390 (2005)
Briais, S., Nestmann, U.: A formal semantics for protocol narrations. Theoretical Computer Science 389(3), 484–511 (2007)
Burrows, M., Abadi, M., Needham, R.: A logic of authentication. Proceedings of the Royal Society Series A 426(1871), 233–271 (1871)
Caleiro, C., Viganò, L., Basin, D.: On the semantics of Alice&Bob specifications of security protocols. Theoretical Computer Science 367(1-2), 88–122 (2006)
Carbone, M., Honda, K., Yoshida, N.: Structured communication-centred programming for web services. In: European Symposium on Programming (2007)
Corin, R., Denielou, P.-M., Fournet, C., Bhargavan, K., Leifer, J.: Secure implementations for typed session abstractions. In: Computer Security Foundations Symposium (2007)
Diffie, W., Hellman, M.: New directions in cryptography. IEEE Transactions on Information Theory 22(6), 644–654 (1976)
Dolev, D., Yao, A.: On the security of public-key protocols. IEEE Transactions on Information Theory 29, 198–208 (1983)
Durante, A., Focardi, R., Gorrieri, R.: A compiler for analyzing cryptographic protocols using noninterference. ACM Transactions on Software Engineering and Methodology 9(4), 488–528 (2000)
Garay, J.A., Jakobsson, M., MacKenzie, P.: Abuse-free optimistic contract signing. In: International Cryptology Conference (1999)
Guttman, J.D., Herzog, J.C., Ramsdell, J.D., Sniffen, B.T.: Programming cryptographic protocols. In: Trust in Global Computing (2005)
Jacquemard, F., Rusinowitch, M., Vigneron, L.: Compiling and verifying security protocols. Logic for Programming and Automated Reasoning (2000)
Kao, I.L., Chow, R.: An efficient and secure authentication protocol using uncertified keys. Operating Systems Review 29(3), 14–21 (1995)
Lowe, G.: Casper: A compiler for the analysis of security protocols. In: Computer Security Foundations Workshop (1997)
Meadows, C.: A model of computation for the NRL protocol analyzer. In: Computer Security Foundations Workshop (1994)
Millen, J., Muller, F.: Cryptographic protocol generation from CAPSL. Technical Report SRI-CSL-01-07, SRI International (December 2001)
Neuman, B.C., Ts’o, T.: Kerberos: An authentication service for computer networks. Technical Report ISI/RS-94-399, USC/ISI (1994)
Project EVA. Security protocols open repository (2007), http://www.lsv.ens-cachan.fr/spore/
Sabri, K.E., Khedri, R.: A mathematical framework to capture agent explicit knowledge in cryptographic protocols. Technical Report CAS-07-04-RK, McMaster University (2007)
The Coq development team. The Coq proof assistant reference manual, 8.1 edition (2007)
Weiser, M.: Program slicing. In: International Conference on Software Engineering (1981)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
McCarthy, J., Krishnamurthi, S. (2008). Cryptographic Protocol Explication and End-Point Projection. In: Jajodia, S., Lopez, J. (eds) Computer Security - ESORICS 2008. ESORICS 2008. Lecture Notes in Computer Science, vol 5283. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-88313-5_34
Download citation
DOI: https://doi.org/10.1007/978-3-540-88313-5_34
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-88312-8
Online ISBN: 978-3-540-88313-5
eBook Packages: Computer ScienceComputer Science (R0)