Jay Thakkar

Aditya Kanade

Rajeev Alur

Transducer-based Algorithmic Verification of Retransmission Protocols over Noisy Channels

Unreliable communication channels are a practical reality. They add to the complexity of protocol design and verification. In this paper, we consider noisy channels which can corrupt messages. We present an approach to model and verify protocols which combine error detection and error control to provide reliable communication over noisy channels. We call these protocols retransmission protocols as they achieve reliable communication through repeated retransmissions of messages. These protocols typically use cyclic redundancy checks and sliding window protocols for error detection and control respectively. We propose models of these protocols as regular transducers operating on bit strings. Streaming string transducers provide a natural way of modeling these protocols and formalizing correctness requirements. The verification problem is posed as functional equivalence between the protocol transducer and the specification transducer. Functional equivalence checking is decidable for this class of transducers and this makes the transducer models amenable to algorithmic verification. We present case studies based on TinyOS serial communication and the HDLC retransmission protocol.

Introduction

Communication protocols play a foundational role in the design of distributed systems. Model checking approaches (e.g. [START_REF] Holzmann | The Model Checker SPIN[END_REF]) analyze protocols for concurrency bugs. The traditional approach here is to build a finite-state model which abstracts message contents. Whether the communication channels between distributed components of a protocol deliver messages correctly or not is modeled as a nondeterministic choice. In practice, the physical channels can give rise to multiple types of faults, including message corruption, loss, and reordering. The realworld protocols, that provide reliable communication over unreliable channels, examine message contents to determine validity and semantics of messages [START_REF] Tanenbaum | Computer Networks[END_REF]. An approach where message contents are abstracted by symbolic constants may capture semantics of such protocols only partially.

A common approach to ensure reliable communication is to combine error detection and error control mechanisms. The sender adds redundancy (checksum bits) to the messages which is used by the receiver to detect errors in the received messages. Upon receiving a corrupted message, the receiver requests the sender for retransmission of the message. We call protocols which follow this scheme as retransmission protocols for noisy channels. These protocols typically use cyclic redundancy checks (CRC) [START_REF] Peterson | Cyclic Codes for Error Detection[END_REF] and sliding window protocols [START_REF] Cerf | A Protocol for Packet Network Intercommunication[END_REF][START_REF] Stenning | A Data Transfer Protocol[END_REF] for error detection and control respectively. By a noisy channel, we mean a channel that can corrupt messages but not drop, re-order, or duplicate them. TinyOS serial communication [1], high-level data link control (HDLC) [START_REF]Data Communication -HDLC Procedures -Elements of Procedure[END_REF], and transmission control protocol (TCP) [2] are examples of widely used retransmission protocols over noisy channels.

The objective of this paper is to devise a technique to model and verify such protocols. We observe that, for accurate modeling of the protocols, we have to encode messages as sequences of bits that are exchanged over channels. (In Section 2, we show that a protocol model, in which messages are abstracted as symbolic constants, can deliver a wrong sequence of messages.) However, verification of finite-state machines communicating asynchronously over unbounded FIFO channels is known to be undecidable [START_REF] Brand | On Communicating Finite-State Machines[END_REF].

In this paper, we present an algorithmic technique for verification of retransmission protocols where messages, checksums, and acknowledgements are treated as bit strings. In our models, the message strings and the number of (re)transmission rounds can be unbounded. Our approach is based on the observation that the protocol components can be viewed as transductions over bit strings. As an example, consider a sender which gets a message M from its client. The sender transmits it and in return, gets an acknowledgement a from the receiver. The combined input to the sender can be modeled as a string M a where is the end-marker attached to the message. The semantics of the sender is that if a is 0 (a negative acknowledgement) then it should retransmit the message. This can be formalized as a transduction f defined as f (M 1) = M and f (M 0) = M M . We give such transducer-based semantics to protocol components (sender and receiver) and obtain the protocol model by sequential composition of its components. Our modeling approach thus differs from the modeling of protocol components as asynchronously communicating finite-state machines [START_REF] Brand | On Communicating Finite-State Machines[END_REF]. The correctness requirement here is that, in spite of message corruption, the receiver delivers only correct messages to its client and in the same order as the sender's client intended. We show that the specification can also be modeled as a transducer. The verification problem is then reduced to checking the functional equivalence of the protocol and the specification transducers.

In many cases, the transductions defined by the sender, the receiver, and the specification of retransmission protocols are regular. Regular transducers are closed under sequential composition [START_REF] Chytil | Serial composition of 2-way finite-state transducers and simple programs on strings[END_REF] and equivalence checking is decidable for them [START_REF] Gurari | The equivalence problem for deterministic two-way sequential transducers is decidable[END_REF]. This makes these transducer models amenable to algorithmic verification. Even though sequential transducers also enjoy similar properties, they are not expressive enough to model components of retransmission protocols. For example, they cannot model the sender transduction f .

In this work, we use deterministic streaming string transducers (SSTs) [START_REF] Alur | Expressiveness of streaming string transducers[END_REF][START_REF] Alur | Streaming Transducers for Algorithmic Verification of Single-pass List-processing Programs[END_REF] as finite-state descriptions of regular transductions. An SST is equipped with a finite set of string variables to store strings over the output alphabet. The output of an SST can be defined in terms of the string variables. As compared to equally expressive models of two-way transducers and MSO-definable transductions, SSTs provide a more natural way of modeling retransmission protocols. In particular, the buffers used by the sliding window protocols for storing messages for retransmission can be modeled directly as string variables of SSTs.

We have designed transducer models of TinyOS serial communication protocol and HDLC with different CRC polynomials and have implemented a prototype tool for their verification. The sliding window protocols are fairly complex and are challenging even for manual proofs [START_REF] Helmink | Proof-Checking a Data Link Protocol[END_REF][START_REF] Havelund | Experiments in Theorem Proving and Model Checking for Protocol Verification[END_REF]. Our approach proposes transducers for modeling only those aspects of these protocols that are relevant for reliable communication over noisy channels and gives an algorithmic verification technique. Some features of these protocols, such as timers and dynamic window sizes, are neither relevant nor amenable to our approach.

In Section 2, we motivate transducer models of retransmission protocols with an example. The modeling approach is presented in Section 3 and the verification algorithm is discussed in Section 4. Section 5 describes case studies. The related work is surveyed in Section 6. In Section 7, we sketch future work and conclude.

Motivating Example

Suppose we want to transmit two messages (bit strings) M 0 and M 1 over a noisy channel. Following the usual procedure of abstraction, let us denote them respectively by symbolic constants m 0 and m 1 . In this example, we use the stop-and-wait protocol for error control. In this protocol, the sender prepends one bit sequence numbers to messages. This defines the space of valid encodings as {0, 1} × {m 0 , m 1 }. Let ack 0 and ack 1 denote acknowledgements indicating that the receiver expects a message with sequence number 0 or 1 next.

Consider a simple model of a noisy channel depicted in Fig. 1(a)-1(b). The sender-to-receiver channel is called the forward channel and the opposite channel is called the backward channel. The forward channel may corrupt the sequence bit of the encoded message as shown in Fig. 1(a). The messages to the left of the arrows are the original messages and those on the right indicate their possible incarnations at the other end of the channel. A dashed arrow indicates message corruption. The backward channel may corrupt ack 0 to ack 1 and vice versa.

The noisy channel can give rise to a sequence of message corruptions inducing the receiver to deliver an incorrect sequence of messages to its client. Fig. 1(c) shows such an example. The strings with Gray background indicate contents of the sliding window buffers. The dashed arrows annotating message exchanges indicate corruptions. In the first message transfer, the receiver cannot detect that (1, m 0 ) is corrupt since (1, m 0 ) does belong to the space of valid messages. It nevertheless discards it, as it is awaiting a message with sequence number 0. As ack 1 belongs the space of valid acknowledgements, the sender too cannot detect corruption and transmits the next message. Even after corruption, (0, m 1 ) is accepted by the receiver since it has the expected sequence number. Overall, the sender believes that it has sent m 0 , m 1 but the receiver accepts m 1 , m 1 .

(0, m0) (1, m 1 ) (0, m 1 ) m1 m1 ack1 ack1 The problem with this protocol model is that it is unable to detect corruption. Our solution is to make the modeling more precise by treating messages, acknowledgements, and checksums as bit strings. We represent a message encoding as a triple (n, M, c) where n is the (fixed-length) bit encoding of a sequence number, M is a message string (of an arbitrary length), and c is the (fixed-length) checksum over strings n and M . It is possible to build finite-state protocol models by bounding the length of message strings. This could be useful for finding bugs quickly. We are however interested in verification of retransmission protocols without bounding the message length artificially.

