Trusted Multiplexing of Cryptographic Protocols

Abstract. We present an analysis that determines when it is possible to multiplex a pair of cryptographic protocols. We present a transformation that improves the coverage of this analysis on common protocol formulations. We discuss the gap between the merely possible and the pragmatic through an optimization that informs a multiplexer. We also address the security ramifications of trusting external parties for this task and evaluate our work on a large repository of cryptographic protocols. We have formally verified this work using the Coq proof assistant. 1 Problem and Motivation A fundamental aspect of a cryptographic protocol is the set of messages that it may accept. Protocol specifications contain patterns that specify the shape of the messages they accept. These patterns describe an infinite set of messages, because the variables that appear in them may be bound to innumerable values. We call this set a protocol’s message space. There is a history of attacks on protocols b...

• Type: Conference
• Year: 2009
• Where: IFIP
• Authors: Jay A. McCarthy, Shriram Krishnamurthi
• Keywords: Common Protocol Formulations, Communications, Cryptographic Protocol, IFIP 2009, Message Space