Secure Pseudonymous Channels

Channels are an abstraction of the many concrete techniques to enforce particular properties of message transmissions such as encryption. We consider here three basic kinds of channels—authentic, confidential, and secure—where agents may be identified by pseudonyms rather than by their real names. We define the meaning of channels as assumptions, i.e. when a protocol relies on channels with particular properties for the transmission of some of its messages. We also define the meaning of channels as goals, i.e. when a protocol aims at establishing a particular kind of channel. This gives rise to an interesting question: given that we have verified that a protocol P 2 provides its goals under the assumption of a particular kind of channel, can we then replace the assumed channel with an arbitrary protocol P 1 that provides such a channel? In general, the answer is negative, while we prove that under certain restrictions such a compositionality result is possible.