(0, m0) (1, m0) (1, m1) (1, m1) (0, m1) (a
(1, m 1 ) m1 m1 ack0 ack0 Sender Receiver (0, M 0 , c 0 ) ER R (0,M0,c0) discarded (corrupt) (Ac k0, c2) (Ac k1, c2) discared (corrupt) (0, M 0 , c 0 ) (0,M0,c0) M0 (Ac k1, c3) Ack1 (1, M 1 , c 1 ) (1,M1,c1) M1 (Ac k0, c2) Ack0 (c) Incorrect communication (d) Correct communication
We propose a transducer-based model that does not exhibit the incorrect communication scenario discussed above. We view the input to the sender as a sequence of messages and acknowledgements (protected by checksum). Consider the following string of inputs to the sender according to our scenario:

M 0 (Ack 1 , c 2 ) (Ack 1 , c 3 ) M 1 (Ack 0 , c 2 )
The acknowledgement strings corresponding to ack 0 and ack 1 are denoted by Ack 0 and Ack 1 respectively. Let the checksum be an even parity bit with c 2 and c 3 as the correct checksums for strings Ack 0 and Ack 1 respectively.

Consider a sender transducer which scans the input string in a single leftto-right pass. Here, it reads the message string M 0 , generates an encoding (0, M 0 , c 0 ), and stores it in a string variable corresponding to the sliding window buffer. It then looks ahead at the acknowledgement to determine its output in the first round of transmission. It detects that (Ack 1 , c 2 ) is an invalid/corrupt acknowledgement string. It does not know whether the message was received correctly at the receiver or not. It conservatively assumes that it was not delivered correctly. The sender sets its output to some string, say ERR, with an incorrect checksum -modeling the effect of corruption to M 0 . Since (Ack 1 , c 3 ) is a valid encoding, the sender sets its output in the second round to (0, M 0 , c 0 ). Finally, it reads and encodes M 1 . The encoding of M 1 is appended to the output since (Ack 0 , c 2 ) indicates its correct delivery. The output string of the sender is thus:

ERR (0, M 0 , c 0 ) (1, M 1 , c 1 )
We depict the message exchanges according the input/output of the sender transducer in Fig. 1(d). It differs from the corresponding scenario in Fig. 1(c) in the output of the sender in the second round. The sender outputs (an encoding of) message M 0 instead of M 1 . Thus, this sender cannot be tricked into making an incorrect transition on receiving a corrupt acknowledgement. The receiver too can be modeled as a transducer. It takes the message triples, verifies the checksum, and accepts a message if the checksum agrees. In this example, it accepts the correct message strings M 0 and M 1 and in the same order as that used by the sender, in spite of corruptions of messages and acknowledgements.

Transducer Models of Retransmission Protocols

We use streaming string transducers for protocol modeling and start with a brief introduction to them before giving the transducer constructions.

Streaming String Transducers

A deterministic streaming string transducer (SST) [START_REF] Alur | Expressiveness of streaming string transducers[END_REF] makes a single left-to-right pass over an input string to produce an output string. It uses a finite set of string variables to store strings over the output alphabet. Upon reading an input symbol, it may move to a new state and update all the string variables using a parallel (simultaneous) copyless assignment where the right-hand side expressions are concatenations of string variables and output symbols. A parallel assignment is copyless if no string variable appears more than once in any of the right-hand side expressions. For example, let a be an output symbol and X = {x, y} be the set of variables. Then, [x = x.y, y = a] is a copyless assignment, whereas, [x = x.y, y = y] is not because y occurs twice on the right-hand side.

Formally, an SST is an 8-tuple (Q, Σ 1 , Σ 2 , X, F, δ, γ, q 0 ) machine, where Q is a finite set of states, Σ 1 and Σ 2 are finite sets of input and output symbols respectively, X is a finite set of string variables, F is a partial output function from

Q to (Σ 2 ∪ X) * with the constraint of copyless assignment, δ is a state transition function from (Q × Σ 1 ) to Q, γ is a variable update function from (Q × Σ 1 × X)
to (Σ 2 ∪ X) * using copyless assignments and q 0 ∈ Q is the initial state. The semantics of an SST is defined in terms of the summaries of a computation of the SST. Summaries are of the form (q, s) where q is a state and s is a valuation from X to Σ * 2 which represents the effect of a sequence of copyless assignments to the string variables. The second component can be extended to a valuation from (Σ 2 ∪ X) * to Σ * 2 . In the initial configuration (q 0 , s 0 ), s 0 maps each variable to the empty string. The transition function is defined by ψ((q, s), a) = (δ(q, a), s ) where for each variable x ∈ X, s (x) = s(γ(q, a, x)). For an input string w ∈ Σ * 1 , if ψ * ((q 0 , s 0 ), w) = (q, s), then if F (q) is defined, the output string is s(F (q)) otherwise it is undefined.

Example Let us consider the sender transduction f described in Section 1. This can be implemented by an SST using four states, Q = {p 0 , p 1 , p 2 , p 3 } where p 0 is

p 0 start p 1 p 2 p 3 0 → [x 1 = x 1 .0, x 2 = x 2 .0] 1 → [x 1 = x 1 .1, x 2 = x 2 .1] → x 1 = x 1 . x 2 = x 2 . 1 → x 1 = x 1 x 2 = 0 → x 1 = x 1 x 2 = x 2
Fig. 2. An SST for the sender transduction f described in Section 1 the initial state, as shown in Fig. 2. Here,

Σ 1 = Σ 2 = {0, 1, }.
A message, M is a string over {0, 1} and is the message end marker. The SST for this example requires two string variables, X = {x 1 , x 2 }, both of which store a copy of the input message M . On reading 0 (resp. 1) in p 0 , the SST remains in state p 0 and appends 0 (resp. 1) to both x 1 and x 2 . The state transitions and variable updates are shown in Fig. 2. On reading the end-marker in state p 0 , the SST moves to state p 1 and appends to both x 1 and x 2 . In state p 1 , there can be two input symbols, 0 (a negative acknowledgement) and 1 (a positive acknowledgement). Upon seeing 1, the SST moves from p 1 to p 2 and frees x 2 . The output function in state p 2 is defined to be x 1 , i.e., F (p 2 ) = x 1 . The contents of x 1 here is M . On reading 0, it goes from state p 1 to state p 3 whose output is x 1 .x 2 , i.e., F (p 3 ) = x 1 .x 2 . This holds the output string M M . The output function F is undefined for other states.

Construction of Sender and Receiver Transducers

We present the transducer constructions abstractly without fixing the window sizes and CRC polynomials. An SST for a specific protocol configuration can be obtained by fixing values of these parameters. Due to the space constraints, for the sliding window logic, we consider only the go-back-n protocol. It is easy to extend the construction to stop-and-wait and selective-repeat protocols.

Sender SST Let W be the size of the sliding window of the sender. The sender can store up to W outstanding messages in a set of buffers. As more than one message can be in transit, to distinguish between them, the sender associates a sequence number with each message. Let the set of sequence numbers that the sender can use be 0, . . . , N -1. As a noisy channel may corrupt a message, the sender attaches a checksum with each of its outstanding messages.

In our setting, a sender receives a sequence of strings over {msg, ack i , b ack} where msg is a bit string that is provided to the sender by its client for transmission, ack i acknowledges the outstanding messages up to sequence number i -1, and b ack is an acknowledgement string with incorrect checksum -modeling corruption in the backward channel. Each acknowledgement corresponds to a (re)transmission round. If the receiver sees a corrupt message, it drops it and resends ack i where i is one plus the sequence number of the last message received successfully. We call such repeated acknowledgements as retransmission requests. The corruptions in the forward channel are thus identified by presence of retransmission requests in the sender's input string. The sender treats a b ack as a retransmission request for all outstanding messages.

The behavior of a noisy channel, that is, message corruption, is modeled in the output function of the sender. The output of the sender is thus the sequence of messages that the receiver sees at its end of the noisy channel. It is a sequence of strings over {ERR, Emsg} where ERR is a string with incorrect checksum, modeling a corrupt message. A string Emsg is an encoded message consisting of concatenations of a sequence number n (represented by a bit string), the message msg being transmitted, and the checksum crc. We require some meta-symbols to separate the substrings of Emsg and to separate consecutive messages and acknowledgements. For brevity, we omit them in this discussion.

For an outstanding message msg with sequence number i, the sender must decide whether the receiver sees ERR or its valid encoding Emsg. The encoding Emsg is emitted only if the subsequent acknowledgement is ack j where j is the sequence number that follows i. Otherwise, ERR is emitted. Thus, the sender must look ahead at the suffix of the string to determine its output. Since there are only a finite number of acknowledgement strings, they form a regular language. Thus, the sender can determine its output with a regular look-ahead.

The output function concatenates the encoded messages and ERR strings. An encoded message is present in the output at most once, only when it is positively acknowledged. For every retransmission request for a message, the fixed string ERR is added to the output instead of the encoded message. Thus, the size of the output string is a constant multiple of the size of the input string. This ensures that the resulting transducer is regular.

Presently, we model the behavior of a noisy (forward) channel in the output of the sender. The channel can also be modeled independently as a deterministic SST. The sender can output an additional bit with a message to indicate whether it is to be delivered uncorrupted or not, based on the regular look-ahead at the acknowledgements. The channel SST could simply inspect this bit to determine its output.

Sliding Window Management

We model each buffer of the sender by a string variable. Let the set X of string variables of the sender SST be {x 0 , . . . , x W -1 }. We remember the sliding window configuration and the next unused sequence number S in the states of the SST. A sliding window configuration is a pair of numbers F and L representing the first and the last occupied buffers respectively. Fig. 3 shows a snapshot of the abstract model of the sender SST. As a convention, if a variable is unmodified, we do not show an assignment to it.

Given F , L, and S, it is straightforward to identify sequence numbers of the outstanding messages. If the sender receives ack i then the buffers containing the messages with sequence numbers up to i -1 are freed (by assigning to them). The pointer F is updated to reflect this as indicated in the transition t 3 in Fig. 3, where OM is the set of sequence numbers of the outstanding messages and R is the number of buffers that are to be freed. If ack S arrives then all outstanding messages are delivered. The sliding window becomes empty (F = 0, L = -1). The transition t 4 shows this behavior. If the sliding window is not full, then the SST may read a message msg. It computes encoding of msg augmented with the sequence number S and stores the encoded message in the next free buffer. The transition t 2 illustrates this. The function enc denotes a CRC computation. We discuss it later in this section. A bad acknowledgement b ack does not affect the state and variables of the SST as indicated by the transition t 1 .

s 1 s 2 s 3 s 4 t 2 : msg → [x (L+1)%W = enc(S, msg)] t 1 : b ack → [y = y.ERR] t 3 : ack i , i ∈ OM →       y = y.T 1 .ERR x F = . . x (F +R-1)%W =       t 4 : ack S →       y = y.T 2 x F = . . x L =      

Handling Retransmission Requests

The protocol runs in potentially unbounded number of (re)transmission rounds. We wish to define the output of the sender across all the rounds as a string. We accumulate the output in a string variable y. The updates to y on every type of acknowledgement are shown in Fig. 3. If ack S is received, all the outstanding messages are appended to y in the order of their sequence numbers. The string T 2 used in transition t 4 is defined in the caption of the figure. If ack i is received then the messages that are acknowledged positively are appended to y. For the messages that were transmitted but not received correctly, we append ERR to y, as shown in both t 1 and t 3 . The output of the sender SST is set to y for every state in which message/acknowledgement is read completely. In each of these transitions, a variable x k is used at most once on the right-hand side of variable update γ. It is either unmodified (not shown in the figure), or assigned to y and at the same time, is reset to . Thus, the resulting assignments conform to the copyless restriction of SSTs. It is easy to see that the sender SST is deterministic.

CRC Computation

We now explain the modeling of the CRC computation, denoted by enc function in transition t 2 . A CRC computation is parameterized with a generator polynomial p. If the degree of the polynomial is r, then it appends an r-bit checksum to the input string. We model all possible values of an r-bit checksum into states of the SST with the initial state corresponding to checksum of zero. We require only a single string variable x to store a copy of the input string. For a state q, representing a checksum value c, we define the output to be x.#.c where # is a separator. We construct the transitions of the SST in such a way that if the SST ends up in a state q after reading the input string w, then the checksum value c, represented by q, is the checksum of w under polynomial p. The logic for constructing the state transitions follows from the semantics of linear feedback shift register (LFSR) circuits used for implementing CRC computations [START_REF] Forouzan | Data Communications and Networking[END_REF]. For want of space, we omit the details here.

The sender needs to verify checksum of the acknowledgement strings to classify them into ack i or b ack. The construction of SST for CRC verification is similar to that of CRC computation except for the variable update γ. From an input string, only the bits corresponding to the message content are copied.

Receiver SST The output from the sender (contents of variable y) forms the input to the receiver. The input to the receiver is thus a sequence of strings over {ERR, Emsg}. The output of the receiver is a sequence of strings over {msg}. In the go-back-n logic, the receiver accepts messages only in order.

We observe that the output of the sender contains the valid encoding of a message exactly once in its output. That is, there is no message duplication. This is because whenever a variable x k is appended to y, it is also freed. Second, the messages are always transmitted in the same order as the order in which they are obtained from the client. Thus, there is no message reordering. These two observations simplify the design of the receiver SST. In particular, the receiver SST must only be able to distinguish between corrupt and correct messages.

The receiver SST therefore consists of only two string variables: a variable x to store the current message contents and a variable y to accumulate the output across all (re)transmission rounds. Upon receiving a message encoding, the message content msg is extracted and stored in x. If the CRC verifies then x is appended to y and freed. The output for any state of the SST is the variable y. Clearly, the receiver SST is deterministic.

Sequential Composition of Sender and Receiver Transducers

The sender and receiver SSTs represent distributed components of the protocol such that the output of the sender is the input to the receiver. These SSTs model the checksum computations, message and acknowledgement encodings, and the sliding window logic of a retransmission protocol. These are however internal details of the protocol. Our goal is to analyze the end-to-end input/output relation implemented by the protocol where the input is a sequence of strings over {msg, ack i , b ack} (same as the sender) and the output is a sequence of strings over {msg} (same as the receiver).

SSTs are known to be closed under sequential composition [START_REF] Alur | Expressiveness of streaming string transducers[END_REF]. Thus, the input/output relation implemented by the protocol can be represented as a protocol SST. Further, the protocol SST can be obtained algorithmically by the sequential composition of the sender and the receiver SSTs. Consider an SST S 2 to be composed with an SST S 1 . The number of string variables in the composed SST is 2.|X 2 |.|Q 2 |.|X 1 |, where Q 2 is the set of states in S 2 and X 1 , X 2 are the sets of string variables in S 1 , S 2 respectively. It is beyond the scope of this paper to discuss the algorithm for sequential composition. We refer the reader to [START_REF] Alur | Expressiveness of streaming string transducers[END_REF]. The sender and receiver SSTs are much simpler to define than the protocol SSTs. Thus, the approach of modeling them individually and then composing is easier than constructing the SST for a protocol directly.

Verification of Transducer Models

In our models, each acknowledgement b ack or ack i corresponds to a separate (re)transmission round. Since the input to the sender can contain an unbounded number of acknowledgement strings, the number of (re)transmission rounds encoded in our models is unbounded. The number of messages received by the sender from its client too is not bounded. Similarly, there is no bound on the length of an individual message msg. Even with these sources of unboundedness, the verification problem for our models is decidable. In this section, we present the specification mechanism and the verification approach.

Specification SST

The key property of a retransmission protocol is that the messages acknowledged by the receiver (across all rounds) are delivered to the receiver's client correctly and in the same order in which the client of the sender handed them to the sender. This property can be specified as an SST. Similar to the protocol SST, the input to the specification SST is a sequence of strings over {msg, ack i , b ack} and the output is a sequence of strings over {msg}. The specification SST does not encode sequence numbers and checksums. It also does not corrupt or retransmit messages. It mainly encodes the sliding window logic to interpret the acknowledgement strings and determine which strings are supposed to be delivered by the receiver to its client.

The specification SST has a similar set of states, transitions, string variables, and output function as the sender transducer. The main difference between the sender and the specification SSTs is in the variable update γ. We refer to Fig. 3 to describe the specification SST for the go-back-n protocol. The specification transducer stores a message msg as it is in a string variable along transition t 2 . It neither attaches a sequence number nor a checksum with it. Since the output of the specification SST is the output of the receiver (and not that of the sender), for transitions t 1 and t 3 , it does not append a corrupt message to the output string variable y. The transition t 4 remains unchanged.

Verification Approach

The verification problem is to check equivalence between the protocol and the specification SSTs. Both these transducers are deterministic. Thus, for every input string w, we want to check whether the output of the protocol and the specification SSTs are same. The equivalence checking problem for (deterministic) SSTs is decidable [START_REF] Alur | Streaming Transducers for Algorithmic Verification of Single-pass List-processing Programs[END_REF]. The input to the verification algorithm consists of the sender and receiver SSTs and the specification SST as shown in Fig. 4. As discussed in Section 3.3, the protocol SST is obtained by sequential composition of the sender and the receiver SSTs.

Equivalence Checking We briefly outline the steps involved in equivalence checking of two SSTs. To check whether two SSTs, say S 1 and S 2 , are equivalent, the equivalence checking algorithm generates a 1-counter automaton, M . The objective is for M to determine whether there is an input string w and a position p such that the output symbols of S 1 and S 2 on w differ at position p. This can be generalized to infer whether (1) there is an input string w such that the output is defined for only one of S 1 or S 2 , or (2) the outputs are defined but the lengths of the output strings differ. The automaton M non-deterministically simulates S 1 and S 2 in parallel. For each of them, it guesses the position p and uses its counter to check whether the guess matches between S 1 and S 2 . The complete details about the configurations of the states and transitions between them is available in [START_REF] Alur | Streaming Transducers for Algorithmic Verification of Single-pass List-processing Programs[END_REF]. A finite set, say F , of states of the automaton are identified such that if any state in F is 0-reachable in M , then the two transducers are not equivalent. Thus, the equivalence checking problem is reduced to checking 0-reachability in a 1-counter automaton. This problem is in Nlogspace. The number of states in M is linear in the number of states of S 1 and S 2 , and exponential in the number of string variables of S 1 and S 2 . Therefore, the SST equivalence problem is in Pspace.

Decidable Extensions Instead of emitting the error string ERR for corrupt messages, the sender may resend the messages themselves. In such a case, the receiver needs to eliminate duplicates. However, for the sender to be a regular transducer, the length of the output strings must be a constant times the length of the input strings. This requirement can be satisfied by considering only a bounded number of retransmissions and using different string variables for different rounds. Several protocols like Philips Bounded Retransmission Protocol (BRP) fall in this class of protocols [START_REF] Groote | A Bounded Retransmission Protocol for Large Data Packets[END_REF].

Another extension can be to model the effect of a noisy channel with nondeterminism using the non-deterministic SSTs (NSSTs). NSSTs are closed under sequential composition, but the equivalence problem for them is undecidable [START_REF] Alur | Nondeterministic Streaming String Transducers[END_REF]. However, there is a subclass of NSSTs, called functional NSSTs, whose equivalence checking problem is decidable. In the future, we plan to explore of nondeterministic and bounded versions of retransmission protocols.

Case Studies

We model two practical protocols as case studies:

1. TinyOS : TinyOS is an open source real-time operating system for wireless sensor networks. Serial communication is used for host-to-mote data transfer.

The SerialP [1] software module of TinyOS computes the checksum and uses the stop-and-wait protocol in the host-to-mote direction. 2. HDLC : HDLC [START_REF]Data Communication -HDLC Procedures -Elements of Procedure[END_REF] is a bit-oriented protocol, that operates at data link layer. The software implementation computes checksum and uses go-back-n. Table 1 summarizes the three protocol configurations that we model. For each protocol, we indicate the window size (W ) and the CRC polynomials used. Real-world implementations of these protocols may use polynomials of higher degree in the CRC computation. The table also shows the number of states (|Q|) and variables (|X|) required in our case studies for sender, receiver, specification and protocol SSTs. The protocol SSTs are derived by our implementation of the sequential composition algorithm.

Modeling As an example, we present the sender and the receiver SSTs for the first protocol configuration in Table 1 (see Fig. 5). We build these according to the constructions described in Section 3. In these SSTs, if a variable update for any string variable v is not mentioned, it means that v is not updated, that is v = v. We use certain meta-symbols as separators: $ to separate consecutive messages and acknowledgements, # to separate the message content from the checksum and + to indicate the start of a message. Here, ack 0 is encoded as 00, where the first 0 indicates the acknowledgement number and the second 0 indicates the checksum bit. Similarly, ack 1 is encoded as 11, whereas b ack ∈ {01, 10} is a bad acknowledgement. The sender uses two string variables: x to store an encoding of the input message, and y to hold the output string. States q 0 to q 3 store the encoding of the input message in x, that is, [x = enc(0, msg)]. States q 1 and q 2 track the checksum value. State q 0 represents the empty sliding window, whereas q 3 represents the full sliding window. In state q 3 , on receiving either ack 0 or b ack, the SST appends a fixed error message, ERR (string 0.#.1.$), to y. On receiving ack 1 , the SST appends x to y, frees x and moves to the initial state for sequence number 1. The output function maps states q 0 and q 3 to y, and is undefined for other states. The part of the SST modeling sequence number 1 is similar (omitted from Fig. 5(a)).

The receiver SST shown in Fig. 5(b) needs two string variables: x to store the current message contents, and y to store the output (sequence of correctly received messages). Starting in r 0 , the receiver SST first validates the sequence number but does not copy it. Then, the message content is extracted and stored in x, in states r 1 and r 2 . State r 3 represents the checksum value 0 and state r 4 represents the checksum value 1. Thus r 3 indicates that the received input message encoding is not corrupt. So, after receiving the end symbol $ in r 3 , x is appended to y, and x is freed. State r 4 says that the received message is corrupt, and leaves y unchanged on receiving $. The output function maps state r 0 to y, and is undefined for other states. Note that all the variable updates are copyless in both the SSTs.

Verification We have implemented a prototype tool in OCaml to perform sequential composition and equivalence checking. For equivalence checking, our tool constructs the 1-counter automaton and uses ARMC for reachability checking [START_REF] Podelski | ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement[END_REF]. The maximum time taken by sequential composition was 4s (for the HDLC protocol). Our implementation successfully verified both variants of TinyOS, but timed out on HDLC. The state space of 1-counter automata is exponential in the number of string variables. For HDLC, this proved to be a bottleneck. We aim to address scalability as part of the future work. One possibility is to explore minimization techniques for reducing the number of states and string variables of the protocol SST.

Related Work

The undecidability of verification problems for finite-state machines communicating asynchronously over unbounded perfect FIFO channels is shown in [START_REF] Brand | On Communicating Finite-State Machines[END_REF]. For some classes of systems and properties, decidability results are obtained in [START_REF] Finkel | Decidability of the termination problem for completely specified protocols[END_REF][START_REF] Sistla | Automatic Temporal Verification of Buffer Systems[END_REF]. For unbounded lossy FIFO channels, reachability, safety of system traces, and eventuality properties are decidable [START_REF] Abdulla | Verifying Programs with Unreliable Channels[END_REF]. The semantics of lossy channels is orthogonal to our notion of noisy channels. For example, the scenario in Section 2 is applicable to lossy channels as well. A lossy forward channel may sometimes deliver corrupt messages to the receiver (and at other times, drop them). If we model messages as symbolic constants then the receiver cannot detect corruption and would deliver an incorrect sequence of messages to its client. Further, unlike these approaches, our choice of formalism for protocol modeling is transducers rather than communicating finite-state machines.

Sliding window protocols, being both complex and heavily used, are popular targets of verification techniques. Several automated techniques handle them by abstracting message contents. The work in [START_REF] Abdulla | Symbolic Verification of Lossy Channel Systems: Application to the Bounded Retransmission Protocol[END_REF] uses a class of regular expressions to represent channel contents where each message comes from a finite alphabet. In contrast, in our work, a message is treated as a finite bit string. The finite-state models obtained by abstracting message contents (and other parameters) are also verified by model checking (see survey [START_REF] Babich | Formal Methods for Specification and Analysis of Communication Protocols[END_REF]). Protocols with a fixed number of retransmission rounds are verified algorithmically in both untimed and timed cases in [START_REF] D'argenio | The Bounded Retransmission Protocol must be on time! In TACAS[END_REF]. Our model does not impose bounds on the number of retransmission rounds. However, modeling timing constraints is beyond the scope of our method.

A number of deductive or semi-automated techniques have been developed for verification of sliding window protocols. The process-algebra framework LOTOS is used in [START_REF] Madelaine | Specification and Verification of a Sliding Window Protocol in LOTOS[END_REF], whereas, I/O automata are used with Coq theorem prover in [START_REF] Helmink | Proof-Checking a Data Link Protocol[END_REF]. Deductive theorem proving is used for reducing the complexity of protocol models and to obtain simpler abstractions suitable for algorithmic verification [START_REF] Havelund | Experiments in Theorem Proving and Model Checking for Protocol Verification[END_REF][START_REF] Smith | Verification of a Sliding Window Protocol Using IOA and MONA[END_REF]. Higher-order logic specifications of the protocols in the language of PVS are designed in [START_REF] Rusu | Verifying a Sliding Window Protocol using PVS[END_REF]. Colored petri net models are used in [START_REF] Billington | How Stop and Wait Protocols Can Fail over the Internet[END_REF] for modeling of stopand-wait protocols. In [START_REF] Chkliaev | Verification and Improvement of the Sliding Window Protocol[END_REF], timed state machines are used for modeling sliding window protocols. Process algebra is also used in [START_REF] Badban | Verification of a Sliding Window Protocol in µCRL and PVS[END_REF] to establish bi-similarity of these protocols with a queue.

The assumptions on reliability of channels vary across approaches. Similar to most of the above approaches, we consider non-duplicating FIFO channels. The approaches [START_REF] Smith | Verification of a Sliding Window Protocol Using IOA and MONA[END_REF][START_REF] Billington | How Stop and Wait Protocols Can Fail over the Internet[END_REF] permit channels to re-order messages, whereas, [START_REF] Madelaine | Specification and Verification of a Sliding Window Protocol in LOTOS[END_REF][START_REF] Chkliaev | Verification and Improvement of the Sliding Window Protocol[END_REF] permit both re-ordering and duplication. Most of the above approaches assume lossy channels and do not model message contents. Noisy channels are modeled in π-calculus through probabilistic semantics [START_REF] Ying | π-calculus with noisy channels[END_REF][START_REF] Cao | Reliability of Mobile Processes with Noisy Channels[END_REF]. A recent work [START_REF] Delzanno | Verification of Ad Hoc Networks with Node and Communication Failures[END_REF] investigates decidability of control state reachability for ad-hoc networks in the presence of different types of node and communication failures.

Finite-state transducers are used in regular model checking for representing transition relations of systems whose configurations can be modeled as words [START_REF] Kesten | Symbolic Model Checking with Rich Assertional Languages[END_REF][START_REF] Wolper | Verifying Systems with Infinite but Regular State Spaces[END_REF][START_REF] Bouajjani | Regular Model Checking[END_REF]. The set of reachable states of these systems are represented by finite automata. However, in this context, the termination of fix-point computation is not guaranteed and the verification problem is in general undecidable. In contrast, the verification problem for the transducer models of the protocols presented by us, posed as functional equivalence checking, is decidable. Recently, more expressive transducer models are being designed by researchers, leading to new approaches to verification. SSTs have been introduced for pre/post verification and equivalence checking of single-pass programs operating over lists [START_REF] Alur | Streaming Transducers for Algorithmic Verification of Single-pass List-processing Programs[END_REF]. Symbolic finite transducers are introduced to analyze web sanitization functions [START_REF] Veanes | Symbolic Finite State Transducers: Algorithms and Applications[END_REF].

Conclusions and Future Work

In this paper, we consider noisy communication channels that may corrupt messages. We show that for accurate modeling of the retransmission protocols, in the setting of noisy channels, the messages, checksums, and acknowledgements must be modeled at the bit-level. We propose streaming string transducers as a modeling framework for retransmission protocols. Even though the message lengths and retransmission rounds are unbounded, we present an algorithm to verify the protocol models. In future, we want to explore non-deterministic and bounded versions of the retransmission protocol models.

Fig. 1 .

 1 Fig. 1. A noisy channel model and scenarios of correct and incorrect communication

F

Fig. 3 .

 3 Fig. 3. A snapshot of the abstract model of the sender transducer where T1 = xF .x (F +1)%W . . . x (F +R-1)%W and T2 = xF .x (F +1)%W . . . xL

Fig. 4 .

 4 Fig. 4. Verification approach

Fig. 5 .

 5 Fig. 5. SSTs for the TinyOS SerialP protocol with CRC polynomial z + 1

Table 1 .

 1 Case studies

				Sender	Receiver	Protocol	Specification
		CRC
	Protocol polynomial W	|Q| |X| |Q| |X| |Q| |X| |Q|	|X|
	TinyOS	z + 1	1	12	2	5	2	38	11	10	2
	TinyOS	z 2 + 1	1	20	2	9	2	80	15	14	2
	HDLC	z + 1	2	83	3	7	2	153	24	72	3

Acknowledgements The first two authors were partially supported by Robert Bosch Centre for Cyber Physical Systems at the Indian Institute of Science.

q 0 start q 1 q 2 q 3 q 5 q 4 Sender for seq. no. 1


Massimo Bartoletti

Alceste Scalas
email: alceste.scalas@unica.it

Emilio Tuosto
email: emilio@mcs.le.ac.uk

Roberto Zunino
email: roberto.zunino@unitn.it

Honesty by Typing

We propose a type system for a calculus of contracting processes. Processes may stipulate contracts, and then either behave honestly, by keeping the promises made, or not. Type safety guarantees that a typeable process is honest -that is, the process abides by the contract it has stipulated in all possible contexts, even those containing dishonest adversaries.

Introduction

Most approaches to the formal specification of concurrent systems typically assume that components behave honestly, in that they always adhere to some agreed specification (e.g., a behavioural type), under the assumption that the static behaviour safely over-approximates the dynamic one. We argue that this assumption is unrealistic in scenarios where competition prevails against cooperation. Indeed, in a competitive scenario components may act selfishly, and diverge from the agreed specification.

We envision a contract-oriented computing paradigm [START_REF] Bartoletti | Contract-oriented computing in CO2[END_REF], for the design of distributed components which use contracts to discipline their interaction. In CO 2 [START_REF] Bartoletti | Contract-oriented computing in CO2[END_REF], a process may advertise contracts; a session is established processes advertising compliant contracts, similarly to other session-centric calculi. This session dictates the actions needed to realise their contracts to processes. A distinguished feature of CO 2 is that processes are not supposed to respect their contracts, nor are they bound to them by an enforcing mechanism.

More realistically, dishonest processes may avoid to perform some actions they have promised in their contracts. This may happen either intentionally, e.g. a malicious process trying to swindle the system, or unintentionally, e.g. because of some implementation bug (possibly exploited by some adversary). In both cases, the infrastructure can determine which process has caused the violation, and adequately punish it. A crucial problem is how to guarantee that a process will behave honestly, in all possible contexts. If such guarantee can be given, the process is protected both against unintentional bugs, and against (apparently honest) adversaries which try to make it sanctioned.

A negative result in [START_REF] Bartoletti | On the realizability of contracts in dishonest systems[END_REF] is that determining if a process is honest is an undecidable problem for a relevant class of contracts (introduced in [START_REF] Carpineti | A formal account of contracts for web services[END_REF], and refined in [START_REF] Castagna | A theory of contracts for web services[END_REF], for modelling WSDL and WSCL contracts). The problem is how to find a computable approximation of honesty, which implies the dynamic one.

Example. Let us consider an on-line store (participant A), which sells apples (a) and bottles of an expensive italian Brunello wine (b). Selling apples is quite easy: once an order is placed, A accepts it (with the feedback ok) and waits for a payment (pay) before shipping the goods (ship-a). However, if expensive bottles of Brunello are ordered, the store is entitled to either decline the order (by answering no), or accept it (and, as above, ship the item after the payment). Using external (+) and internal (⊕) choice, the store contract can be modelled as c = a.ok. pay.ship-a + b. no ⊕ ok.pay.ship-b External choice requires the other party to decide how to drive the contract evolution; in this case, the customer chooses between apples a and bottles b. Internal choice, instead, allows the advertising party to choose; in this case, the store selects either ok or no.

Intuitively, contract compliance hinges on the duality between internal and external choices. Hence, to sell its goods, the store needs to find an agreement with a participant advertising a contract compliant with its contract c, such as:

d = b . (ok.pay.ship-b + no)
A buyer B advertising d wants to buy Brunello: she promises to select b (dual of b in the store contract), and then offers an external choice that lets the store choose between ok or no; in the first case, she promises to pay and wait for shipment.

In CO 2 , the behaviour of each participant is a process capable of advertising contracts and executing the actions required to honour them. For instance, the store A can advertise its contract c by firing the prefix tell K ↓ x c, where the index x in ↓ x c is the name of a channel of A, and K is the name of an external broker, whom the contract is being advertised to. We shall not specify the behaviour of K, and just assume that when it finds a contract compliant with c, a session is established between A and another participant, say B. Technically, x is replaced with a fresh session name s. Participants A and B will then use such session to perform the actions required by their contracts.

A possible specification of the store A is e.g.:

P M = (x) (tell K ↓ x c . (do x a . X M (x) + do x b . X M (x))) X M (x) def = do x ok . do x pay . ask x ship-a? . do x ship-a
Here, A creates a private channel x, and advertises the contract c. Once a session starts, P M can accept an order for a or b on x. This is modelled by the guards do x a and do x b of the choice operator + (not to be confused with + of contracts).

In both cases, the process X M (x) is invoked. There, A accepts the transaction with ok, and waits for payment. Then A checks whether the contract requires to ship apples: if the query ask x ship-a? passes, the goods are shipped. Otherwise, when the customer B orders Brunello, A maliciously gets stuck, and so B has paid for nothing. This store is dishonest: it does not respect its own contract c. Consider now a non-malicious implementation of the store. Before accepting orders, the store requires an insurance to cover shipment damages. With the contract c p = payP . cover ⊕ cancel , A promises to pay (payP) and then choose between getting the coverage, or cancelling the request. The new store process is:

P N = (x, y) tell C ↓ y c p . do y payP . tell K ↓ x c . do x a . do x ok . X N (x) + do x b . Y N (x, y) X N (x) def = do x pay . ask x ship-a? . do x ship-a + ask x ship-b? . do x ship-b Y N (x, y) def = do y cover . do x ok . X N (x) + τ . do x no
The store A first requests an insurance by advertising c p to an insurance company (say C); once C agrees, A pays the premium (on channel y), and then advertises c; once an agreement with a customer B is reached, A waits for a or b orders. If apples are requested, A acknowledges (ok) and invokes X N (x); there, A waits for payment, checks which good has to be shipped, and actually ships it. Otherwise, if Brunello is requested, Y N (x, y) is invoked: there, A requests the insurance coverage paid in advance; then, either the order is accepted and X N (x) is invoked for payment and shipment (as above), or the transaction is declined after an internal action τ (e.g. a wake up after a timeout).

This implementation is not malicious as the first attempt: it is keen to ship the goods, but it is not honest either due to the interaction between A and the insurance company. If C does not execute cover, A gets stuck on do y cover, unable to honour c by providing the expected ok/no. Furthermore, A is dishonest w.r.t. c p : the premium is paid in advance, but A may never perform do y cover nor do y cancel -e.g. if no agreement on c is found, or if the customer B is stuck, or if B simply chooses to buy apples. Thus, due to implementation naïveties, A may be blamed due to the unexpected (or malicious) behaviour of other participants.

Contributions. Our main contribution is a type discipline for statically ensuring when a CO 2 process is honest. The need for a static approximation is due to the fact that honesty is an undecidable property [START_REF] Bartoletti | On the realizability of contracts in dishonest systems[END_REF]. Our type system associates behavioural types to process channels. Checking honesty on these abstractions is decidable (Th. 1). We establish subject reduction (Th. 2) and progress (Th. 3), which are then used to prove type safety: typeable processes are honest (Th. 4).

Due to space constraints, we publish the proofs and further examples in a separate report [START_REF] Bartoletti | Honesty by typing[END_REF].

A Calculus of Contracting Processes

The calculus CO 2 is parametric on the contract model, i.e. on the language of contracts. Contract models for CO 2 have been defined based e.g. on formulae of Propositional Contract Logic [START_REF] Bartoletti | A calculus of contracting processes[END_REF], and on CCS processes [START_REF] Bartoletti | Contract-oriented computing in CO2[END_REF]. In this paper we focus on the two-party contracts of [START_REF] Castagna | A theory of contracts for web services[END_REF], as in [START_REF] Bartoletti | On the realizability of contracts in dishonest systems[END_REF]. Due to space limits, here we only give the main definitions, and refer the reader to [START_REF] Bartoletti | Honesty by typing[END_REF] for the full details.

We assume a set of participants A, B, . . ., and a set of atoms a, b, . . ., that represent the actions performed by participants. We use an involution ā, as in CCS, and assume a distinguished atom e, modelling a successfully terminated participant, such that e = ē.

A unilateral contract of [START_REF] Castagna | A theory of contracts for web services[END_REF] is a CCS-like process c which models the promised behaviour of a single participant. An internal sum c = i∈I a i ; c i requires a participant (say, A) to choose one of the actions a i , do it, and then behave according to its continuation c i . An external sum c = i∈I a i . c i requires A to offer a choice among all the branches; if a i is chosen by the other participant, then A must continue according to c i . Finally, c = ready a.c models an obligation of A to do a, and then to proceed as c . We denote (guarded) recursive contracts with rec X . c, and we let E = rec X . e ; X.

A bilateral contract γ = A says c | B says d combines the contracts of two participants. Its behaviour is given in [START_REF] Bartoletti | On the realizability of contracts in dishonest systems[END_REF] as a LTS. Its main rules regulate the interaction between the internal choices of A, and the external choices of B:

A says (ā ; c ⊕ c ) | B says (a . d + d ) A says a -----→ → A says c | B says ready a.d (1) A says c | B says ready a. d B says a -----→ → A says c | B says d (2)
By ( 1), if A chooses branch ā in her internal sum, then B is committed to the branch a in his external sum. We mark the selected branch with ready a, and discard the others. This enables (2) where B takes the marked branch. When an internal choice is not matched by an action in the external choice of the partner, the contract gets stuck. Intuitively, two contracts c, d are compliant, c d in symbols, when this situation cannot occur. The formal definition of compliance builds upon that of ready sets. For a contract c, the ready sets RS(c) are:

{{ready a}}, if c = ready a.c RS(c ), if c = rec X . c {{a i } | i ∈ I}, if c = i∈I ai ; ci and I = ∅ {{a i | i ∈ I}}, if c = i∈I ai . ci
Then, the relation on contracts is the largest relation preserved by contract transitions such that, whenever c d,

∀X ∈ RS(c), Y ∈ RS(d). {ā | a ∈ X }∩Y = ∅ or ∃a. ready a ∈ (X ∪Y)\(X ∩Y)
We now briefly review CO 2 . Let V and N be disjoint sets of, respectively, session variables x, y, . . . and session names s, t, . . .. Let u, v, . . . range over V ∪N . Systems S, processes P , prefixes π, and latent contracts K are defined below.

Definition 1 (CO 2 syntax). The syntax of CO 2 is given by:

P ::= i π i .P i P |P ( u)P X( u) π ::= τ tell A ↓ u c fuse do u a ask u φ K ::= ↓ u A says c K |K S ::= 0 A[P ] A[K] s[γ] S |S ( u)S
Processes specify the behaviour of participants. A process can be a prefixguarded finite sum i π i .P i , a parallel composition P | Q, a delimited process ( u)P , or a constant X( u). We write 0 for ∅ P , and π 1 .Q 1 +P for i∈I∪{1} π i .Q i provided that P = i∈I π i .Q i and 1 ∈ I. We omit trailing occurrences of 0.

We stipulate that each X has a unique defining equation X(u 1 , . . . , u j ) def = P s.t. fv(P ) ⊆ {u 1 , . . . , u j } ⊆ V, and each constant occurring in P is prefix-guarded.

Prefixes include the silent action τ , contract advertisement tell A ↓ u c, contract stipulation fuse, action execution do u a, and contract query ask u φ. In each prefix π = τ , the identifier u refers to the target session involved in the execution of π.

As in [START_REF] Bartoletti | On the realizability of contracts in dishonest systems[END_REF], we leave the syntax of observables φ unspecified.

A latent contract ↓ x A says c represents a contract c advertised by A but not stipulated yet. The variable x will be instantiated to a fresh session name upon stipulation. K simply stands for the parallel composition of latent contracts.

A system is composed of participants A[P ], sessions s[γ], sets of latent contracts advertised to A (denoted by A[K]), and delimited systems ( u)S. Delimitation ( u) binds session variables and names, both in processes and systems. Free variables and names are defined as usual, and denoted by fv( ) and fn( ). A system/process is closed when it has no free variables. Each participant may have at most one process, i.e. we forbid systems of the form

A[P ] | A[Q].
We say that S is A-free when it does not contain the participant A[P ], nor latent contracts of A, nor sessions with A's contracts. Note that sessions cannot contain latent contracts.

The semantics of CO 2 is formalised by a reduction relation on systems (Def. 2). This relies on a standard structural congruence relation -of which we just point out that ( u)A[( v)P ] ≡ ( u v)A[P ] allows to move delimitations between systems and processes, while

A[K] | A[K ] ≡ A[K | K ] allows A to collect latent contracts.
In order to define honesty in § 3, here we decorate transitions with labels, by writing

A : π,σ
----→ for a reduction where participant A fires prefix π. Also, σ is a substitution which accounts for the instantiation of session variables upon a fuse. The rules in Fig. 1 are a minor variation of those presented in [START_REF] Bartoletti | On the realizability of contracts in dishonest systems[END_REF]. Their intuitive meaning is sketched in the introductory example (Sec. 1): [Tell] advertises a contract c, [Fuse] creates a new session s upon contractual compliance, [Do] performs a contractual action, [Ask] blocks until session s satisfies observable φ.

Example 1. A possible execution of S = A[(x)X(x)] | B[(y)Y (y)] | C[fuse], where X(x) def = tell C ↓ x (a ; E) . do x a and Y (y) def = tell C ↓ y (a . E) . do y ā, is: S B : tell C ↓yā,∅ --------→ A[(x)X(x)] | C[fuse] | (y) (B[do y ā] | C[↓ y B says ā . E]) A : tell C ↓xa,∅ --------→(x)(A[do x a] | (y)(B[do y ā] | C[fuse] | C[↓ x A says a;E |↓ y B says ā.E])) C : fuse,∅ -----→ (s) (A[do s a] | (y) (B[do s ā] | C[0] | s[A says a;E | B says ā.E])) A : dos a,∅ ------→ (s) (A[0] | B[do s ā] | s[A says E | B says ready ā . E]) A[τ.P + P | Q] A : τ,∅ ----→ A[P | Q] [Tau] S A : π,σ ----→ S ran σ ∩ fn(S ) = ∅ S | S A : π,σ ----→ S | S σ [Par]
A[tell B ↓u c.P

+ P | Q] A : tell B ↓uc,∅ --------→ A[P | Q] | B[↓u A says c] [Tell] K σ γ ran σ = {s} s fresh A[fuse.P + P | Q] | A[K] A : fuse,σ -----→ A[P | Q]σ | s[γ] [Fuse] γ A says a -----→ → γ A[dos a.P + P | Q] | s[γ] A : dos a,∅ ------→ A[P | Q] | s[γ ] [Do] γ φ A[asks φ.P + P | Q] | s[γ] A : asks φ,∅ -------→ A[P | Q] | s[γ] [Ask] S A : π,{s/x} -------→ S (x)S A : π,∅ ----→ (s)S [Del1] S A : π,σ ----→ S u ∈ ran σ σ =u = ∅ (u)S A : π,σ =u ------→ (u)S [Del2] X( u) def = P A[P { v / u } | Q] | S A : π,σ ----→ S A[X( v) | Q] | S A : π,σ ----→ S [Def]
Fig. 1. Reduction semantics of CO2 .

On Honesty

A participant A is honest when she realizes every contract she advertises, in every session she may be engaged in. If a system S contains a session s with a contract c advertised by A, such as

A[P ] | s[A says c | • • •] | • • •, then A must realize c
, even in a system populated by adversaries who play to cheat her. To realize c, A must be "ready" to behave according to c. For instance, if A[P ] has advertised a contract c with an internal choice c i = a ⊕ b, then P must be ready to do at least one of the actions a, b. Instead, if c is an external choice c e = a + b, then P must be ready to do both the actions a and b.

Realizability requires the readiness property to be preserved by all transitions of S. In other words, in any reduct of S containing a reduct P of P and a reduct c of c, the process P must be ready for c . To formalise when "P is ready for c" we inspect the ready sets RS(c), which reveal whether c is exposing an internal or an external choice. At the process level, we consider the reachable actions in P . -P 0 = do s a is ready for c i , because {a} ∈ RS(c i ) and do s a is enabled in P 0 . Instead, P 0 is not ready for c e , since the ready set {a, b} of c e also contains b, which is not enabled in P 0 . -P 1 = do s a + do s b + do s z is ready for both c i and c e . Indeed, P 1 enables do s a and do s b, thus covering the ready sets of c i and c e . The branch do s z is immaterial: rule [Do] blocks actions not expected by the contract. -P 2 = τ.do s a + τ.do s b is ready for c i , because whatever branch is taken by P 2 , it leads to an unguarded action which covers one of the ready sets in c i . Instead, P 2 is not ready for c e , because after one of the two branches is chosen, one of the two actions expected by c e is no longer available. -P 3 = do t w.do s a + do t z.do s b is a bit more complex than the above cases. Readiness w.r.t. c i depends on the context. If the context eventually enables one of the do t , then either do s a or do s b will be enabled, hence P 3 is ready for c i . Otherwise, P 3 is stuck, hence it is not ready for c i . Notice that P 3 is not ready for c e , regardless of the context.

To formalise readiness, we start by defining the set RD A u (S) (for "Ready Do"), which collects all the atoms with an unguarded action do u of A in a system S.

Definition 3 (Ready do). For all S, A and u, we define the set RD A u (S) as:

RD A u (S) = {a | ∃ v, P, P , Q, S . S ≡ ( v) (A[do u a.P + P | Q] | S ) ∧ u ∈ v}
As seen for P 2 and P 3 , readiness may also hold when the actions expected in the contract ready sets are not immediately enabled in the process. To check if A[P ] is ready for s (in a system S), we need to consider all actions which (1) are exposed in P after some steps, taken by P itself or by the context, and (2) are not preceded by other do s performed by A. These actions form the set WRD A s (S).

Definition 4 (Weak ready do). We define the set of atoms WRD A u (S) as:

WRD A u (S)
WRD A x (S) = {ā} = RD A x (S) WRD A y (S) = {a} ⊇ RD A y (S) = ∅
On channel y, the action a is weakly reachable through its τ prefix. Action b is not weakly reachable, because guarded by a stuck do x . Action c is not weakly reachable as well, because preceded by another do on the same channel.

Example 4. Let P 3 as in Ex. 2, and consider the following system:

S = A[P 3 ] | B[τ . do s ā . do s b] | C[do t w + do t z + τ ] | s[A says a + b | B says ā ⊕ b] | t[A says w + z | C says w ⊕ z]
In session t, A is immediately ready to do either w or z, so her ready do set coincides with her weak ready do set in t. The same for C, with the dual atoms w and z. Thus:

WRD A t (S) = RD A t (S) = {w, z} WRD C t (S) = RD C t (S) = {w, z}
In session s, the ready do sets of both A and B are empty, because their actions are not immediately enabled. Before they can be reached, the whole system S must first reduce, either with the contribution of C on session t (in the case of A), or through a τ action (in the case of B). These reductions fall within the definition of their weak ready do sets, which are accordingly non-empty.

WRD B s (S) = {ā} ⊇ RD B s (S) = ∅ WRD A s (S) = {a, b} ⊇ RD A s (S) = ∅
Notice that b ∈ WRD B s (S): in fact, b is guarded by do s ā. Also, if C chooses to perform τ , then the actions in WRD A s (S) would not be reached. Indeed, Def. 4 requires that each element in the set becomes reachable at the end of a suitable reduction trace -but it does not prevent S from reducing along other paths.

A participant A is ready in a system S with a session s[A says c | • • • ] iff A is (weakly) ready to do all the actions in some ready set of c. Note that A is vacuously ready in systems not containing sessions with A's contracts.

Definition 5 (Honesty). We say that A is ready in S iff, whenever S ≡ ( u)S for some u and

S = s[A says c | • • •] | S 0 , ∃X ∈ RS(c) . ∀a = e . a ∈ X ∨ ready a ∈ X =⇒ a ∈ WRD A s (S ) A[P ] is honest iff ∀ A-free S and ∀ S such that A[P ] | S → * S , A is ready in S .
The A-freeness requirement in Def. 5 is used just to rule out those systems already carrying stipulated or latent contracts of A outside A[P ], e.g.

A[P ] | B[↓ x A says pay | • • •].
In the absence of A-freeness, the system could trivially make A[P ] dishonest.

Example 5. In the system below, A might look honest, although she is not.

S def = A[(x, y) (P A | fuse | fuse)] | B[P B ] | C[P C ] P A def = tell A (↓ x a . E) . tell A (↓ y b ; E) . do x a . do y b P B def = (z) (tell A (↓ z b . E) . do z b) P C def = (w) (tell A (↓ w ā ; E) . 0)
In fact, if we reduce S by performing all the tell and fuse actions, we obtain:

S = (s, t) ( A[do t a . do s b] | B[do s b] | C[0] | t[A says a . E | C says ā ; E] | s[A says b ; E | B says b . E]
Here, S cannot reduce further: A is stuck, waiting for ā from C, which (dishonestly) avoids to do the required internal choice. So, A is dishonest, because she does not perform the promised b.

Formally, A is dishonest because RS(b ; E) = {{b}}, but b ∈ WRD A s (S )
. Thus, A is not ready in S , hence not honest in S. Our definition of honesty subsumes a fair scheduler, eventually allowing participants to fire persistently (weakly) enabled do actions. For instance, let c = a ⊕ b, and let:

P def = (x) tell A ↓ x c . fuse . X(x) where X(x) def = τ . X(x) + τ . do x a + τ . do x b
Let S = A[P ] | S 0 , and assume that the fuse in P passes. Under an unfair scheduler, A could always take the first branch in X, while neglecting the others. Intuitively, this would make A not respect her contract, which expects a or b. However, a fair scheduler will eventually choose one of the other branches.

We now introduce a type system for CO 2 . The main result is type safety (established in Th. 4), which guarantees that typeable participants are honest.

The type of a process P is a function f , which maps each channel to a channel type. Channel types are behavioural types which essentially preserve the structure of P , while abstracting the actual prefixes and delimitations. Mainly, the prefixes of channel types distinguish between nonblocking and possibly blocking actions.

Channel types

Channel types are Basic Parallel Processes (BPPs [START_REF] Christensen | Decidability and Decomposition in Process Algebras[END_REF]) with standard semantics. Their prefixes can be atoms (a, b, . . .), contract advertisement actions ( c ), nonblocking (τ ), possibly blocking (τ ? ), and conditional (τ φ ) silent actions.

Definition 6 (Channel types). Channel types T and prefixes α are:

T ::= 0 α . T T + T T | T rec X . T X α ::= a τ τ ? τ φ c Example 6. Let P = tell B ↓ x c i | tell B ↓ y d . do x ā
, where c i = ā ⊕ b, and d is immaterial. We anticipate that the channel types associated by our type system to P on channels x and y are, respectively, T x = c i | τ . ā, and

T y = τ | d . τ ? .
Note that the advertisement of ↓ x c i is recorded in T x , while that of ↓ y d is abstracted there as a τ . Instead, the τ ? in T y represents the fact that do x ā is not visible from channel y, and may potentially block.

The execution of CO 2 systems relies both on processes and contracts. Thus, we use an abstraction of the contract/process interplay to define abstract processes.

Definition 7 (Abstract processes). An abstract process is a pair (C, T ) or (c, T ), where C is a set of contracts, c is a contract, and T is a channel type.

An abstract process (C, T ) represents a process abstracted by T on some channel x, after the contracts in C have been advertised. Instead, (c, T ) represents a process abstracted by T on channel x, after the contract c has been stipulated.

The semantics of abstract processes is given in Fig. 2. The set C grows when a channel type T in (C, T ) performs a transition with label c . After a contract c ∈ C has been stipulated, the set is reduced to c. A label a models a do a action performed by T , while rule ctx models an (unknown) action performed by the context. Further advertisements after contract stipulation are neglected.

The relation -→ → abstracts the contract semantics -→ →, by considering only the contract advertised by P (instead of the whole bilateral contract). We leave the relation -→ → unspecified (see [START_REF] Bartoletti | On the realizability of contracts in dishonest systems[END_REF] for a possible instantiation), and we just require that -→ → is decidable, and for all γ = A says c | B says d such that c d, We now introduce the abstract counterpart of the dynamic notion of honesty in § 3. We shall follow the path outlined for concrete processes: first we define when a channel type T is "ready for a contract", and then when T is honest.

γ A says a -----→ → A says c | B says d =⇒ c a - → → c γ B says b -----→ → A says c | B says d =⇒ c ctx --→ → c T c ---→ T (C, T ) → (C ∪ {c}, T ) T d ---→ T (c, T ) → (c, T ) c ∈ C (C, T ) → (c, T ) c ctx --→ → c (c, T ) → (c , T ) T α --→ T α ∈ {τ, τ ? , τ φ } (C, T ) → (C, T ) c a -→ → c T a --→ T (c, T ) → (c , T ) T α --→ T α ∈ {τ, τ ? , τ φ } (c, T ) → (c, T ) T a -→ T T a = ⇒ T T τ -→ T a = ⇒ T T a = ⇒ T T d --→ T a = ⇒ T T a = ⇒ T T τ φ -→ T a = ⇒ T c A φ T a = ⇒ T
Weak transitions abstract the weak ready do. They are defined in Fig. 2 as a labelled relation a

=⇒ c

A (simply written as a =⇒ when unambiguous). The first two rules are standard: they just collapse the τ actions as usual. The third rule also collapses contract advertisement actions, which are nonblocking as well. Possibly blocking actions τ ? are not collapsed, while τ φ (which abstract ask u φ prefixes) are dealt with the last rule: they abstract the CO 2 prefix ask u φ, and they are collapsed only if such ask is nonblocking. The relation A safely (under-) approximates this condition. We leave A unspecified (just like in § 2), and we only require that it respects the constraint in Def. 8 below. Unlike in the concrete case, the context is immaterial in determining weak transitions. Below we relate the weak transitions of a channel type with the ready sets of a contract, similarly to what we did in Def. 5 for CO 2 processes. Weak transitions under-approximate the weak ready do set. Thus, if an abstract process is honest then also the concrete one will be such (while the vice versa is not always true).

Honesty of abstract processes is defined similarly to Def. 5. In order to be honest, a process must keep itself (abstractly) ready upon transitions. Readiness must be checked against all the contracts that may be stipulated along the abstract process reductions. Definition 9 (Abstract honesty). We say that channel type T is abstractly ready for contract c iff ∃X ∈ RS(c).∀a = e. (a ∈ X ∨ ready a ∈ X ) =⇒ T a =⇒ . An abstract process (-, T ) is honest iff, whenever (-, T ) → * (c, T ), then T is ready for c. A channel type T is honest iff (∅, T ) is honest. To prove T x is honest, we examine all the reducts of the abstract process (∅, T x ) to check for readiness. We have the following cases:

1. (∅, T x ). Nothing to check, because no contracts have been advertised yet. 6. (c i , a). We have that a is ready for c i , similarly to the previous case. 7. (E, 0). We have that 0 is vacuously ready for E.

Th. 1 below establishes that checking the honesty of a channel type T is decidable. Indeed, abstract readiness and abstract dishonesty are reachability properties. Abstract processes are the product of a finite state system (C and c only admit finitely many states), and a BPP T . This product can be modelled as a Petri net. Decidability follows since reachability is decidable for Petri nets [START_REF] Mayr | Decidability and Complexity of Model Checking Problems for Infinite-State Systems[END_REF].

Theorem 1. Abstract honesty is decidable.

Process types

A CO 2 process type associates session names/variables to channel types, thus abstracting the behaviour of a process on all channels. Here, we introduce a "dummy" channel * ∈ N ∪V, for collecting type information about unused channels. Formally, a process type is a function f from N ∪ V ∪ { * } to channel types.

Our type system abstracts concrete prefixes of CO 2 processes as actions of channel types. We observe the behaviour of a process P on each channel, say u. When P performs an action on one of its channels, say v, we have two cases: v = u: we will only observe a silent action, either nonblocking (τ ) or blocking (τ ? ), depending on the concrete prefix fired. v = u: we may observe more information, depending on the concrete prefix. For instance, if P advertises a contract c with a tell ↓ v c, then the action c will be visible if v = u, while we shall just observe a τ if v = u (because tell is nonblocking). Similarly, if P performs do v a we shall observe the action a if v = u and τ ? if v = u (because do is blocking). Finally, if P executes a query ask u φ we shall observe the conditional silent action τ φ if v = u and τ ? otherwise.

Definition 10 (Prefix abstraction). For all u ∈ N ∪ V ∪ { * }, we define the mapping [•] u from CO 2 prefixes to channel type prefixes as follows:

[τ ] u = τ [fuse] u = τ ? [tell A ↓ v c] u = if v = u then c else τ
We have given a type system for a calculus of contracting processes. Type safety establishes honesty: typeable processes honour their contracts in all contexts.

In [START_REF] Bartoletti | On the realizability of contracts in dishonest systems[END_REF], A is considered "honest" when not definitely culpable (in any session), i.e., A eventually performs the actions her contract prescribes. In Def. 5, honesty is based on readiness, rather than culpability; we conjecture that the two notions are equivalent. The main advantage of this new approach compared to [START_REF] Bartoletti | On the realizability of contracts in dishonest systems[END_REF] is that it simplifies the proof of the correctness of the static analysis of honesty, by more directly relating abstract transitions with concrete ones. Also, the new definition helps in proving decidability of abstract honesty, which was left open in [START_REF] Bartoletti | On the realizability of contracts in dishonest systems[END_REF].

In [START_REF] Bocchi | A theory of design-by-contract for distributed multiparty interactions[END_REF] (multiparty) asserted global types are used to adapt design-by-contract to distributed interactions. In our framework, a participant declares its contract independently of the others; a CO 2 primitive (fuse) tries then to combine advertised contracts within a suitable agreement. In other words, one could think of our approach as based on orchestration rather than choreography.

In [START_REF] Honda | Multiparty asynchronous session types[END_REF] the progress property is checked only when participants engage at most in one session at a time. Honesty is a sort of progress property, and our type system allows participants to interleave many sessions as done in [START_REF] Coppo | Global Progress for Dynamically Interleaved Multiparty Sessions[END_REF]. A crucial difference with respect to [START_REF] Coppo | Global Progress for Dynamically Interleaved Multiparty Sessions[END_REF] is that the typing discipline there requires the consistency of the local types of any two participants interacting in a session. Namely, if in a session s, A and B are typed as T A and T B respectively and they interact then the projection of T A with respect to B must be dual of the projection of T B with respect to A. In our type system instead, participants are typechecked 'in isolation' and to establish the honesty of a participant A our typing discipline only imposes that the surrounding context is A-free.

Other approaches deal with safety, by generating monitors that check at runtime the interactions of processes against their local contract (e.g., [START_REF] Chen | Specifying Stateful Asynchronous Properties for Distributed Programs[END_REF][START_REF] Chen | Asynchronous distributed monitoring for multiparty session enforcement[END_REF]).

The problem of checking if a contract c, representing the behaviour of a service, conforms to a role r of a choreography H has been investigated in [START_REF] Bravetti | Towards a unifying theory for choreography conformance and contract compliance[END_REF]. Conformance of c is attained by establishing a should testing pre-order between c and the projection of H with respect to role r. Similar techniques have been used in [START_REF] Bravetti | Contract-based discovery and composition of web services[END_REF] to define contract-based service composition. A main difference w.r.t. our approach, is that [START_REF] Bravetti | Towards a unifying theory for choreography conformance and contract compliance[END_REF][START_REF] Bravetti | Contract-based discovery and composition of web services[END_REF] do not consider conformance in the presence of dishonest participants. Actually, they focus on matching a contract as a role within a choreography, while we establish if a process abides by its own contracts, regardless of the context.

In [START_REF] Buscemi | Constraints for service contracts[END_REF][START_REF] Buscemi | CC-Pi: A constraint-based language for specifying service level agreements[END_REF], constraints are used to rule out "inconsistent" executions. This is orthogonal to our approach, since our aim is to blame participants that misbehave.

Definition 2 (

 2 CO 2 semantics). The relation A : π,σ ----→ between systems (considered up-to structural congruence ≡) is the smallest relation closed under the rules of Fig. 1. The relation K σ γ holds iff (i) K has the form ↓ x A says c | ↓ y B says d, (ii) c d, (iii) γ = A says c | B says d, and (iv) σ = { s /x,y} maps x, y ∈ V to s ∈ N . The substitution σ =u in rule [Del2] is defined as σ(v) for all v = u, and it is undefined on u.

Example 2 .

 2 Let c i = a ⊕ b, and let c e = a + b. Then, RS(c i ) = {{a}, {b}}, and RS(c e ) = {{a, b}}. Consider now the following processes:

Example 3 .

 3 = {a | ∃S : S =(A : dou) ------→ * S and a ∈ RD A u (S )} where S =(A : dou) ------→ S iff ∃B, π, σ. S B : π,σ ----→ S ∧ (B = A ∨ ∀a. π = do u a). For S = A[do x ā . do y b + τ . do y a . do y c | (x) do x b], we have:

Fig. 2 .

 2 Fig. 2. Abstract processes semantics and channel type semantics.

Definition 8 (

 8 Abstract observability). We write c A φ for any decidable relation satisfying: c A φ =⇒ ∀B . ∀d . (c d =⇒ A says c | B says d φ).

Example 7 .

 7 Let T x = c i | τ . a, and recall the contract c i = a ⊕ b from Ex. 2.

  2. (∅, c i | a). Similar to the previous case. 3. ({c i }, τ . a). Nothing to check, since no contracts have been stipulated yet. 4. ({c i }, a). Similar to the previous case. 5. (c i , τ .a). Here τ .a is ready for c i , as {a} ∈ RS(c i ) = {{a}, {b}} and τ .a a =⇒.

[do v a] u = if v = u then a else τ ? [ask v φ] u = if v = u then τ φ else τ ?The typing judgments for processes have the form Γ P : f , where Γ is a typing environment, giving types to processes of the form X( v).Definition 11 (Typing environment).A typing environment Γ is a partial function associating process types to constants X( v).

Acknowledgments. Work partially supported by Aut. Region of Sardinia under grants L.R.7/2007 CRP-17285 (TRICS), P.I.A. 2010 Project "Social Glue", and by MIUR PRIN 2010-11 project "Security Horizons", and by the Leverhulme Trust Programme Award "Tracing Networks", and by COST Action IC1201: Behavioural Types for Reliable Large-Scale Software Systems (BETTY), and by European Union Seventh Framework Programme under grant agreement no. 295261 (MEALS).

Γ Pi : fi ∀i ∈ I Γ i∈I πi . Pi : λu . i∈I [πi]u . fi(u)

where

Fig. 3. Typing rules for processes.

In Fig. 3 we introduce the typing rules for CO 2 processes. Rule ) is worth some comments. Assume that P is typed with f . Since u in not free (u)P , the actions on channel u must not be observable in the typing of (u)P . To do that, in the typing of (u)P we discard the information on u, by replacing it with the typing information on the "dummy" channel * . However, since this might hide a dishonest behaviour on u, the rule also checks that f (u) is honest. Moreover, if the environment Γ has typing information on channel u, this cannot be used while typing P . The typing environment Γ =u , which discards the information on u, is used to this purpose. Example 8. Recall process P 2 = τ .do s a+τ .do s b from Ex. 2. Its typing derivation is:

We have f (s) = τ . a + τ . b, and for all u = s, f (u) = f ( * ) = τ . τ ? + τ . τ ? . In other words, the process type f performs some visible actions when observed at channel s, while remaining "silent" on other channels.

The type system assigns the same type (up-to structural congruence) to all non-free session names/variables, and to * ; such type may only contain τ and τ ? .

Lemma 1. For all P , P : f =⇒ f ( * ) only contains τ and τ ? actions.

A process type f takes a transition on a CO 2 prefix π when all its points f (u) agree to take a transition on the abstract prefix [π] u . Definition 12. We write

Note that, in this case, we also have

If f is the type of some CO 2 process (i.e., f is inhabited ), and a single point f (u) takes an abstract transition, then the whole f can take a transition.

Note that, when P : f , checking the honesty of f amounts to checking f (u) honest only for each u ∈ fnv(P ). In fact, f (v) = f ( * ) when v ∈ fnv(P ), and f ( * ) is trivially honest because it cannot advertise contracts.

System typing

In this section we establish type safety for CO 2 processes: for any typeable closed P , A[P ] is honest. To prove this result, we have to consider the transitions of a process within a system. Hence, in order to construct an invariant of the system transitions (i.e., proving subject reduction), we extend typing to systems.

Type judgments for systems are of two kinds. A judgment of the form A S : f guarantees that a participant A in S behaves according to f . Instead, a judgment of the form A S f means that A is not in S, and S is compatible with any participant A behaving as f . Our notion of compatibility is liberal: intuitively, it just checks that the context S does not contain forged contracts of A. SDel1] it represents the behaviour of A outside S. Note that if A[P ] is typeable, then it can be inserted in any A-free system, and the composed system will be typeable.

