Abstract
Protocol narrations are an informal means to describe, in an idealistic manner, the functioning of cryptographic protocols as a single intended sequence of cryptographic message exchanges among the protocol’s participants. Protocol narrations have also been informally “turned into” a number of formal protocol descriptions, e.g., using the spi-calculus. In this paper, we propose a direct formal operational semantics for protocol narrations that fixes a particular and, as we argue, well-motivated interpretation on how the involved protocol participants are supposed to execute. Based on this semantics, we explain and formally justify a natural and precise translation of narrations into spi-calculus.
An erratum to this chapter can be found at http://dx.doi.org/10.1007/11580850_20 .
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
Abadi, M.: Security Protocols and their Properties. In: Foundations of Secure Computation, pp. 39–60. NATO ASI. IOS Press, Amsterdam (2000)
Abadi, M., Gordon, A.D.: A Calculus for Cryptographic Protocols: The Spi Calculus. Information and Computation 148(1), 1–70 (1999)
Bodei, C., Buchholtz, M., Degano, P., Nielson, F., Nielson, H.: Automatic validation of protocol narration. In: Proceedings of 16th IEEE Computer Security Foundations Workshop (CSFW 16), pp. 126–140 (2003)
Borgström, J., Briais, S., Nestmann, U.: Symbolic Bisimulation in the Spi Calculus. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 161–176. Springer, Heidelberg (2004)
Blanchet, B.: Automatic Verification of Cryptographic Protocols: A Logic Programming Approach. In: Proceedings of Principles and Practice of Declarative Programming (PPDP 2003). ACM, New York (2003)
Basin, D., Mödersheim, S., Viganò, L.: An On-the-Fly Model-Checker for Security Protocol Analysis. In: Snekkenes, E., Gollmann, D. (eds.) ESORICS 2003. LNCS, vol. 2808, pp. 253–270. Springer, Heidelberg (2003)
Briais, S.: Formal proofs about hedges using the Coq proof assistant (2004), http://lamp.epfl.ch/~sbriais/spi/hedges/hedge.html
Clark, J.A., Jacob, J.L.: A survey of authentication protocol literature. Technical Report 1.0, University of York (1997)
Cremers, C., Mauw, S.: Operational Semantics of Security Protocols. In: Leue, S., Systä, T.J. (eds.) Scenarios: Models, Transformations and Tools. LNCS, vol. 3466, pp. 66–89. Springer, Heidelberg (2005)
Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory IT-29(12), 198–208 (1983)
Gensoul, C.: Spyer — un compilateur de protocoles cryptographiques. Semester Project Report, EPFL (July 2003)
Jacquemard, F., Rusinowitch, M., Vigneron, L.: Compiling and Verifying Security Protocols. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol. 1955, pp. 131–160. Springer, Heidelberg (2000)
Lowe, G.: Casper: A Compiler for the Analysis of Security Protocols. Journal of Computer Security 6, 53–84 (1998)
Millen, J.K.: CAPSL: Common Authentication Protocol Specification Language, http://www.csl.sri.com/users/millen/capsl/
Menezes, A.J., van Oorschot, P.C., Vanstone, S.A.: Handbook of Applied Cryptography. CRC Press, Boca Raton (1996)
Paulson, L.C.: The Inductive Approach to Verifying Cryptographic Protocols. Journal of Computer Security 6(1-2), 85–128 (1998)
Sumii, E., Tatsuzawa, H., Yonezawa, A.: Translating Security Protocols from Informal Notation into Spi Calculus. IPSJ Transactions on Programming 45 Written in Japanese, abstract in English (2005) (to appear)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Briais, S., Nestmann, U. (2005). A Formal Semantics for Protocol Narrations. In: De Nicola, R., Sangiorgi, D. (eds) Trustworthy Global Computing. TGC 2005. Lecture Notes in Computer Science, vol 3705. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11580850_10
Download citation
DOI: https://doi.org/10.1007/11580850_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-30007-6
Online ISBN: 978-3-540-31483-7
eBook Packages: Computer ScienceComputer Science (R0)