Concurrent Composition and the Isolation Assumption

A security proof almost always considers one protocol instance running against one adversary. Real deployments run many instances, of several protocols, over the same network, sometimes with the same long-term keys, and sometimes with the same randomness source. The gap between the proof and the deployment is not a matter of rigor in the proof; it is a gap in what the theorem quantifies over. Composition theorems exist to close it, and the conditions they require are precisely the parts of a protocol design that are easiest to leave implicit.

What “secure in isolation” leaves out

A standalone proof gives the adversary a set of oracles corresponding to the protocol’s messages and asks it to distinguish a real execution from an ideal one. The adversary may schedule messages, corrupt parties, and choose inputs. It may not, in the usual formulation, run a second instance of the protocol and treat the first instance’s outputs as inputs to the second, because the model has no way to express that the two instances are related.

The attacks this hides are not exotic. A protocol that derives a key from a Diffie–Hellman exchange and uses it directly in a second protocol gives an adversary a value whose distribution in one context is correlated with its distribution in the other. A protocol that uses a counter starting at zero for nonces, run twice with the same key, repeats nonces. A protocol that uses a hash function as both a random oracle and a collision-resistant hash in different components has to satisfy two incompatible idealisations at once, and the composition of the two proofs is not a proof of the composition.

The classic concrete instance is the failure of naive composition for encryption and authentication. Encrypt-then-MAC, MAC-then-encrypt, and encrypt-and-MAC are each individually reasonable-looking, and only one of them composes safely with an arbitrary MAC and an arbitrary encryption scheme. The others admit attacks when the components are instantiated in ways their standalone proofs permit, because the proof of the encryption scheme assumed a ciphertext was delivered unmodified, and the proof of the MAC assumed its input was independent of the key.

Two composition notions and what each buys

Sequential composition says: if protocol A is secure and protocol B is secure, then running A to completion and then B, with B receiving A’s outputs as inputs, is secure. The theorem holds under conditions that are mild but not vacuous: B must be secure against an adversary that knows A’s outputs, and A’s outputs must be treatable as inputs to a secure channel. The proof replaces A with its ideal functionality, then argues B remains secure when its input comes from the ideal functionality rather than from A. It is the composition notion that matches a layered stack, where one protocol establishes a channel and the next uses it.

Concurrent composition says: many instances of the protocol, or of several protocols, run at the same time, interleaved arbitrarily, with a single adversary controlling the network and able to corrupt parties across instances. This is the notion a network protocol needs, and it is strictly stronger. A protocol secure under sequential composition can fail under concurrent composition, because the adversary can use one instance’s messages as another instance’s inputs while both are in flight, and neither instance’s proof accounted for a peer that is mid-handshake elsewhere.

Universal composability, in Canetti’s formulation, is the strongest of these: a protocol is UC-secure if it realises an ideal functionality such that for every adversary there is a simulator producing an indistinguishable view, and the definition is preserved under arbitrary concurrent composition with other UC-secure protocols. The price is that UC security is impossible for many natural tasks without setup assumptions, because a simulator that must produce a view indistinguishable from a real execution has to be able to extract the adversary’s inputs and equivocate on commitments. Commitment, oblivious transfer, and secure computation in the plain model are all ruled out; common reference strings, trusted setup, or signature-based authentication restore possibility.

The practical reading for a protocol designer is narrower than the theory. The properties that make a protocol compose are the ones that give each instance an identity and keep its secrets separate from every other instance’s. A proof that a protocol has those properties, in a model that allows concurrent instances, is a stronger and more useful statement than a proof of the same protocol in a model that allows one.

Session identifiers as the isolation mechanism

The single most effective design element for composition is a session identifier: a value, agreed by both parties at the start of an instance, that every subsequent message of that instance is tagged with. A message that arrives tagged with an identifier the receiver does not recognise is discarded; a message tagged with another instance’s identifier is not accepted even if it is otherwise valid.