Definition 14 (System typing). The relations

Assume that P : f . Then, a typing derivation of S = A[P ] | S 0 is:

Type safety

Subject reduction guarantees that typeability is preserved by transitions. We need to distinguish two cases, according to which participant moves: either the participant A under typing, or any other B. If the transition is done by A, then also its process type must take a transition, otherwise the type is preserved. The substitution induced when executing a fuse also affects the type of the reduct system. For instance, consider A[P ] | S, where P : f and f (x) = T . Assume that S fires a fuse, with a substitution σ mapping x to a fresh session name s. In the type, this is reflected by updating f according to σ, so to map s to T , and x, which is no longer free, to f ( * ). Technically, this is done as follows.

Definition 15. For a type f and a mapping { v / u}, the partial operator • is:

Theorem 2 (Subject reduction). If A S : f with f honest, then:

Progress guarantees that if a typeable process has a "non-blocking" type, then it can take a transition. More precisely, if the type of P on channel u can take a weak transition with label a, then P will have a in its weak ready do set. A , then a ∈ WRD A s (S). The main result of this paper is the type safety of CO 2 processes. It ensures that a participant A with a well-typed process P will always respect her contractsboth those already advertised, and those that she will publish along her reductions. Therefore, A will never be considered culpable in any context. Theorem 4 (Type safety). ∀ A[P ] with P closed, P : f =⇒ A[P ] is honest.