Transformations between Cryptographic Protocols

Abstract. A transformation F between protocols associates the messages sent and received by participants in a protocol Π1 with messages sent and received in some Π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 A1 of Π1—which we call “skeletons”—to skeletons F(A1) of Π2. Good transformations should act as functors, preserving homomorphisms (informationpreserving maps) from one Π1-skeleton to another. Thus, if H : A1 → A2 is a homomorphism between Π1-skeletons, then there should be a homomorphism F(H): F(A1) → F(A2) between their images in Π2. We illustrate protocol transformation by examples, and show that our definition ensures that transformations act as functors.

• Type: Conference
• Year: 2009
• Where: IFIP
• Authors: Joshua D. Guttman
• Keywords: Communications, IFIP 2009, Protocol Composition, Protocol Design, Protocol Transformation