{'fraction_non_alphanumeric': 0.05345741666561725, 'fraction_numerical': 0.007921016509463663, 'mean_word_length': 4.341360059191498, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 1, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 17, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
A theory of protocol composition

Real-world communication protocols are often built out of a number of simpler protocols that cater for some specific functionality (e.g., banking, authentication). However much of the formal definitions of protocols used for program verification treat protocols as monolithic units. Composition is considered for implementations of a protocol, but not for the protocols themselves as engineering components. We propose primitives and techniques for the modular composition of protocols. Our notion of composition defines an interleaving of two or more protocols in a way that satisfies user-specified context-dependent constraints which serve to explain “contact points” between the protocols. The resulting approach gives a theoretical basis for protocol (re-)engineering based on a process calculus with constraint annotations. We have implemented our approach as a tool for Erlang that supports generation of protocol compositions with formal guarantees, and code generation/extraction.

This up-front, single point of definition runs contrary to the human aspects of real-world programming, in which a programmer gradually pieces together their code, perhaps heavily leveraging libraries, to reach their intended goal; programs are gradual compositions. A view that is globally defined once does not reflect the real process of software composition. In contrast, a view that defines lots of local protocols or sub-protocols places the burden of configuring their interaction on the programmer: programmers must themselves work in a situation where they have to consider many smaller protocols and work out how they want dependencies between them to be resolved. Instead, a flexible, non-monolithic notion of composition (and possibly recomposition, when a piece of code is refactored and rewritten, or reused) is needed to support the engineering of protocol-dependent code. Ideally, such a notion should support well-founded semi-automated protocol composition and implementation with formal guarantees.
This work lays a foundation for compositional protocol engineering based on a notion of interleaving composition of protocols. An interleaving composition of two protocols 'weaves' them together into a single unified protocol, differing from a sequential composition in which one protocol follows the other, or one's inputs are coupled to the other's outputs. We address, in general terms, the question of what a correct protocol composition is, and introduce a syntactic definition of composition that characterises finite sets of correct interleaving compositions, each representing a 'good way' to interleave the component protocols with respect to domain-specific user-specified constraints. The resulting approach gives a theoretical basis for protocol (re-)engineering based on a process calculus with constraint annotations. Interleaving composition has the purpose of enhancing the awareness (of engineers and programmers) of what a protocol means, as well as facilitating the reasoning about its properties. We give an algorithmic implementation of interleaving composition supporting the process of defining protocols and inspecting the generated compositions, and code generation for Erlang, producing skeletons of processes following a given protocol (composite or not). Code generation is based on Erlang/OTP gen_statem behaviour [1] allowing code to be automatically migrated in subsequent compositions and reengineering. Correspondence of our protocol language with Finite State Machines (FSM) (via directed graphs) yields a straightforward link between protocols and FSM-structured code.
A related line of work is that of automata compositions. Team Automata, introduced in [7, 16], provide several means of composing machines via synchronization on their common actions, and give a formal framework for composition. Unlike Team Automata, we express composition constraints orthogonally to communication: instead of synchronization on common actions, we use 'asserts'/'requires' as asymmetric contact points for composition, and reason about the properties of a composite protocol from the perspective of the application logic. The resulting composition relation given in this work is not characterizable as one of the synchronizations of Team Automata (discussed further in Section 7). Another related line of work defines composition as run-time weaving, for example applying principles of aspect-oriented programming to protocol composition [32]. Unlike the aforementioned work, we statically derive protocol compositions that enable (human/automated) reasoning and verification of their properties.
Motivating example Consider the banking protocol discussed earlier in this section. The banking protocol can be formally specified as S B in Figure 1 using a process calculus notation. S B repeatedly (via a fixed point µt) offers (denoted &) three options: option statement is followed by a send action (denoted !) of a message with the bank statement, option payment is followed by a receive action (denoted ?) with details of the payment, and option logout is followed by termination of the protocol (denoted end). After each of the first two options, the control flow goes back to the initial state (via t).
Assume now that we want to extend S B with two-level authentication: one level for accessing the service and one additional level for each payment transaction. Concretely, we wish to compose S B with the PIN/TAN (Personal Identification Number/Transaction Authentication Number) protocol modelled in Figure 1 as S A which offers two-stage authentication. The first stage is pin authentication: the server receives a pin and decides (⊕) whether to continue (i.e., ok) or terminate (i.e., fail). If ok is chosen, the protocol enters a loop (i.e., µr) that manages multiple TAN authentications, supporting multiple transactions requiring an additional level of security. In the loop, the server sends an identifier id for which the client must send back a tan. The server notifies the client about the correctness of the tan with either ok or fail.
We want to compose the banking and authentication protocols into one single protocol where the actions of the two protocols follow a specific interleaving: access to the banking service requires a PIN authentication, and each payment instance/iteration requires an extra TAN authentication (see dotted arrows in Figure 1). This specific interleaving entails an authorization property, which we later express and ensure by using assertion annotations. Moreover, we want tools that facilitate (re-)engineering of programs implementing interleaving compositions. For example, we want to obtain a skeleton implementation for the banking and PIN/TAN protocol, and in a second stage we want to reuse the code when composing banking with a different multi-factor authentication protocol, e.g., offering other options besides TAN, such as keycard authentication.
Contributions Central to our work is our definition of interleaving composition. We use a process-calculus-based notation for protocols with 'assertions' that specify contact points and constraints between component protocols (Section 2). Interleaving composition is defined relationally as there may be many possible valid interleaved protocols (or even none) (Section 3). In Section 4, we prove that our composition relation returns correct interleaving compositions. Correctness comprises three properties: (1) behaviour preservation (Theorem 1): interleaving compositions only perform sequences of actions that may be performed by either of the component protocols, (2) fairness (Theorem 3): interleaving compositions eventually execute the next available action of each protocol, and (3) well-assertedness (Proposition 3): interleaving compositions always satisfy requirements prescribed by the assertions in the protocols being composed. Thus, we establish that the composition relation produces sets of correct-by-construction protocol compositions. In Section 3.1 we provide two less restrictive definitions of interleaving composition with the use of two additional rules, weak branching and correlating branching that are able to capture a larger number of scenarios but enjoy a weaker fairness property (Theorem 2).
In Section 5, we introduce a tool to aid code reuse and modularisation in Erlang. The tool implements interleaving composition, and provides code generation as well as protocol extraction from existing code. For instance, starting with two gen statem separated implementations of the authentication and banking protocols, we can extract their underlying protocols (together with any assertion constraints they may have), automatically compose the extracted protocols and generate a new Erlang module.
In Section 6, we discuss instantiating our protocol language into well-known formalisms such as CCS [27] and Session Types [19,8,20], and illustrate possible synergies. Section 7 discusses related work.

Asserted Protocols
We introduce a simple language of protocols to abstractly capture essential features of sequential computation: sequencing, choice, and looping. Our protocol language somewhat resembles Milner's CCS [27] or the π-calculus [30] (but without parallel composition or name restriction) and has some relation to Kleene algebras [24] but we provide more general patterns of recursion via recursive binders rather than a single closure operator.
Generally, two protocols can be composed in several ways, each reflecting a possible interleaving of the actions of the two protocols. Not all such interleavings are meaningful depending on the scenario or domain. The protocol language therefore includes a notion of 'assertions' which can be used to capture the behavioural constraints of a protocol to guide interleaving composition in a meaningful way; they act as a specification of minimal 'contact points' between protocols akin to pre-and post-conditions.
Following an explanation of the syntax and various examples, we give an operational model to the protocol language which serves to explain both the program semantics which it abstracts, and the meaning of the assertion actions.
Definition 1 (Asserted protocols). Asserted protocols, or just protocols for short, are ranged over by S and are defined as followsing syntax rules: assert(n).S assert (produce) assertion fragment | require(n).S require | consume(n).S consume where p ∈ P ranges over prefixing actions, l ∈ L ranges over labels used to label each branch of the n-ary branching construct, t ranges over protocol variables for recursive protocol definitions, n ∈ N ranges over names of logical atoms used by assertions. The sets of actions P, labels L, and names N are parameters to the language and thus can be freely chosen. Furthermore + ranges over a set of operators O used to represent branching choice and thus can also be instantiated.
The prefixing action provides sequential composition (in the style of process calculi). Branching is n-ary, taking the form of a set of protocol choices with a label l i for each choice. Looping behaviour is captured via the recursive protocol variable binding µt, which respects the usual rules of binders, and recursion variables t. We assume variables to be guarded in the standard way (they only occur under actions or branching). Unless otherwise stated, we consider protocols to be closed with respect to these recursion variables.
Protocols can be annotated with assertions to introduce guarantees assert(n), requirements require(n), and linear requirements consume(n): assert(n) introduces a true logical atom n into the scope of the following protocol, require(n) allows the protocol to proceed only if n is in scope, and consume(n) removes the truth of logical atom n from the scope of the following protocol.
Remark 1 (Language instantiation). The protocol language can be instantiated to model different protocol languages. In the examples we often instantiate the prefixing actions P to sends !T and receives ?T capturing interaction with some other concurrent program, i.e., p ∈ {!T, ?T} where T is a type (e.g., booleans, integers, strings), and instantiate choice + to a pair of polarised choice operators: + ∈ {⊕, &}, either offering of a choice ⊕ or selecting from amongst some choices &. This yields a session types-like syntax like the one of Dardha et al. [14]. Different instantiations are possible, as shown in Section 6.
Examples often colour assertions green and labels purple for readability.

Assertion examples
Consider a payment process ?pay.end that receives a payment and terminates, and a dispatch process !item.end that sends a product link and terminates. We can interleave these two protocols in two ways: ?pay.!item.end (payment first) or !item.?pay.end (dispatch first). By using assertions, we can require that payment happens before dispatch: below, I 1 asserts the logical atom paid as a post-condition to receiving payment while in I 2 the sending action depends on the logical atom paid as a pre-condition, and in doing so consumes it.
I 1 =?pay.assert(paid).end I 2 = consume(paid).!item.end The only interleaving composition of I 1 and I 2 that satisfies the constraints posed by the assertions is: ?pay.assert(paid).consume(paid).!item.end The exact definition of well-assertedness, that specified constraints are satisfied in all of the protocol's executions, will be given later in this section (Definition 6). Linear constraints model guarantees that can be used only once. For example, the scenario "in a recursive payment/dispatch scenario there is one dispatch for each one payment " can be modelled by recursive payment µt.?pay.assert(paid).t and recursive dispatch µr.consume(paid).!item.r protocols. Non-linear constraint require(n) does not consume guarantees. It can express, e.g., that at a prepaid buffet, payment remains valid (hungry) until the meal ends (end): µt.&{hungry : require(paid).!food.t, end : consume(paid).end} Example 1 (Asserted banking and authentication protocols). Returning to the banking and PIN/TAN example, the informal requirement discussed in the introduction can be modelled using assertions. An asserted version of the banking protocol, given below as S ′ B , uses require(pin) to ensure a successful PIN authentication before accessing the banking menu; consume(tan) to require one successful TAN authentication for each iteration involving a payment; and consume(pin) to remove the PIN guarantee when logging out. Assertions assert(pay) and consume(pay) ensure TAN authentication only happens in case of payment.

Protocols semantics
The semantics of a protocol is given in Definition 3 in terms of an environment that keeps track of guarantees, and lets protocols progress only if stated guarantees can be met by the environment. The semantics is up to the (standard) structural equivalence rules given in Definition 2 where S[µt.S/t] is the one-time unfolding of µt.S (all occurrences of t are substituted with µt.S).
Definition 2 (Structural congruence). Protocols have a structural congruence relation ≡ (used in reasoning and the proofs for this paper) where: Definition 3 (Operational semantics). The semantics of protocols is defined by a labelled-transition system (LTS) over configurations of the form (A, S) where A ranges over 'environments': sets of logical atoms (i.e., A ⊆ N ), with transition labels ℓ ::= p | +l | assert(n) | require(n) | consume(n) and the transition rules below:

Rec
Rules Inter and Branch always allow a protocol to proceed with some action, resulting in the appropriate continuation, without any effect to the environment. Rule Assert adds atom n to the environment. Rules Require and Consume both require the presence of atom n in the environment for the protocol to continue. Although Require leaves the environment unchanged, Consume consumes the atom n from the environment. In Rec , S ′ [µt.S/t] means that the recursive protocol is unfolded by substituting µt.S for t in S ′ .
We write: for a vector ℓ. We omit labels and target states where immaterial.
Definition 5 (Progress). A protocol S enjoys progress if every state (A ′ , S ′ ) reachable from (∅, S) is not stuck.
A protocol may reach a stuck state when it does not have sufficient preconditions in its environment A. In Example 1, S ′ B does not enjoy progress because the pre-condition expressed by require(pin) cannot be met; similarly, S ′ A does not enjoy progress because of unmet pre-condition consume(pay).

Well-assertedness
The assertions are key to generating meaningful compositions of protocols. Following the labelled transitions semantics, we define a judgment which captures the pre-and post-conditions of a protocol implied by its assertions. We use the notation A {S} A ′ reminiscent of a Hoare triple where A and A ′ are pre-and post-conditions of S respectively.
Definition 6 (Well-assertedness). Let A be a set of names. Well-assertedness of a protocol S with respect to A is defined below, as an inference system on judgments of the form A {S} A ′ , where A ′ is the set of names (logical atoms) resulting after the execution of S given the set of names A.
We write A {S} when A {S} A ′ for some A ′ (i.e., when the post-condition is not of interest). We say that S is very-well-asserted if ∅ {S}. We say that a state (A, S) is well-asserted if S is well-asserted with respect to A.
Protocols S ′ A and S ′ B in Example 1 are not very-well-asserted but they are wellasserted with respect to {pin, tan} and {pay}, respectively.
We now consider some properties of well-asserted protocols. Proofs are in Appendix C. Firstly, protocols that do not contain assertions are very-well-asserted: Proposition 1 (Very-well-assertedness) If S is generated by the grammar in Definition 1 without the assertion fragment then it is very-well-asserted.
Next, well-asserted protocols can have their environment weakened, akin to pre-condition weakening in Hoare logic: Next, Lemma 1 states that the redux of a well-asserted state is well-asserted, moreover the postconditions are not weakened by reduction: Lemma 2 (Well-asserted protocols are not stuck). If A {S} and S is closed with respect to recursion variables (fv(S) = ∅) then (A, S) is not stuck.
Next, Lemma 3 shows that if a protocol "gets stuck", this is because it does not have enough preconditions to proceed. Thus, the protocol needs assumptions that may be provided by other protocols it could be composed with.
Lemma 3 follows by induction on the length of a protocol's execution, combined with Lemmas 1 and 2.
We next introduce protocol composition, which produces protocols that are meaningful with respect to their assertions (i.e., that exhibit progress).

Interleaving Compositions
We compose protocols by computing syntactic interleavings. We derive the 'interleaving composition' of two protocols S 1 and S 2 via a relation with judgments of the form: T L , T R , A, S 1 • S 2 ⊢ S where S is the resulting composed protocol, and A is the set of names (i.e., assertions) provided by the environment to S. Environments T L and T R are sets of protocol variables that are free in S 1 and S 2 respectively, and are used to handle composition of recursive protocols. The composition relation is illustrated by examples after its definition in Definition 7.
Definition 7 (Interleaving composition). Let Top(µt.S) = {t} and Top(S) = ∅ for all other cases of S. Interleaving composition is defined as follows.
The composition of a recursive protocol with a non-recursive one is delicate. An approach to composition that is too permissive could generate interleaving compositions that violate behaviour preservation and fairness. These properties will be formally introduced later, but we offer an intuition here so that the reader can understand some of our design choices for Definition 7.
The intuition of behaviour preservation is: 'All executions allowed by an interleaving composition preserve the interaction structures of each component protocol that comprises it'. When composing a recursive protocol with a non-recursive one e.g., S 1 = µt.!p 1 .t with S ′ 2 = !p 2 .end, then we would not want to derive the following protocol: S = µt.!p 1 .!p 2 .t. This allows e.g., execution !p 1 , !p 2 , !p 1 , !p 2 where action !p 2 is repeatedly executed (while S 2 only prescribes one instance of !p 2 ) hence violating behaviour preservation (Theorem 1). Our rules do not allow S above to be derived from S 1 and S ′ 2 , thanks to rule [call] checking that the protocols being composed are indeed recursive protocols that have been correctly merged (i.e., share a recursion variable t). Below, for illustration purposes, we use to denote 'non-derivable protocol': [sym] {t}, ∅, ∅, t • !p 2 .end ⊢ !p 2 .
Another consideration when composing recursive and non-recursive protocols is fairness. The intuition of fairness is: 'In all executions allowed by an interleaving composition, each component protocol can proceed until it terminates'. For the two protocols S 1 and S ′ 2 given above, if we interleave them so that S 1 'comes first' we may obtain the following interleaving composition µt.!p 1 .t that morally represents the protocol that behaves as S ′ 2 after an infinite loop. Such a protocol clearly violates fairness. Similarly, an interleaving µt.!p 1 .!p 2 .end would violate fairness by preventing S 1 from proceeding until it terminates (i.e., forever) again compromising fairness (Theorem 2). A composition that satisfies fairness is one in which the terminating protocol 'comes first': !p 2 .µt.!p 1 .t. Such a composition is obtained via [rec3]. Crucially, [rec3] only allows a recursive protocol to be introduced in an interleaving composition when the non-recursive component has already been all merged (i.e., it is end). Thus, we can derive: The premise fv(µt 1 .!p 1 .t 1 ) = ∅ prevents [rec3] being used inappropriately in case of nested recursion, e.g., to prevent the composition of µt 1 .!p 1 .µt 3 .!p 1 .t 1 and !p 2 .end to produce (with some applications of [rec1], [act], [sym], and finally [rec3]) µt 1 .!p 1 .!p 2 .µt 3 .!p 1 .t 1 , which would violate behaviour preservation.

Variations on the branching rule
The branching rule of interleaving composition can be viewed as a distributivity property: sequential composition after a control-flow branch can be distributed inside the branches. Algebraically, we can informally describe this distributivity exhibited by the branching rule as follows, for a 2-way branch (sans labelling): . Such a property is familiar in Kleene algebra models of programs and program reasoning [24] and monotone dataflow frameworks in static analysis [22]. Since interleaving composition generates a set of possible protocols it would be more accurate to express this property in terms of set membership rather than equality (for simplicity of the analogy, this elides the fact that each composition • is itself a set): In this section we consider two variants of this distributive behaviour for composition called (1) 'weak branching' and (2) 'interchange branching' which can be summarised via the algebraic analogy as variants of distributivity, respectively: In (weak), composition distributes inside one branch but not the other. In (interchange) 2 , composing branches with branches has a 'merging' effect on the branches rather than distributing within. We motivate and discuss each variation in term from the protocol perspective. In the rest of this section we introduce two additional composition rules: [wbra] for weak branching, and [cbra] for interchange branching (which we will refer to as correlating branching as it better reflects the effects of the rule on the protocols). Note that these two variations grow the set of possible interleavings, rather than shrinking it: they provide more general composition behaviours but do not exclude the more specialised behaviours. For generality of the theory, the derivation of interleaving composition can apply any branching ([bra], [wbra], [cbra]). For practicality, our tool allows engineers to choose the kind of branching to use in any specific scenario (as shown in Section 5).
Weak branching Weak branching allows for partial execution of some of the protocols being composed if there are not sufficient assertions to continue, as long as all protocols are completely executed in some execution path.
Example 3 (Branching with "asymmetric" guarantees). Protocol S B below needs assertion n to proceed. Assume we want to compose S B with a protocol S A , which can provide n in only one of its branches ok. S A may be an authentication server, granting or blocking access to S B depending on a password pwd: S A ::= ?pwd. ⊕ {ok : assert(n). end, ko : end} S B ::= require(n).S ′ for some S ′ . Since we want the actions of S B not to be executed after selection of label ko, we want interleaving composition to generate the following protocol: S AB = ?pwd. ⊕ {ok : assert(n).require(n).S ′ , ko : end} Interleaving composition S AB is not attainable using the rules of Definition 7: the derivation blocks when composing require(n).S ′ with the second branch's end in the empty environment. 3 Example 3 illustrates that asymmetric composition is a reasonable characterization of some scenarios. Definition 8 introduces a 'weak branching' composition rule [wbra] to allow for asymmetric guarantees.
Definition 8 (Weak branching). Weak branching composition of protocols is derived using the judgements in Definition 7 and the additional rule [wbra]: Precondition I A = ∅ ensures that each protocol's actions are executed in at least one execution path, and is key to the fairness property introduced in Section 4.1.
Hereafter we denote with ⊢ s derivations obtained using the judgements in Definition 7 only, and ⊢ w for derivations with the additional rule [wbra].
Example 4 (Weak interleaving composition of banking and PIN/TAN). Consider the banking and PIN/TAN protocols in Example 1. Interleaving composition of S A and S B using ⊢ s returns an empty set. When using ⊢ w , instead, we can derive the following interleaving composition modelling a banking/authentication protocol that satisfies the requirements specified in Section 1. Correlating branching Correlating branching allows two protocols to be composed by 'correlating' each branch of one with at least one branch of the other.
Definition 9 (Correlating branching). The correlating branching composition of two protocols is derived using the judgement in Definition 7 with the addition of rule [cbra] below: The first premise requires that: (1) each branch of the first protocol can be correlated with at least one branch of the second protocol (J i = ∅), and (2) each branch of the second protocol can be correlated with at least one branch of the first protocol ( i∈I J i = J). This precondition is critical to ensure the fairness property we introduce in Section 4.1. Rule [cbra] allows us to obtain S 12 as the interleaving composition of S 1 and S 2 above, modelling the intended correlation.
Hereafter we denote with ⊢ c (resp. ⊢ wc ) derivations obtained using the judgments in Definition 9 with the addition of rule [cbra] (resp. [cbra] and [wbra]). The inclusion relation between the different kinds of judgment is shown of the right (with ⊢ s and ⊢ wc being the most and less strict, respectively).

Properties of interleaving composition
In this section, we give the main properties of interleaving compositions. First, we give some general properties of well-assertedness and algebraic/scoping properties (i.e., sanity checks). Then, in Section 4.1 we give behaviour preservation and fairness, both formulated using a semantics of 'protocol ensembles' (a semantic counterpart of syntactic composition). Hereafter, we will denote with ⊢ any kind of judgment in {⊢ s , ⊢ w , ⊢ c , ⊢ wc }.
Well-assertedness of compositions Critical for the validity of our approach is that interleaving compositions preserve the constraints of assertions: Appendix D details the proof. A corollary of Proposition 3 and Lemma 3 (progress of very-well-asserted protocols) is that interleaving compositions enjoy progress: Algebraic and scoping properties Protocols may contain recursion variables, thus we consider notions of open and closed protocol with respect to recursion variables. Observe that, when composing two closed recursive protocols we only obtain closed protocols. This property is a corollary of a more general property, that free variables are preserved by interleaving composition: That is, the free variable set of a composed protocol is exactly the union of the free variables of the protocols being composed. Hence, composing protocols with no free variables necessarily obtains a closed protocol: Corollary 2 (Composition preserves closedness) For all A, S and closed protocols S 1 , S 2 , if T L , T R , A, S 1 • S 2 ⊢ S then S is a closed protocol.
A useful algebraic property is that composition has end protocols as units: Proposition 5 (Interleaving composition has left-and right-units) Appendix E details the proofs of the above results.

Behaviour preservation and fairness of protocol ensembles
To formalise a notion of behaviour preservation for interleaving composition, we first define an intermediate notion of protocol ensembles.
Protocol ensembles In Section 3, we gave a syntactic definition of interleaving composition. Interleaving composition makes the dependencies between protocols explicit, and provides a blue-print of an implementation. In this section, we consider 'protocol ensembles', which can be understood as the semantic compositions of two asserted protocols. Semantic compositions have a behaviour that is similar to parallel composition (e.g., as in CCS), but unlike parallel composition the two asserted protocols cannot communicate with each other, i.e., there are no internal τ actions. All interactions in a semantic composition are directed towards other endpoints (i.e., communication co-parties). Semantic composition provides a more general and somewhat familiar notion of composition, which we will use as a reference to analyze the properties of interleaving compositions.
Protocol ensembles, ranged over by C, are defined as follows: By defining protocol ensembles C as either asserted protocols (which may be compositions) or semantic compositions, we obtain a common LTS for comparing the behaviour of interleaving compositions and semantic compositions. For simplicity of presentation, we limit the theory to the composition S 1 || S 2 of two protocols S 1 and S 2 . The extension to n parallel protocols is straightforward although possibly verbose e.g., based on labelling each protocol, as well as its actions, with a unique identifier.
The LTS for protocol ensembles extends the LTS for asserted protocols: it is defined over states of the form (A, C), transition labels L (as for asserted protocols), and by the rules in Definition 3 plus the following two rules: Protocols in C do not communicate internally, but they may affect each other by adding, checking, or removing assertions in A.
Behaviour preservation Fix an LTS for protocol ensembles (Q, L, − →) defined on the set Q of states s of the form (A, C). We use the standard notion of simulation [30] to compare protocols of interleaving compositions and protocol ensembles, using protocol ensembles as a correct general model to which interleaving compositions need to adhere.
We call 'similarity' the largest simulation relation. We write s 1 s 2 when there exists R such that s 1 Rs 2 .
Definition 11 (Behaviour preservation). We say that C 1 preserves the be- Theorem 1 (Behaviour preservation of compositions -closed).
Therefore, interleaving compositions will only show behaviour that would be allowed by a protocol ensemble. Clearly, protocol ensembles allow more possible executions than an interleaving composition, which is only one of the possible interleavings. The proof of Theorem 1 is by induction on the derivation of S and, although the statement assumes closed protocols, some inductive hypotheses in the proof (e.g., premises of [rec1] or [rec2]) require reasoning about open protocols. The proof hence relies on a property (Lemma F6 -appendix) on open protocols: (roughly) given two protocols and one of their interleaving compositions, any action of the interleaving composition is matched by an action of the ensemble of the two protocols, and this property is preserved upon transition. Note that, while environments T L and T R are trivially empty in Theorem 1 (closed protocols), they have a key role in proving Lemma F6 (open protocols): they include the variables of each component protocol that are "morally" bound in a derivation, and give critical information of the scope and structure of the original component protocols in that derivation. The proof focusses on proving ⊢ wc which is the most general case; the other cases can be obtained by omitting the cases for rules not used by that kind of composition (e.g., for ⊢ s omit the [wbra] and [cbra] case). Appendix F details the full proof.
Fairness The fairness enjoyed by interleaving compositions depends on the set of composition rules used to derive that composition.
Given the ensemble of two protocols S 0 || S 1 , and any of their interleaving compositions S, each action of S 0 • S 1 (and hence of any one of the two protocols S 0 and S 1 being composed) can be observed in at least one execution of the interleaving composition S, possibly after a finite sequence of other actions by the other protocol being composed. For readability, in the following definition we will write ( , S) to denote (A, S) when A is not relevant to the definition.
One key characteristic of fairness in Definition 12 is that first we fix ℓ, and then we require at least one execution in which ℓ is eventually executed by S. This implies that although not all possible future branches include all parts of the protocols being composed, some will. This is illustrated for ⊢ c in Example 6, and for ⊢ w later in the section in Example 7.
Example 6 (Fairness and correlating branching). We illustrate fairness on S 1 , S 2 , and their interleaving composition S 12 with correlating branching given in Example 5. If S 1 makes a transition, then it is trivial to show that S 12 is a fair composition by taking r as the empty vector. The interesting case is the one where S 2 makes a step, picking one of the two possible labels. Assume S 2 transitions with ⊕ p1. Given ℓ = ⊕ p1, there exists r = ⊕ s1, assert(1) such The case for ⊕ p2 is similar.
In Theorem 3 we give a stronger fairness result for compositions using only [bra] (i.e., holding only for ⊢ s judgments). Each action of the protocol ensemble S 0 • S 1 (and hence of one of the protocols in the ensemble) can be observed in any execution of the interleaving composition, possibly after a finite sequence of other actions by the other protocol in the ensemble composed.
By Definition 13 any action of a composition can be matched by an action of the protocols being composed, and this property is preserved by transition. Vectors r, r ′ , and r ′′ are used to universally quantify on r and yet allow for the cases where ℓ comes before (1) or after (2) r in the composition.
Theorem 3 (Strong fairness of compositions with ⊢ s ). Assume ∅, ∅, A, S 0 • S 1 ⊢ s S then S is strongly fair with respect to S 0 and S 1 on A.
Appendix G details the proofs.
Example 7 (Fairness and weak branching). Consider a simpler variant of the protocols in Example 3 (omitting password exchange and continuation): We show that S AB is a fair composition w.r.t. S A and S B on ∅, but it is not a strongly fair one.
First focus on fairness. S A can move with either label ⊕ ok or ⊕ ko. In either cases (∅, S AB ) can immediately make a corresponding step with r empty. If S B moves, that is by label require(n), then for some environment {n}: There exists a sequence of transitions with labels r = ⊕ ok, assert(n) such that and ∅, ∅, ∅, end • end ⊢ w end. In the case above, we could select a 'good' path of S A and S AB that allows the transition with label require(n) to happen. Focus now on strong fairness and again, consider the step in Equation (1) by S B . Now we can pick an arbitrary r, say, ⊕ ok, such that (∅, Looking at S AB , there is no prefix nor extension of r = ⊕ ok that allows a require(n) step by S AB once the branch ko is taken. Therefore, S AB is not strongly fair with respect to S A and S B on ∅.

Implementation
We have implemented our approach as a tool for Erlang that offers functionality for protocol composition, code generation, and protocol extraction.
Interleaving composition. Interleaving composition is defined as a function producing 0 or more possible protocol compositions, giving an algorithmic implementation of the relation in Definition 7. Following the variations on the branching rule, the tool offers strong, weak, correlating, and weak/correlating compositions. The user can select the kind of branching to use. Looking at the running Example 1, we can give as input the banking and authentication protocols, and opt for strong composition, which returns an empty set as expected. When opting for weak composition instead, the tool outputs two possible interleaving compositions, from which the user can choose the desired protocol. The banking and authentication protocols are composed into a single protocol where the actions of the two protocols follow a specific interleaving dictated by the assertions. The resulting interleaving composition, equivalent to example 4, is:  way to reduce the number of returned (irrelevant) compositions is to introduce more relevant assertions. In fact, one of the aims of the tool is to support step-wise understanding of the protocol via progressive insertion of assertions.
For the main examples, presented in this paper, by selecting the most appropriate kind of composition and most appropriate assertions, the tool returns at most two interleaving compositions; this mostly happens when composing two recursive protocols as [sym] allows the recursion variable of each component to be used to denote the interleaved recursion. Table 1 shows the number of interleaving compositions obtained for each variation of the branching rule for a suite of examples used in this paper or from literature. For additional details and examples, see our repository with the complete benchmark (https://anonymous.4open.science/r/protocol-reengineering-implementation-2DC5/).
For most examples, with appropriate assertions, the tool returns a small number of compositions. Thus, it is not hard for the user to assess and choose the most suitable for their domain. However, if for instance, several branches of a protocol offer the same assertion, when composed with another with that particular requirement, the number of compositions will be higher. Code generation. Code generation takes a protocol definition and produces an Erlang stub. Protocol structures (action, sequence, choice) can be represented as a directed graph and then as finite state machines that transition based on the messages received. The finite state machines are used to generate a stub that uses the Erlang/OTP gen_statem [1], a generic abstraction which supports the implementation of finite state machine modules. Not only is it convenient to represent the protocol as a state machine, but gen_statem offers some useful features. Internal events from the state machine to itself are a good way of representing branches that make a selection among some choices. Co-located callback code for each state enables the use of non-atomic states, e.g., complex states or even hierarchical states. 'Postponing events' and timeouts provide functionality for further implementation of the generate code stubs.
Action and branch are represented as events that trigger a state transition. We use function declarations to represent incoming events, and function appli-cations to represent outgoing events. Each state has its own handler function used to send an event to the state machine. When the event is received the corresponding state function is called and the transition to the next state is made. The default generated event is an asynchronous communication (called a 'cast' in Erlang/OTP parlance). For sending actions and selecting branches, the event type is internal, an event from your state machine to itself. End is represented by the terminate function of a gen_statem module, whilst the fixed-point and the recursive variables dictate the control flow of the state machine. State variables must be declared by including them in a record definition -Data.
Following the example of [13], we represent assertions as specially formatted comments. For example: {assert, pay} is represented as an Erlang comment %assert pay. These comments are positioned before code that implements the state to which this assertion acts as a pre-condition in the protocol.
Below is an excerpt of the code generated for the PIN/TAN Banking protocol, bank_pt(), showing the states generated for the first action and branch: Protocol extraction and migration. Protocol extraction generates protocols from code via a static analysis of Erlang modules implemented as state machines using either gen_statem, or gen_fsm behaviour. When assertions are expressed using the comments illustrated above, they are also extracted. The obtained protocol can be annotated with extra assertions as necessary and composed with another to obtain a more complex protocol. The extraction option preserves preexisting local code that can be automatically migrated when generating a new stub. For example, starting out from an existing implementations of banking, we can use the tool to extract the protocol S B (in this case manual introduction of assertions may be needed), obtain an interleaving composition with S A , and generate a new implementation where pre-existing code for the banking code can be migrated.
If we wanted to re-engineer the banking/authentication server to include an option for keycard authentication (in addition to TAN authentication) we could further compose the PIN/TAN Banking Protocol with a keycard option protocol as the one below. Assertions ensure that the branching for choosing TAN or keycard authentication is plugged in (using assertion keyp) to the payment option of the PIN/TAN protocol, and that TAN authentication in PIN/TAN protocol is plugged only in the tan branch of the keycard protocol (using assertion otp): By adding an assertion of keyp and a consume otp at the beginning of the branch payment of the PIN/TAN Protocol one would obtain the desired extension as interleaving composition, using the weak composition option. The tool can be used to generate a stub for the extended protocol and migrate reusable code from the implementation of the PIN/TAN Banking Protocol to the new implementation. Together these features satisfy the requirements laid out in Section 1, facilitating program re-engineering. We can obtain skeleton implementations for banking and PIN/TAN protocol, extract the protocol and reuse the code when composing with a different protocol.

Instantiation to known protocol languages
Our protocol language (Section 2) is parametric on the set of action/branching prefixes and branching labels and our results hold regardless of the specific instantiation used. Instantiation allows us to apply our framework to different scenarios. Many of the examples in this paper are in the context of concurrency or distribution, yet protocols are pervasive in monolithic sequential code, e.g., for interacting with an operating system or libraries. A classic example is the stateful protocol of file handling in which files must be opened and closed, and only read and written to according to their permissions between those two actions. Our protocol language can easily model such situations, with interleaving composition providing a range of choices to a developer about how to combine and interact multiple stateful protocols.
In this section we provide a more concrete discussion of a few use cases focussing on interaction and communication, providing hints at possible synergies between our framework and techniques already studied for specific formalisms.

Protocols for communicating processes
Interaction structures of a communicating process can be characterised using process calculi such as CCS [27]. For example, a CCS process S = com.S + out.0 can be understood as a protocol prescribing the interactions supported by a server: repeatedly receive commands (com is a receive action) or decide to logout (out is a send action) and terminate. The CCS notation can be expressed in our protocol language by instantiating where a (resp. a) models a receive (resp. send) action on channel a, and Names is a set of channel names. Hence, S above can be represented in our framework as the process below µt. + {com : t, out : end}. In many examples in this paper we used the following instantiation: where T is a set of datatypes for messages. The above instantiation yields a session types-like syntax in the style of [14]. Session types [18,33,19] represent types of sessions through communication channels, describing the type of data that can be sent or received on a channel (e.g., !T and ?T where T is a datatype) and the patterns of message exchanges (e.g., sequential composition, recursion). This syntax is more restrictive than CCS (e.g., it is not possible to model mixed choices as in the CCS process above, where S is in a state in which it can either receive or send a message). The syntactic restrictions of session types contribute to their effectiveness for verification.

Protocols as session types
As mentioned in Remark 1 we often used a session types-like syntax in our examples. In this section we show how to use our framework in combination with session types techniques.
Recall, in Example 4, we have used interleaving composition to generate a banking/authentication protocol S BA using a session types-like syntax, and in Section 5 we have shown that our tool can generate a stub implementation of S BA , which one can then extend with local (i.e., non communication-related) behaviour. Assume this implementation, say bank pt.erl, is published as a web API. S BA can be published as a behavioural API.
So far, our framework has provided assurances on the relationship between component protocols and their interleaving composition (which pertains to the engineering within one node in a distributed system -in this case the banking/authentication server). Session types serve an orthogonal purpose: to provide assurances about the inter-relations of the protocols implemented in different nodes, e.g., given a well-defined banking/authentication server, how to derive a suitable client?
Anyone willing to develop a client for the banking/authentication service can use S BA to algorithmically derive a client protocol by using the notion of duality of Session Types [18,33,19]. The dual of a protocol is obtained alghorytmically, by swapping the 'direction' of each action and branching: ! with ?, ⊕ with &, and vice-versa. We let S BA denote the dual of S BA . Our tool can be used again to generate a stub for S BA (e.g., file co bank pt.erl). Session types duality and communication structuring (e.g., determinism, no mixed choices) yields a safe distributed system, resulting from, say, the concurrent and possibly distributed execution of bank pt.erl and co bank pt.erl. In this context, safe means no deadlock and no communication mismatches even when communications are asynchronous [12] as in Erlang.

Related Work and Conclusion
There is a vast literature on protocol specification (both theory and practice, e.g. [25]). Most techniques provide a monolithic, closed view of a system: a protocol is given for the entire system and all components are assumed to be present. We instead studied composition in open, general terms, defining composition as the interleaving of protocols, using 'assertions' to specify contact points and constraints between the protocols. We have given correctness in terms of behaviour preservation, fairness and well-assertedness, and shown that all compositions enjoy it. There are three main lines of research that relate to our work.
Firstly, software adaptors give typed protocol interfaces between software components [34]. The idea is similar to the structured view of communication in session types [19], with the notion of duality capturing when opposite sides of a protocol are compatible. Composition in these works is really about parallel composition along a protocol interface, guaranteeing sound communication. Instead, we study a sequential interleaving composition of protocols from the perspective of a single party (the common situation of engineering a single component of a larger system). Our assertions provide a kind of compatibility, but at the level of the protocol's (possibly interacting) application logics.
Secondly, composition has been studied as the run-time 'weaving' of component actions. Barbanera et al. study such a composition in the setting of asynchronous FIFO communicating finite state machines, while guaranteeing lock freedom [2,3]. Participants in two communicating systems can be transformed into coupled 'gateways', forming a composite system. Messages sent to one of the gateways are forwarded to the other, which in turn sends it to the other system. A compatibility relation is based on dual behaviour of the two gateways. Safety of the resulting system is by this compatibility, along with conditions of 'no mixed states' and determinism for sends and receives. Building from this idea, later work looks at composition in a setting of synchronous CFSMs, and replaces the two coupled gateways with a single one [5].
[4] look at direct composition and decomposition on global types in the setting of multiparty session types. Inspired by aspect-oriented programming, [32] support protocol extensions with 'aspectual' session types, that allow messages in session types to be matched and consequently introduce new behaviour in addition to, or in place of, the matched messages.
[29] look at composition in the setting of choreographies. Composition relies on the use of partial choreographies, which can mix global descriptions with communication among external peers. Unlike the above approaches, we focus on a syntactic, statically derivable notion of composition. Concretely, we use process calculi to model protocols as simple syntactic objects that can be used to reason about the desired application logic and generate/engineer modular code. Again, we differ in that our protocols are understood as being enacted by a single process (within a larger system).
The third pertinent thread in the literature defines syntactic compositions in the form of Team Automata [16,7,6] or related calculi [7]. These works define different ways of composing machines, primarily based on synchronising machines via common actions. They consider a general framework that is parametric in choices about synchronisation in an n-party context. In contrast, our means of composition is via assertions (orthogonal to actions) which express directional (i.e., rely-guarantee-style) dependencies. Our use of assertions aims to reflect programming practice. Assertions are also kept in our generated code and can be used to enable protocol extraction and re-engineering (as well as understanding and code documentation). Thus we focus on protocol compositions that are sensitive to the application logic of the protocols being composed. Our composition cannot capture the whole range of synchronizations offered by Team Automata. Conversely, Team Automata cannot capture the range of compositions possible in our approach. One can encode some interleaving compositions as Team Automata, by modelling each assert(n)-require(n) or assert(n)-consume(n) pair as a common synchronization action. However, the options offered by Team Automata (e.g., 'free', 'state indispensable', or 'action indispensable') do not capture our requirement that synchronization (i) always happens on assertionactions and (ii) never happens on communication actions (these are a separate syntactic entity). Furthermore, our assertions do not imply immediate synchronisation: an assert(n) can occur in a protocol some way before a require(n). Thus an attempted encoding of Team Automata into our protocols, encoding synchronization actions as unique assert(n)-consume(n) pairs, would not preserve the behaviour of Team Automata for all possible compositions (just the ones where such 'annihilating' pairs appeared contiguously). Thus, Team Automata and our approach overlap in some synchronising behaviours, but not all. A formal study of the class of overlapping compositions between our approach and Team Automata is further work.
Unlike applications of team automata for safe communication [6], and other works discussed above, we do not focus on safe communications as such, which is an orthogonal concern for us. Our focus is on correct representation of the application logic via a notion of composition steered by assertions. However, the specific session-type-like notation we use, following [14], would allow us to inherit communication-safety properties from session types, even with asynchronous communications [12] and multiparty sessions [9], as discussed in Section 6.2. We can model higher order messages by instantiating prefixes to incorporate the entire protocol language itself, preventing use of delegated channels using assertions.
Future work For the theory, we are currently working on a factorisation function that decomposes protocols, as a kind of algebraic inverse to composition. This would allow us to 'close the loop', factorizing (possibly extracted) protocols into simple components for later (re)composition. Interestingly, our weak composition still retains sufficient information (existential quantification on the branches in Definition 8) about the component protocols for them to be correctly factorized. We also plan to extend recursion to model quantified recursion and assertion environments as multisets (e.g., to quantify on rely and guarantees).

A.2 Interleaving Composition and Multiparty Session Types
Consider a protocol, modelled using the session types syntax, that specifies the possible interactions between a user U and a remote instrument I (e.g., a camera). Below, S I is the protocol specified from the perspective of I, which offers a menu with two choices: set or get. In case of set, I receives coordinates to update its own state, and in case of get, I sends a picture from the current coordinates. Protocol S U is the dual of S I (i.e., specified from the perspective of U ). The protocols above may have been designed top-down or extracted using our tool out of an existing system. Assume we need to modify the scenario above by introducing a proxy agent A, so that U and I will only interact via A. We need to: (1) express the protocols so that it is clear which roles are involved in each interaction, and (2) define the protocol for A. We address (1) by using a different instantiation of the protocol language to make roles explicit. For example, by fixing a set Roles of protocol roles, a set T of datatypes, and letting Then we obtain protocols in a multiparty session types syntax (e.g., local types in [9]), where ab! (resp. ab?) denotes a send action by a (resp. receive action by b) in an asynchronous interaction from a to b. Similarly for branching and selection. This instantiation allows us to model the following multiparty versions of S I and S U , respectively: We would like A to act as a server for U and as a client for I. Concretely, we could generate the protocol for A as a specific 'forwarding' interleaving of the dual of S AI and the dual of S UA . We use assertions to ensure that A sends I a menu choice only after having received one from U (and this must be the same choice received by U ), and then A must reflect the behaviour of I following the given choice. The asserted protocols to be composed into the protocol for A are given below, where assert(set)/consume(set) and assert(get)/consume(get) express the desired correlation between branches, and assert(f )/consume(f ) model the forwarding pattern: Using interleaving composition with correlating branching (Section 3.1) on the two protocols above we obtain the following interleaving composition specifying the protocol for A, where we omit the assertions for readability: Now that we have the protocols of the extended multiparty system we can use our tool to generate code for S UAI , S AI , and S UA . Thanks to the extraction/migration functionality of our tool, pre-existing local code for U and I can be reused in the new code for U and I, where the specific endpoints for communication can be added manually. The tool does not yet support syntax for specifying roles, so in the case of an agent communicating with several parties such as S UAI the direction of the communication would need to be specified manually.
In the multiparty scenario, correctness of the interaction structures can be checked using multiparty compatibility [15] and verification techniques [26].

B Basic properties of protocols
We first define some additional results in this appendix which are used for some of the key lemmas of this section. We have the following set of inversion lemmas on well-assertedness: Proof. There is only one rule that provides the well-assertedness of prefixing: Proof. There is only one rule that provides the well-assertedness of branching: Given the antecedent of this lemma, we then have that {A i } i∈I = {B i } i∈I and A ′ = i∈I B i then the premise provides the consequent of the lemma, ∀i ∈ Proof. There is only one rule that provides the well-assertedness of assert: Proof. There is only one rule that provides the well-assertedness of require: Thus we have that A = B ∪ {n} and so n ∈ A and A ′ = B ′ thus the premise provides the consequent of this lemma.

Lemma B5 (Consume well-asserted inversion)
Proof. There is only one rule that provides the well-assertedness of consume: Thus let A = B ∪ {n} and A ′ = B ′ and therefore n ∈ A. The (first) premise of this rule then provides the consequent of this lemma.

Lemma B6 (Recursion well-asserted inversion)
Proof. There is only one rule that provides the well-assertedness of recursion: Thus we let A = B and A ′ = B ∪B ′ yielding (A ⊆ A ′ ) and then premise provides the consequent of this lemma.
By induction on each then we have A {S i [µt.e.+{l i : S i } i∈I /t]} A ′ i allowing us to re-derive branching well-assertedness: which equals our goal by the definition of syntactic substitution: t Such a protocol is not allowed by the syntactic guardness requirement, so this case is trivial (ex falso quodlibet).
By induction over the structure of S i . In each case, we proceed by induction, rebuilding well-assertedness (exactly as in the proof of Lemma B7). The key case is when we have a recursion variable that we are substituting into, t ′ .
t ′ ≡ t then we substitute here: t ′ [+{l i : µt.S i } i∈I /t] = +{l i : µt.S i } i∈I and so well-assertedness holds by the second conunct of the premise.
which yields our goal by the definition of syntactic substitution.
which by the definition of syntactic substitution yields the goal: By . which yields our goal by the definition of syntactic substitution.
Then we can apply construct wellassertedness by the derivation: • t = t ′ then t ′ [µt.t ′ /t] = t ′ therefore using the assumption we have Proof. By induction on the structure of A {S} A ′ .
Then the only possible reduction is Inter : Therefore we can conclude with the premise of A {S} A ′ which shows that S is well-asserted (and trivially A ⊇ A).
Then the only possible reduction is Branch : Therefore we can conclude with the premise A {S j } A j which shows that S j is well-asserted (and A j ⊇ i∈I A i since j ∈ I).
Then the only possible reduction is Require with: (note the trivial satisfaction of the side condition here). Therefore we can conclude with the premise A∪{n} {S} A ′ which shows that S is well-asserted (and trivially A ′ ⊇ A ′ ). We now proceed by an inner induction on the structure of S to prove that • (prefix) S = p.S 1 thus A {p.S 1 } A ∪ A ′ , and thus ( * ) must be the reduction: Then by the definition of substitution and lemma B1 (inversion of prefix well-assertedness) on (**) we get: and thus ( * ) must be the reduction: By lemma B9 on A {+{l i : S i } i∈I } A∪A ′ and unfolding the definition of syntactic substitution then A {+{l i : Then by the definition of substitution and lemma B2 (inversion of branch well-formendess) on (**) we get: Then taking i = j we get A {S j [µt. + {l i : S i } i∈I /t]} A j providing the goal of this lemma with A ′′′ = A j and A j ⊇ A ∪ A ′ = i∈I A i since j ∈ I. • (assert) S = assert(n).S 1 thus A {assert(n).S 1 } A ∪ A ′ , and thus ( * ) must be the reduction: Rec and thus A ′′ = A.
Then by the definition of substitution and lemma B4 (inversion of require well-assertedness) on (**) with n ∈ A we get: A {S 1 [µt.require(n).S 1 /t]} A∪A ′ matching the goal with A ′′′ = A∪A ′ . • (consume) S = consume(n).S 1 thus A {consume(n).S 1 } A∪A ′ , and thus ( * ) must be the reduction: Rec Then by the definition of substitution and lemma B5 (inversion of consume well-assertedness) on (**) with n ∈ A we get: and thus ( * ) must be the reduction: Rec and thus A ′′ = A 1 . By lemma B9 on A {µt 1 .S 1 } A ∪ A ′ then (unfolding substitution and since t = t 1 ) Then by the definition of substitution and lemma B6 (inversion of consume well-assertedness) on (**) with A ⊆ A ∪ A ′ by usual set theory laws, then we get: A recursive variable on its own cannot reduce thus this case holds trivially since the premise is false.
The terminated process end cannot reduce thus this case holds trivially since the premise is false.
Lemma 2 (Well-asserted protocols are not stuck). If A {S} and S is closed with respect to recursion variables (fv(S) = ∅) then (A, S) is not stuck.
Proof. We proceed by structural induction on the derivation of well-assertedness A {S} A ′ (and thus simultaneously on the structure of S since every syntactic construction has one well-assertedness rule): -S = end there are no further reductions possible and the thesis trivially holds: we conclude with the first conjunct of the definition 4. -S = t then progress is trivial since the premise is that the S is closed.
Thus S can reduce by Inter as (A, where A ′ = i∈I A i . Thus, S can reduce by Branch to (A, S j ) for any j ∈ I.
Thus S can reduce by Consume to (A\{n}, S ′ ) since well-assertedness gives us that n ∈ A. to give us the side condition of this reduction rule.
Thus S can reduce by Require to (A∪{n}, S ′ ) since well-assertedness gives us that n ∈ (A ∪ {n}) to give us the side condition of this reduction rule.
By induction on the first premise we get that S ′ = end or (A, S ′ ) → (A ′′′ , S ′′ ).
• In the case of S ′ = end then we have S = µt.end which by structural congruence (definition 2) then means S = end.
Below we write: Lemma 3 (Progress of very-well-asserted protocols). If S is very-wellasserted (i.e., ∅ {S}) and closed then it exhibits progress. In the latter case (of a reduction), we then apply lemma 1 to get that Then we have the assumption that (∅, S) → k+1 (A k+1 , S ′ k+1 ) and thus there exists (∅, S) → k (A k , S ′ k ) → (A k+1 , S ′ k+1 ). We can apply the lemma inductively on (∅, S) → k (A k , S ′ k ) (i.e., the n = k case) to get that S ′ k = end (not possible because of the k + 1 reduction here) By lemma 2 (local progress) with In the case of the left disjunct we are done. In the case of the right disjunct, we then have the remaining piece of evidence via lemma 1 (reduction preserves well-assertedness) Thus we are done.

D Proof of Proposition 3 on validity of composition
Proposition 3 (Validity) If T L , T R , ∅, S 1 • S 2 ⊢ S then S is very-well-asserted.
Proof. The proof is by induction on the derivation, proceeding by case analysis on the last rule (Definition 7) applied. Inductive cases. We show below the inductive cases.
-Case last rule is [act]. The conclusion is on the form By induction, from (Equation (18)) it follows: By applying rule [act] in Definition 6 to (Equation (19)) it follows A {p.S ′ } as required.
By induction, from (Equation (20)) it follows that A{S} as required. -Case last rule is [require]. The conclusion is on the form By induction, from (Equation (21) By induction, from (Equation (22)) it follows By applying (Equation (23)) as a premise for rule [consume] in Definition 6 obtain {n} ∪ A ′ {consume(n).S ′ } as required. -Case last rule is [assert]. The conclusion is on the form By induction, from (Equation (24)) it follows By applying rule [act] in Definition 6 to (Equation (19)) it follows A {assert(n).S ′ } as required.
-Case last rule is [bra] (without weakening). The conclusion is on the form By induction, from (Equation (26)) it follows: By applying (Equation (27)) as premise of [bra] in Definition 6 it follows A {+{l i : S ′ i } i∈I } as required. -Case last rule is [bra] (with weakening). The conclusion is on the form with premises I A ∪ I B = I, I A ∩ I B = ∅ and I A = ∅, and By induction, from (Equation (28)) it follows: By applying (Equation (29)) and (Equation (30)) as premise of [bra] in Definition 6 it follows A {+{l i : S ′ i } i∈IA ∪ +{l i : S i } i∈IB } as required. -Case last rule is [rec1]. The conclusion is of the form The thesis follows by condition A {µt 1 .S} in the premise (Equation (31)). -Case last rule is [rec2]. The conclusion is of the form The conclusion is of the form with premise A {µt 1 .S ′ 1 } which gives the thesis. Lemma E1 Assume T L , T R , A, S 1 • S 2 ⊢ S and t ∈ fn(S 1 ), then t ∈ fn(S 2 ) and t ∈ fv(S).
Proof. The proof is by induction on the derivation of S, proceeding by case analysis on the last rule used. Base case [end] holds since t ∈ fn(S 1 ). Base case [call] yields immediately t ∈ fn(S 2 ) and t ∈ fv(S). Base case [rec3] holds since fn(S 1 ) = ∅ (by condition in the premise). All other cases hold directly by induction.
Proof. By induction on T L , T R , R, S 1 • S 2 ⊢ S: S By induction and then that fv(p.S) = fv(S).
By induction and commutativity of ∪ on sets.
By induction and then fv(require(n).S) = fv(S) (recall free variables are with respect to recursion variables rather than assertion names). -(consume) By induction and then fv(consume(n).S) = fv(S).
Corollary 2 (Composition preserves closedness) For all A, S and closed protocols S 1 , S 2 , if T L , T R , A, S 1 • S 2 ⊢ S then S is a closed protocol.

Proposition 5 (Interleaving composition has left-and right-units)
Appendix E details the proofs of the above results.
Proof. We split the proposition into two parts. First proving the right unit, then the left unit.
For the right unit, we proceed by induction on the derivation of A {S}: Then by induction on S ′ we have that T L , T R , A, S ′ • end ⊢ S ′ and thus by (act) we get T L , By induction on the premise for each S i we get that T L , T R , A, S i • end ⊢ S i . Applying all these as the premises of (bra), we get that: Satisfying the goal.
Applying this to (require) for interleaving composition then gives us: Satisfying the goal.
Applying this to (consume) for interleaving composition (with the side condition of n ∈ A from the well-assertedness rule) then gives us: Applying this to (assert) for interleaving composition then gives us: If fv(µt.S) = ∅ then we apply (rec3) and obtain the thesis. If fv(µt.S) = ∅ the hypothesis does not hold hence done.
We can then conclude with our goal via the (end) rule of interleaving composition: In this case fv(S) = {t} = ∅ which contradicts the hypothesis hence done.
Thus we have proved the right unit property of interleaving composition: that for all S we have T L , T R , A, S • end ⊢ S.
To prove the left unit property we can then compose the above result with the (sym) rule of interleaving composition: giving the left-unit property. ⊓ ⊔

F Proof of behaviour preservation (Theorem 1)
We recall the theorem for convenience.
Proof. We use stratification of similarity, along the lines of [30] (Definition 2.2.10).

First note that:
-R1 is used to capture the initial scenario of two closed types producing an interleaving composition -R2 is used to handle the scenario where two recursive processes in R1 (one component and the composition) have a transition involving unfolding: -R4 is a simulation as it is a special case of R4 in Lemma F9 where S = S 1 , and models the case of weak branching.
We show that is two processes are in relation R1, upon transition they will 'stay' in R1 or go to states related by R2, R3, or R4, which are simulations. First assume that the two processes considered are in R1. Assume (A, S) ℓ − → (A ′ , S ′ ), we proceed by case analysis on the structure of S.
Case ℓ ∈ {⊕l, &l} By Lemma 6 (point 3) we have two cases. If the transition is matched by a transition of either S 1 or S 2 that preserves the composition derivation this case is identical to the case for ℓ ∈ {⊕l, &l}). If, instead, (A, S)
Proof sketch. The proof is by induction observing that no reduction rule adds free names.
Lemma F4 (Environment Unfolding) and and Proof. This lemma holds for all variants of composition: ⊢ s , ⊢ w , ⊢ c , and ⊢ wc (recall that notation ⊢ is used to refer to any of the aforementioned composition judgments). The proof focusses on proving ⊢ wc which is the most general case; the other cases can be obtained by simply omitting the inductive cases for rules not used by that kind of composition (e.g., for ⊢ s omit the [wbra] and [cbra] case). The proof by induction on the derivation of S by case analysis on the last rule used.
[rec1] -S 1 = µt.S ′ 1 and S = µt.S ′ . By hypothesis (showing the last rule application by [rec1]) By induction, considering the premise of eq. (37) Since T R ⊆ T ′ R and T ′ R = ∅ the above is equivalent to as required.
[rec2] -S 1 = µt.S ′ 1 By hypothesis (showing the last rule application by [rec2]) By induction By applying the above as a premise of [rec2] we obtain (41) Observe the following: T L ∪fn(S 1 ) = T L since fn(S 1 ) ∈ T L by hypothesis (1) and Lemma B (43) So The thesis is equivalent to hypothesis eq. (34) observing that as desired.
[consume] -S 1 = consume(n).S ′ 1 By hypothesis • S 2 ⊢ S By induction, considering the premise of the derivation above: by using the above as a premise of [consume] we obtain which is the thesis, observing that fn(consume(n).S ′ 1 ) = fn(S ′ 1 ) as desired.
[wbra] -S 1 = +{l i : S i } i∈I By hypothesis By induction: and by second premise of eq. (46) (48) By applying eq. (47) and eq. (48) as premise of [wbra] we obtain which by definition of substitution is equivalent to which is the thesis, observing that fn(+{l i : S i } i∈I ) = i∈I fn(S i ) as desired.
[bra] -S 1 = +{l i : S i } i∈I This case is a special case of [wbra] above with I B = ∅.
Fold(p.S, t) = p.Fold(S, t) Fold(assert(n).S 1 , t) = assert(n).Fold(S, t) Fold(consume(n).S 1 , t) = consume(n).Fold(S, t) Fold(require(n).S 1 , t) = require(n).Fold(S, t) Fold(+{li : S i } i∈I , t) = +{li : Proof. This lemma holds for all variants of composition: ⊢ s , ⊢ w , ⊢ c , and ⊢ wc (recall that notation ⊢ is used to refer to any of the aforementioned composition judgments). The proof focusses on proving ⊢ wc which is the most general case; the other cases can be obtained by simply omitting the inductive cases for rules not used by that kind of composition (e.g., for ⊢ s omit the [wbra] and [cbra] case).
By induction on the derivation of S by case analysis on last rule used.
[end] The hypothesis does not hold since (A, end) → hence done.
[call] The hypothesis does not hold since (A, t) → hence done.
[consume] -S = consume(n).S The top of the derivation is of the following form: The thesis (item 1) follows immediately by the premise of (eq. (49)) observing that Top(S 1 ) = ∅ and Top(S) = ∅ and @ is the empty substitution.
S = +{l i : S ′ i } i∈IA ∪ +{l i : S i } i∈IB can only move by Branch with ℓ = l j and either j ∈ I A or j ∈ I B .
The thesis hold (item 1) as it is the premise in (eq. (50)) for i = j ∈ I A observing that Top(+{l i : S ′ i } i∈I ) = ∅ and Top(+{l i : S i } i∈I ) = ∅ and @ is the empty substitution.

Cases [cbra] By hypothesis
S = +{l i : + ′ {l ′ j : S ij } i∈Ji } i∈I can only move by Branch with ℓ = l i as follows: (A, +{l i : The first premise in (eq. (50)) can be applied as axiom in the derivation below to obtain the thesis (item 1) and observing that Top(+{l i : S ′ i } i∈I ) = ∅ and @ is the empty substitution: The last rule applies is of the following form: . By induction one of the following holds: Case [rec1] -S = µt 1 .S and T R = ∅ By hypothesis and By induction, considering the premise of (eq. (52)) we have one of the following three cases: Case S 1 moves and composition is preserved. If (A, S 1 ) ℓ − → (A ′ , S ′ 1 ) and then by premise of (eq. (52)) Top(S 1 ) = ∅ hence @ is empty substitution and we get By rec , (A, µt 1 .S 1 ) . The thesis to prove is therefore Observing that Top(S 1 ) = t 1 , the derivation above is equivalent to that is T L , ∅, A ′ , S ′ 1 @ • S 2 ⊢ S ′ Observing that @ is the empty substitution since in Top(S 1 ) = t 1 and t 1 ∈ fn(S ′ ) the above follows immediately by eq. (54).
Case S 2 moves and composition is preserved. If (A, S 2 ) ℓ − → (A ′ , S ′ 2 ) and then by Lemma F5, Top(S) = ∅ and @ is empty. Therefore, the above is equivalent to The thesis is equivalent to eq. (55) since: Top(S) = t 1 , Fold(S ′ [µt 1 .S/t 1 ], t 1 ) = S ′ and @ is the empty substitution (as fn(S ′ ) = t 1 which is not a name in S 2 as we assume bound names of S 1 and S 2 to be disjoint.
Case ℓ ∈ {⊕l, &l} and composition is not preserved. By induction either S 1 or S 2 makes a transition with label ℓ. We show the case in which S 1 moves, as the case in which (A, with fn(S ′ ) \ fn(µt 1 .S) = t 1 and fn(S ′ 1 ) \ fn(µt 1 .S 1 ) = t 1 hence the thesis.
Case [rec2] -S = µt 1 .S and T R = T R ∪ {t} By hypothesis and We apply induction to the premise of eq. (56). By induction considering the premise of eq. (56) we have one of the following cases: 1. First, assume and Observe that by premise of eq. (56) Top(S 1 ) = ∅ hence Top(S 1 [t/t 1 ]) = ∅. It follows that @ is empty and eq. (59) is equivalent to By rec with premise eq. (58) ) By the transition above and Lemma F2 We need to prove In eq. (63), @ = [t/t 1 ] since t 1 ∈ Top(S 1 ) and t 1 ∈ fn(S) and t ∈ T R ∪ {t}, hence eq. (63) is equivalent to eq. (60). The thesis eq. (62) holds therefore by eq. (60). 2. Second, assume By induction on the premise of eq. (56) Top(S 2 ))@ ⊢ Fold(S ′ , Top(S)) (65) for some @. Applying eq. (65) as premise of [rec2] we obtain the thesis 3. Finally, assume ℓ ∈ {⊕l, &l}. By induction we have (A, S 1 ) The thesis hold for S = S ′ since fn(S ′ ) \ fn(S) = ∅, fn(S ′ 1 ) \ fn(µt 1 .S 1 ) = t 1 . Proof. This lemma holds for all variants of composition: ⊢ s , ⊢ w , ⊢ c , and ⊢ wc (recall that notation ⊢ is used to refer to any of the aforementioned composition judgments). The proof focusses on proving ⊢ wc which is the most general case; the other cases can be obtained by simply omitting the inductive cases for rules not used by that kind of composition (e.g., for ⊢ s omit the [wbra] and [cbra] case).
We proceed by induction on derivation of S proceeding by case analysis on the last rule used.

Case [sym]
The last rule applies is of the following form: By bra , picking i ∈ I A which is not empty by premise of the derivation above (A, +{l i : The thesis holds as it is identical to the the premise of the derivation above for j ∈ I A .

Case [cbra] By hypothesis
By bra , picking i ∈ I (A, +{l i : By applying [sym] to the second premise of eq. (66): By applying eq. (67) as premise of [bra] and then [sym] we obtain the thesis (1): Case [rec1] -S = µt 1 .S and T R = ∅ By hypothesis and By Lemma F6 we have one of the following three cases: and By premise of eq. (68) Top(S 1 ) = ∅ and by Lemma F5 Top(S) = ∅. Hence by eq. (70) we obtain, with @ being the empty substitution: By premise of eq. (68) [rec1] A{µt 1 .S} which looking at the well formedness rule [rec] can be written as for some A ′′ . By Lemma 1 eq. (72) and eq. (69) imply By Lemma F4 since eq. (68) and eq. (71) and eq. (73) we obtain and By Lemma F5, Top(S) = ∅ hence eq. (74) is equivalent to We proceed by inner induction on the syntax of S 2 .
Proof. (sketch) (S, S 1 ) ∈ R2. So S = S ′ [µt.S/t] and S 1 = S ′ 1 [µt.S 1 /t]. We proceed by induction on S ′ . All cases are immediate as any step of S ′ is matched by a step of S ′ 1 since S ′ S ′ 1 . Notice that the only case that would require care, S ′ = t is ruled out.
R3 is a simulation.
Proof. (sketch) We proceed by induction on S ′ . All cases (except the case S ′ = t) are immediate as any step of S ′ is matched by a step of S ′ 1 since S ′ S ′ 1 . If S ′ = t then S ′ → hence done.
R4 is a simulation.
Proof. (sketch) Straightforward by induction on the structure of S.

G Proofs of fairness
Definition 17. Define the following context: ]. Define the following functions: Proof. Proof. By induction on the syntax of C.
-Case C = [ · ] (and hence V(C) is the empty vector of labels). We show the case for S ′ = consume(n).S ′′ and hence clab(S) = {consume(n)}. By wellassertedness of S, which in this case last applies rule [consume], n ∈ A, then by semantic rule consume we have 3. ℓ ∈ clab(S ′ ) Proof. We proceed by induction on the proof of S, proceeding by case analysis of the last rule applied.

Case [cbra]
Fix ℓ ∈ clab(S 1 ). In this case S = +{l i : + ′ {l j : S ij } j∈Ji } i∈I , S 0 = +{l i : S i } i∈I and ∀i ∈ I J i = ∅ i∈I J i = J j ∈ J i . T L , T R , A, S i • S j ⊢ S ij ∀j ∈ J \ J i T L , T R , A, S i • S j ⊢ T L , T R , A, +{l i : S i } i∈I • + ′ {l j : S j } j∈J ⊢ +{l i : + ′ {l j : S ij } j∈Ji } i∈I By induction ∀i ∈ I there exist C i [ S i ] = S i and C ′ i [ S ij ] = S ij such that V(C i [ · ]) = V(C ′ i [ · ]) and ℓ ∈ clab(S ij ). Hence, forall l j ∈ clab(S 0 ) (which is non empty since I = ∅) there exist j ∈ J i , C 1 [ S i ] = +{l i : C i [ S ′ i ]}∪{l j : S j } j∈I\{j} and C[ S ij ] = +{l i : ) and still ℓ ∈ clab(S ij ).

Case [sym]
In this case Assume that [sym] is applied only once. If [sym] it is applied multiple (but finite) times subsequently, say n times, then if n is even the thesis is immediate by hypothesis, and if n is odd then the case is equivalent to the one where the rule is applied once. Lemma G7 is a stronger version of Lemma G6 where quantification over contexts is universal rather than existential, and holds only for strong composition (not for weak one).
Lemma G7 If T L , T R , A, C 0 [ S 0 ] • S 1 ⊢ s S and clab(S 1 ) = ∅, then either: The cases for consume, assert, and require are similar to the prefix case above.
In both case (1) and case (2) above, it remains to prove that For every transition r ∈ r, by Lemma 6 (1) the composition relation is preserved; this can be shown proceeding as in Lemma G8. The case for i = 1 is symmetric (proceeds similarly, thanks to symmetric rules of composition and transition of protocols ensembles).