The identifier must be unique and must be agreed before any secret-dependent message is sent. It is usually a hash of the first flight, which has the useful property that it commits to the peers’ contributions without requiring a separate round. TLS 1.3’s session identity is effectively the transcript hash, and every derived secret is bound to it through the label context described in domain separation and labelled key derivation. Two concurrent connections therefore cannot share a traffic key even if they share a pre-shared key, because their transcripts differ and the derivation includes the transcript.

What a session identifier does not do is prevent cross-protocol attacks, where an instance of protocol A accepts a message produced by an instance of protocol B. That requires domain separation at the level of the protocol, not the session: a protocol identifier in every hash input, a distinct key derivation label per protocol, and distinct message type spaces. The five-byte protocol label difference between TLS and DTLS, mentioned in domain separation and labelled key derivation, is exactly this mechanism, and its absence is what allows a message from one protocol to be interpreted as a message in another.

The two mechanisms are complementary and both are needed. A session identifier separates instances of one protocol; a protocol identifier separates one protocol from another. A protocol with session identifiers but no protocol identifier is vulnerable to being fed another protocol’s messages with a matching session tag, and a protocol with a protocol identifier but no session identifier is vulnerable to having two of its own instances spliced together.

Where composition theorems stop applying

Three assumptions are commonly violated by real deployments, and each violation invalidates the theorem without necessarily producing a visible bug.

Shared randomness. Composition proofs assume each instance’s randomness is independent. A virtual machine snapshot restored to two hosts, a forked process inheriting a seeded PRNG, or a hardware random source that fails to reseed after resume all break this. The resulting nonce reuse is the failure described in nonce construction and reuse limits, and it is fatal rather than degrading. The protocol-level defence is to mix fresh entropy into every key derivation and to refuse to operate when the source is unavailable, which is a deployment requirement rather than a cryptographic one.

Shared long-term keys across protocols. A signing key used to sign handshake transcripts in two protocols can have its signatures reinterpreted if the two protocols’ signed structures are not distinguishable. The composition theorem for the two protocols would require that the key be used by one of them, or that the signed structures be domain-separated. Key reuse across protocols is common in practice because key management is expensive, which makes the domain separation requirement a design obligation rather than an optional refinement.

State that outlives the instance. A protocol whose security argument assumes each instance starts from a clean state fails when an instance is resumed, forked, or rolled back. Resumption is the designed case and is usually handled; forking and rollback are not. A protocol that stores a sequence counter in memory and resets it on process start has an instance that, from the peer’s perspective, restarts in the middle of a key’s lifetime.

A concrete check for a new protocol

The following set of checks is a practical substitute for a composition proof, and it catches the failures that a standalone proof does not.

Every message should carry a session identifier that both parties agreed before any key-dependent value was sent. Every key derivation should include a protocol identifier and a version. Every instance’s randomness should come from a source independent of every other instance’s. Every long-term key should be used by exactly one protocol, or the signed and MACed structures should be domain-separated across the protocols that share it. Resumption and rekeying should derive a fresh key rather than reset a counter under an old one. And each of these should be enforced by the message format, rather than by a convention in the implementation.

The last clause is the one that decides whether the composition argument holds. A property that lives in the code can be lost in a refactor; a property that lives in the wire format is checked by every peer that parses it.

Per-instance state a protocol must carry, and what each field defends against:

  session_id      -- agreed in the first flight, tags every later message
                     (splicing of two concurrent instances)
  proto_label     -- protocol name and version in every hash and KDF input
                     (cross-protocol reinterpretation)
  key_epoch       -- increments on every rekey; resetting the nonce counter
                     is legal only when this changes
  rand_source_id  -- identifies the entropy instance; a repeated value
                     signals a fork or a snapshot rollback

The framing that makes such properties expressible at all is the subject of unambiguous message framing, and the binding of an outer channel’s identity to an inner protocol’s authentication is the composition case examined in channel binding and transport identity.

One further limit deserves to be stated plainly. Composition theorems preserve the security notion they are stated in, and no more. A protocol proved secure for confidentiality and integrity of message streams says nothing about traffic analysis, about the metadata the protocol exposes, or about what an adversary learns from message sizes and timing. Those properties are outside the model, so composing the protocol with anything does not carry them, and a design that needs them requires a different model rather than a stronger proof of the same one.