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

3.3 Properties and Claims

In our case study, the agents make an agreement to trust the content of logs,
in order to establish liability for a given set of claims. Then it is necessary to
express these claims in terms of log events in an unambiguous way. We assume
that liability for claims take the form: “if Prop holds, then agent defendant is
responsible”. This structure is explained in more details in [15].
The machine Claims below introduces some general definitions and allows us
to declare particular instances of properties and claims.

MACHINE Claims
INCLUDES LogModel
CONSTANTS PROP,CLAIM
PROPERTIES
/* Log Properties */
PROP

= { prop | prop ∈F ( AGEN T ) × ( LOG FILE → BOOL) ∧

∀ ( )) }∧

prop NoRoom ∈ PROP ∧ prop LateCancel ∈ PROP ∧

ags, log ) . ( prop =( ags, log ) ⇒ ags = agents ( log

... ∧

/* Claims */
CLAIM = { claim | claim ∈ ( AGEN T × AGEN T × PROP ) ∧

∀ ( plain, def, prop ) . ( claim =( plain, def, prop ) ⇒

{ plain, def }⊆ agents ( prop )) }∧

NoRoom ∈ CLAIM ∧ NoRoom =( Client , Agency , prop NoRoom ) ∧

LateCancel ∈ CLAIM ∧ LateCancel =( Client , Agency , prop LateCancel )

END
Due to the distributed nature of logs, the first element of a property explicitly
states the agents that are concerned with this property. The second element of
the property is a partial function that maps a log file to true or false depending if
thelogfileverifiestheproperty.Weusethenotation agents

)
indicating respectively the first and second parts of a property prop .Inaproperty
it is imposed that the domain of logs matches exactly with the agents concerned
by the property. Claims are tuples consisting of a plaintiff, a defendant, and a
property that describes the claim, with the plaintiff and the defendant belonging
to the agents of the property.

( prop ) and val ( prop

Example 5. (property prop NoRoom ) Now, consider the claim N oRoom described
in Section 2.1. Let prop NoRoom be the property that describes the claim where
Client complains of Agency being responsible for charging him/her without
booking the reservation:

agents ( prop NoRoom )= { Client, Agency }∧

val ( prop NoRoom )= λlog. ( agents ( log )= { Client, Agency }|

( Send, Client, Agency, Request ) ∈ events ( log ) ∧

( Send, Agency, Bank, Debit ) ∈ events ( log ) ∧

( Send, Agency, Hotel, Book ) ∈ events ( log )) ∧

pos (( Send, Client, Agency, Request ) ,log ) <

pos (( Send, Agency, Bank, Debit ) ,log ))