Abstract
A transformation F between protocols associates the messages sent and received by participants in a protocol \({\it\Pi}_1\) with messages sent and received in some \({\it\Pi}_2\). Transformations are useful for modeling protocol design, protocol composition, and the services that protocols provide.
A protocol transformation determines a map from partial behaviors \({\mathbb A}_1\) of \({\it\Pi}_1\)—which we call “skeletons”—to skeletons \(F({\mathbb A}_1)\) of \({\it\Pi}_2\). Good transformations should act as functors, preserving homomorphisms (information-preserving maps) from one \({\it\Pi}_1\)-skeleton to another. Thus, if \(H:{\mathbb A}_1\mapsto{\mathbb A}_2\) is a homomorphism between \({\it\Pi}_1\)-skeletons, then there should be a homomorphism \(F(H): F({\mathbb A}_1)\mapsto F({\mathbb A}_2)\) between their images in \({\it\Pi}_2\).
We illustrate protocol transformation by examples, and show that our definition ensures that transformations act as functors.
Supported by the MITRE-Sponsored Research program.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
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.
References
Carbone, M., Honda, K., Yoshida, N.: Structured communication-centred programming for web services. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 2–17. Springer, Heidelberg (2007)
Cortier, V., Delaitre, J., Delaune, S.: Safely composing security protocols. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 352–363. Springer, Heidelberg (2007)
Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: Abstraction and refinement in protocol derivation. In: Proceedings of Computer Security Foundations Workshop. IEEE CS Press, Los Alamitos (2004)
Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: A derivation system and compositional logic for security protocols. Journal of Computer Security 13(3), 423–482 (2005)
Doghmi, S.F., Guttman, J.D., Thayer, F.J.: Completeness of the authentication tests. In: Biskup, J., Lopez, J. (eds.) ESORICS 2007. LNCS, vol. 4734, pp. 106–121. Springer, Heidelberg (2007)
Doghmi, S.F., Guttman, J.D., Thayer, F.J.: Searching for shapes in cryptographic protocols. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 523–537. Springer, Heidelberg (2007), http://eprint.iacr.org/2006/435
Fröschle, S.: Adding branching to the strand space model. In: Proceedings of EXPRESS 2008. Electronic Notes in Theoretical Computer Science. Elsevier, Amsterdam (2008) (to appear)
Guttman, J.D.: Cryptographic protocol composition via the authentication tests. In: de Alfaro, L. (ed.) Foundations of Software Science and Computation Structures (FOSSACS). LNCS, vol. 5504, pp. 303–317. Springer, Heidelberg (2009)
Guttman, J.D., Herzog, J.C., Ramsdell, J.D., Sniffen, B.T.: Programming cryptographic protocols. In: De Nicola, R., Sangiorgi, D. (eds.) TGC 2005. LNCS, vol. 3705, pp. 116–145. Springer, Heidelberg (2005)
Guttman, J.D., Thayer, F.J.: Protocol independence through disjoint encryption. In: Proceedings, 13th Computer Security Foundations Workshop, IEEE Computer Society Press, Los Alamitos (2000)
Guttman, J.D., Thayer, F.J.: Authentication tests and the structure of bundles. Theoretical Computer Science 283(2), 333–380 (2002); Conference version appeared in IEEE Symposium on Security and Privacy (May 2000)
Hui, M.L., Lowe, G.: Fault-preserving simplifying transformations for security protocols. Journal of Computer Security 9(1/2), 3–46 (2001)
Mostrous, D., Yoshida, N., Honda, K.: Global principal typing in partially commutative asynchronous sessions. In: ESOP Proceedings. LNCS. Springer, Heidelberg (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Guttman, J.D. (2009). Transformations between Cryptographic Protocols. In: Degano, P., Viganò, L. (eds) Foundations and Applications of Security Analysis. ARSPA-WITS 2009. Lecture Notes in Computer Science, vol 5511. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-03459-6_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-03459-6_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-03458-9
Online ISBN: 978-3-642-03459-6
eBook Packages: Computer ScienceComputer Science (R0)