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)