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
, 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
, 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
provides its goals under the assumption of a particular kind of channel, can we then replace the assumed channel with an arbitrary protocol
that provides such a channel? In general, the answer is negative, while we prove that under certain restrictions such a compositionality result is possible.