A Formal Framework for Specifying and Analyzing Logs as Electronic Evidence - Formal Methods: Foundations and Applications - page 198

injective sequences of elements of A . A sequence is delimited by the square brackets
(' )

denotes the function that maps every x that verifies the predicate P into the value
of expression E . Finally, for readability, we sometimes omit the declaration of the
type of variables whenever we judge the type is easy to infer.

[ 'and' ] ') and its elements separated by commas (' , '). The notation λx. ( P | E

3 Logs and Claims

In this section we present how, in our framework, we specify the expected infor-
mation about the system, the logs and the claims. The proposed model is based
on exchanged messages that are used to represent the interactions between the
entities of the system. We will assume here that each message is unique. We
will also assume that we are able to identify the origin of exchanged messages.
However, our framework can be easily adapted for working without assuming
such hypothesis. This model of communication is well adapted to the domain
of B2B applications that we mentioned in the introduction, including electronic
service and resource provision.
We consider a system consisting of agents participating in some form of inter-
actions described as events, and each event is performed by one of the agents.
Particular agents may have the ability to monitor the events performed by itself
and other agents and record these events in a log 2 . The agents should agree that
the produced logs are liable for representing the event's history.

3.1 System Information

The machine SystemInfo specifies a set of agents ( AGEN T ) and a set of actions
( ACT ION ). Each action is associated with the agent that can execute it by the
function Interface . The information associated with the system in study is
marked in bold.

Example 3. (agents and interface) Let us write the machine SystemInfo for our
case study such that:
MACHINE SystemInfo
SETS
AGEN T

= { Client , Agency , Hotel , Bank } ;

ACT ION = { Request , Book , Debit , Confirm , Justify , Cancel }

CONSTANTS Interface
PROPERTIES
Interface : ACT ION → AGEN T ∧

Interface = { ( Request , Client ) , ( Book , Agency ) , ( Debit , Agency ) ,

( Confirm , Hotel ) , ( Justify , Bank ) , ( Cancel , Client ) }

END

2 Logs can also be produced by some mechanism that does not directly belong to the
system, such as protocol sniffers.