contractual freedom. 14

3. FoRmaL sPeCiFiCation oF LiaBiLities

The share of liabilities between the parties was expressed in Section 2. 3 in a traditional, informal way. Texts in natural language, even in legal language, often conceal ambiguities and misleading representations. The situation is even worse when such statements refer to mechanisms which are as complex as software. Such ambiguities are sources of legal uncertainties for the parties executing the contract. The use of formal (mathematical) methods has long been studied and put into practice in the computer science community to define the specification of software systems (their expected behavior) and to prove their correctness or to detect errors in their implementations. For various reasons however (both technical and economical), it remains difficult to apply formal methods at a large scale to prove the correctness of a complete system.

In contrast with previous work on formal methods, our goal here is not to apply them to the verification of the system itself (the mobile phone solution in our case study) but to define liabilities in case of malfunction and to build an analysis tool to establish these liabilities from the log files of the system.

It should be clear however, as stated in Section 1, that our goal is not to provide a monolithic framework in which all liabilities would have to be expressed. The method proposed here can be used at the discretion of the parties involved and as much as necessary to express the liabilities concerning the features or potential failures deemed to represent the highest sources of risks for them.

In this section, we present successively the parameters which are used to establish liabilities (Sections 3. 1 and 3. 2) before introducing the liability function in Section 3. 3.

3. 1. trace model

Following the informal description in Section 2, the sets of components, parties, and users are defined as follows:

Components = {Serv, SigApp, Card, IO, OpSys}

Parties = {MPP, SAP, SCP}

Users = {OWN, ECC}

Q is the set of stamps and C the set of communicating entities (components and users). O and M denote, respectively, the set of communication operations and message contents. The distinction between send and receive events allows us to capture communication errors.d We assume that signature sessions in traces are complete d This feature is not illustrated in this paper.

and the type (document, response, PIN code, and signature) of each element composing a message is implicitly associated with the element itself in order to avoid any ambiguity.

We denote by Traces the set of all traces, a trace T being
defined as a function associating a stamp with a list of items.
Each item is defined by the communication operation (Send
or Receive), the sender, the receiver, and the content of the
message:
A first comment on the above definition is the fact
that we use a functional type (from stamps to lists
of items) to represent traces. This choice makes the
manipulation of traces easier in the sequel because we
are always interested in the items corresponding to a
given session. Other representations could have been
chosen as well, such as lists of items including the stamp
information.

3. 2. trace properties

We present successively the two types of trace properties used in this paper: error properties and claim properties. Error Properties: The most important parameter to determine the allocation of liabilities is the nature of the errors which can be detected in the log files of the system. Ideally, the framework should be general enough to reflect the wishes of the parties and to make it possible to explore the combinations of errors in a systematic way. One possible way to realize this exploration is to start with a specification of the key properties to be satisfied by the system and derive the cases which can lead to the negation of these properties.

Our goal being to analyze log files, we characterize the expected properties of the system directly in terms of traces. For example, the fact that SigApp should send to IO the document D received from Serv (and only this document) can be expressed as follows:

Same-Doc (T,q) ≡
∀D ∈ Documents,
(Receive, Serv, SigApp, [D]) ∈ T (q) ⇔
(Send, SigApp, IO, [D]) ∈ T (q)

In the scenario considered here, the systematic study of the cases of violation of this property leads to the following errors:

SigApp-Diff ( T,q) ≡

$D, D′ ∈ Documents, D ≠ D′ Ù

(Receive, Serv, SigApp, [D]) ∈ T(q) Ù (Send, SigApp, IO, [D′ ]) ∈ T(q)