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

5LogAn ly s

In this section, we give the general method of our log analyzer. Given the values
of the current logs and a particular claim, the aim is to establish the truthfulness
of this claim based on the content of the logs.

5.1 Log Analyzer

First, we present the definition of the operation PropAnalysis .
scen, ok

← PropAnalysis ( logs, prop )=

PRE
logs ∈ LOG ARCH ∧ prop ∈ PROP ∧ agents ( prop ) ⊆ agents ( logs )

THEN
scen :=

extract agents ( prop ) [ merge [ logs ]];

) − 1 [ { TRUE } ]

ok := scen ∩ val ( prop

END
END
For a given set of logs logs , the operation PropAnalysis researches scenarios
that hold for a given property prop . Two results are computed: the set of possible
different scenarios ( scen ) zooming only on the concerned agents of the property,
and among them, the subset of these scenarios that fulfill the property ( ok ). The
ratio between the two sets scen and ok may inform us the level truthfulness of
the researched property for the given logs.
Now, the method for the analysis of a claim of the form ( plain, def, prop )

proceeds as follows:

1. Select a set of logs in the global log architecture such that { plain, def }⊆

.These logs may represent the current global set of logs or only
a subset of them.
2. Execute scen, ok

agents ( prop )

)
3. Analyze the results in term of the admissibility of the claim and its expla-
nation. For instance:
- if ok

← PropAnalysis ( logs, prop

scen the property holds for all scenarios, which leads us to
conclude that the claim is valid and the defendant is responsible;
- if ok

=

the property is false for all scenarios, and leads us to conclude
that the claims should be rejected;
- otherwise, an appropriate examination of scenarios that fulfill (or not)
the property has to be conducted.

= ∅

If the results are not conclusive, it could be necessary to increase the amount of
logs used in the analysis, as we explain in Section 5.2.

Example 8. (claim N oRoom analysis) Suppose we have the following current
logs representing the scenario illustrated in Figure 3: