Secure Pseudonymous Channels (updated version: August 3, 2009)

Different kinds of channels can be employed in security protocols and web services as a means of securing the communication. We consider here three basic kinds of channels: authentic, confidential, and secure.

We define channels as assumptions, i.e. when the messages of a protocol may be transmitted over such channels. More specifically, we define the Ideal Channel Model, which describes the ideal functionality of a channel, and the Cryptographic Channel Model, which employes concrete cryptographic messages on insecure channels. We relate these two models by showing that attacks in either model can be simulated in the other.

We also define the meaning of channels as goals, i.e. when a protocol has the goal of establishing a particular kind of channel. This gives rise to an interesting question: given that we have verified that a protocol P2 provides its goals under the assumption of a particular kind of channel, can we then replace the assumed channel with an arbitrary protocol P1 that provides such a channel? In general, the answer is negative, while we prove that under certain restrictions such a compositionality result is possible.

Finally, we generalize all our results to channels where agents may be identified by pseudonyms rather than by their real names, and also consider channels that ensure the freshness of messages by suppressing message replay.

A condensed version of this report has appeared in: "Computer Security - ESORICS 2009", Lecture Notes in Computer Science, Vol. 5789 (Springer / Heidelberg September 2009), pp. 337-354