Time-Stamped Claim Logic

TL;DR

This paper introduces Time-Stamped Claim Logic, a formal system for reasoning about evidence from multiple sources with trust considerations, demonstrated through a cyber-attribution case study.

Contribution

It defines a new logic with a sound and complete calculus for managing and resolving contradictory evidence based on trustworthiness.

Findings

The logic reduces evidence set size effectively.

It ensures consistency with trust relations.

Applied successfully in a cyber-attribution case study.

Abstract

The main objective of this paper is to define a logic for reasoning about distributed time-stamped claims. Such a logic is interesting for theoretical reasons, i.e., as a logic per se, but also because it has a number of practical applications, in particular when one needs to reason about a huge amount of pieces of evidence collected from different sources, where some of the pieces of evidence may be contradictory and some sources are considered to be more trustworthy than others. We introduce the Time-Stamped Claim Logic including a sound and complete sequent calculus that allows one to reduce the size of the collected set of evidence and removes inconsistencies, i.e., the logic ensures that the result is consistent with respect to the trust relations considered. In order to show how Time-Stamped Claim Logic can be used in practice, we consider a concrete cyber-attribution case study.

Equations

$$K_P=\{-(t\cdot p),t\cdot p\mid t\in X_T\text{ and }p\in P\}$$

$$a_1::(t\cdot {\text{inplace}}_C^J,t\cdot {\text{capable}}_C^J,t\cdot {\text{motive}}_C^J/t\cdot {\text{culprit}}_C^J)$$

$$\forall x.x{⊴}_{{\text{motive}}_{\text{C}}^{\text{J}}}{a}_3$$

$${\text{var}}_A:\wp L_P\to \wp X_A$$

$$\Gamma \to \Delta ,$$

$$\frac{{\Gamma }_1\to {\Delta }_1\cdots {\Gamma }_n\to {\Delta }_n}{\Gamma \to \Delta }F$$

$$--(t\cdot p)$$

$$\frac{}{\beta ,\Gamma \to \Delta ,\beta }$$

$$\frac{\beta ,\Gamma \to \Delta \Gamma \to \Delta ,\beta }{\Gamma \to \Delta }$$

$$\frac{}{\Gamma \to \Delta ,t\cong t}$$

$$\frac{}{t_1\cong t_2,\Gamma \to \Delta ,t_2\cong t_1}$$

$$\frac{}{t_1\cong t_2,t_2\cong t_3,\Gamma \to \Delta ,t_1\cong t_3}$$

$$\frac{}{t_1\cong t_2,[a:\varphi {]}_{t_2}^{t_1},\Gamma \to \Delta ,a:\varphi }$$

$$\frac{}{a_1{⊴}_p{a}_2,a_2{⊴}_p{a}_3,\Gamma \to \Delta ,a_1{⊴}_p{a}_3}$$

$$\frac{}{\Gamma \to \Delta ,a{⊴}_{p}a}$$

$$\frac{}{a_1{⊴}_p{a}_2,a_2{⊴}_p{a}_1,[a:\varphi {]}_{a_2}^{a_1},\Gamma \to \Delta ,a:\varphi }$$

$$\frac{\Gamma \to \Delta ,b{⊴}_{p}a}{\Gamma \to \Delta ,\forall x.x{⊴}_{p}a}b$$

$$\frac{a^{\prime }{⊴}_{p}a,\forall x.x{⊴}_{p}a,\Gamma \to \Delta }{\forall x.x{⊴}_{p}a,\Gamma \to \Delta }$$

$$\frac{a:-\varphi ,\Gamma \to \Delta ,a:\varphi }{a:-\varphi ,\Gamma \to \Delta }$$

$$\frac{-\varphi ,\Gamma \to \Delta ,\varphi }{-\varphi ,\Gamma \to \Delta }$$

$$\frac{\Gamma \to \Delta ,t_1\cong t_2,a:-(t_1\cdot p),a:t_2\cdot p}{\Gamma \to \Delta ,t_1\cong t_2,a:-(t_1\cdot p)}$$

$$\frac{\Gamma \to \Delta ,t_1\cong t_2,-(t_1\cdot p),t_2\cdot p}{\Gamma \to \Delta ,t_1\cong t_2,-(t_1\cdot p)}$$

$$\frac{b:-\varphi ,a{⊴}_{{\text{var}}_P(\varphi )}b,\Gamma \to \Delta }{\Gamma \to \Delta ,a:⊡\varphi }b$$

$$\frac{a:⊡\varphi ,\Gamma \to \Delta ,a{⊴}_{{\text{var}}_P(\varphi )}{a}^{\prime }a:⊡\varphi ,\Gamma \to \Delta ,a^{\prime }:-\varphi }{a:⊡\varphi ,\Gamma \to \Delta }$$

$$\frac{b:-\varphi ,b:⊡-\varphi ,\Gamma \to \Delta \Gamma \to \Delta ,\varphi ,a:\varphi \Gamma \to \Delta ,\varphi ,a:⊡\varphi }{\Gamma \to \Delta ,\varphi }b$$

$$\frac{b:\varphi ,b:⊡\varphi ,\Gamma \to \Delta }{\varphi ,\Gamma \to \Delta }b$$

$$\frac{\varphi ,\Gamma \to \Delta ,a:-\varphi \varphi ,\Gamma \to \Delta ,a:⊡-\varphi }{\varphi ,\Gamma \to \Delta }$$

$$\frac{{\varphi }_1,\dots ,{\varphi }_n,\Gamma \to \Delta ,a:\varphi }{\Gamma \to \Delta ,a::({\varphi }_1,\dots ,{\varphi }_n/\varphi )}$$

$$\frac{\Gamma \to \Delta ,{\varphi }_1\cdots \Gamma \to \Delta ,{\varphi }_{n}a:\varphi ,\Gamma \to \Delta }{a::({\varphi }_1,\dots ,{\varphi }_n/\varphi ),\Gamma \to \Delta }$$

$$⊢\Gamma \to \Delta ,$$

Full text

Keywords: Time-stamped claim logic, labelled deduction, Gentzen calculus, evidence logic, cyber security.

1 Introduction

The main objective of this paper is to define a logic for reasoning about distributed time-stamped claims. Such a logic is interesting for theoretical reasons, i.e., as a logic per se, but also because it has a number of practical applications, most notably the ability to reason about the attribution of cyber-attacks.

When reasoning about a cyber-attack, a digital forensics analyst typically collects a huge amount of pieces of evidence from different sources. Some of the pieces of evidence may be contradictory and the analyst might consider some sources to be more trustworthy than others. Inferring conclusions from such evidence thus requires particular care and time. A similar problem is faced by historians when they are trying to date particular historic events.

The Time-Stamped Claim Logic that we introduce in this paper provides the forensics analyst with a sound and complete means to reduce the size of the collected set of evidence and remove inconsistencies, i.e., the logic ensures that the result is consistent with respect to the trust relations that the analyst considers to hold. More specifically, the Time-Stamped Claim Logic is a monotonic propositional logic whose language contains assertions of different kinds: labeled assertions to expressing statements of agents about time-stamped claims and relational assertions indexed by propositional symbols that are used to relate agents. In particular, a trust relation with respect to each propositional subject is defined between agents.

We formalize a Gentzen calculus for our logic, which allows one to infer a time-stamped claim whenever (i) there is an agent that states the claim and (ii) each agent that is more trustworthy with respect to the subject does not state the opposite claim. We define a modal and many-valued semantics for our logic, and prove that the calculus is sound and complete with respect to this semantics. In order to show how Time-Stamped Claim Logic can be used in practice, we consider, as a proof of concept, a concrete cyber-attribution case study, inspired by the Ukraine Power Grid Attack that occurred in December 2015.

We proceed as follows. In Section 2, we define the language of Time-Stamped Claim Logic. In Section 3, we formalize a Gentzen calculus for the logic together with a running example. In Section 4, we introduce the semantics, and we then prove the soundness and the completeness of the calculus in Section 5 and Section 6, respectively. In Section 7, we apply Time-Stamped Claim Logic to a realistic case study taken from the cyber-security area. We discuss the most relevant related work in Section 8 and provide some concluding remarks and ideas for future work in Section 9.

2 The Language of Time-Stamped Claim Logic

In this section, we introduce the language of the Time-Stamped Claim Logic.

Definition 2.1

Let $P$ be a non-empty set of propositional symbols and assume fixed non-empty pairwise disjoint sets $X_{A}$ and $X_{T}$ of variables, which represent agents names and time points, respectively. The set $K_{P}$ of time-stamped propositional claims is defined as

[TABLE]

$\blacksquare$**

Definition 2.2

The language $L_{P}$ of assertions is defined as follows:

• •

$K_{P}\subseteq L_{P}$;

• •

$t_{1}\cong t_{2}\in L_{P}$* whenever $t_{1},t_{2}\in X_{T}$;*

• •

$a_{1}\mathbin{\trianglelefteq}_{p}a_{2}\in L_{P}$* whenever $a_{1},a_{2}\in X_{A}$ and $p\in X_{P}$;*

• •

$\forall x.\,x\mathbin{\trianglelefteq}_{p}a$* whenever $a\in X_{A}$ and $p\in P$;*

• •

$a:\phi\in L_{P}$* whenever $a\in X_{A}$ and $\phi\in K_{P}$;*

• •

$a:\mathop{\boxdot}\phi\in L_{P}$* whenever $a\in X_{A}$ and $\phi\in K_{P}$;*

• •

$a::(\phi_{1},\,\dots,\,\phi_{n}/\phi)$* whenever $a\in X_{A}$ and $\phi,\phi_{1},\dots,\phi_{n}\in K_{P}$. $\blacksquare$*

Let us briefly discuss the intuitive meaning of these assertions:

• •

$t_{1}\cong t_{2}\in L_{P}$ establishes that $t_{1}$ and $t_{2}$ are equivalent time points.

• •

$a_{1}\mathbin{\trianglelefteq}_{p}a_{2}$ establishes that agent $a_{2}$ is more trustworthy with respect to $p$ than agent $a_{1}$.

• •

$\forall x.\,x\mathbin{\trianglelefteq}_{p}a$ establishes that $a$ is the most trustworthy agent with respect to statements about $p$.

• •

$a:\phi$ establishes that $a$ states $\phi$.

• •

$a:\mathop{\boxdot}t\cdot p$ establishes that there are no agents more trustworthy with respect to $p$ than $a$ that state ${-}(t\cdot p)$. That is, each agent more trustworthy with respect to $p$ than $a$ does not claim ${-}(t\cdot p)$. Similarly, for $a:\mathop{\boxdot}{-}(t\cdot p)$.

• •

$a::(\phi_{1},\,\dots,\,\phi_{n}/\phi)$ establishes that $a$ states $\phi$ conditional to statements $\phi_{1},\dots,\phi_{n}$.

Given the relation of $\phi$ with respect to the other statements we will refer to $a::(\phi_{1},\,\dots,\,\phi_{n}/\phi)$ as a derived evidence. We will instead refer to the previous two assertions $a:\phi$ and $a:\mathop{\boxdot}\phi$ simply as evidence.

Let us now illustrate how our logic is used by means of a running example.

Example 2.3

Let us suppose that we want to model a crime situation C that possibly occurred at time $t$ in which there is a potential culprit J and some sources $a_{1}$, $a_{2}$ and $a_{3}$ providing statements on the case. Let us further suppose that for the source $a_{1}$ a person is a culprit provided that person was at the scene of the crime, is capable of committing the crime and has a motive. This can be expressed by the assertion

[TABLE]

over $P=\{\textrm{inplace}^{J}_{C},\textrm{capable}^{J}_{C},\textrm{motive}^{J}_{C},\textrm{culprit}^{J}_{C}\}$. Moreover, we can write the assertion

[TABLE]

to express that $a_{3}$ is a source recognized to be the most trustworthy with respect to knowing the motive of the potential culprit $J$. Furthermore, the assumptions

• •

$a_{1}$ is less trustworthy than $a_{2}$ with respect to knowing the motive of $J$ to have committed the crime $C$,

• •

$a_{1}$ claims that $J$ does not have a motive to have committed the crime $C$ at time $t$,

• •

$a_{2}$ claims that $J$ has a motive to have committed the crime $C$ at time $t$

can be expressed in the Time-Stamped Claim Logic by means of the assertions

• •

$a_{1}\mathbin{\trianglelefteq}_{\textrm{motive}^{\textrm{J}}_{\textrm{C}}}a_{2}$,

• •

$a_{1}:{-}(t\cdot\textrm{motive}^{J}_{C})$ and

• •

$a_{2}:t\cdot\textrm{motive}^{J}_{C}$,

respectively. Hence, if $a_{3}$ does not have an opinion about whether or not $J$ has a motive to have committed the crime $C$ at time $t$, then

• •

$a_{3}:\mathop{\boxdot}\,t\cdot\textrm{motive}^{J}_{C}$ and $a_{3}:\mathop{\boxdot}{-}(t\cdot\textrm{motive}^{J}_{C})$ should hold,

• •

$a_{2}:\mathop{\boxdot}\,t\cdot\textrm{motive}^{J}_{C}$ should hold and $a_{2}:\mathop{\boxdot}{-}(t\cdot\textrm{motive}^{J}_{C})$ should not hold, and

• •

both $a_{1}:\mathop{\boxdot}\,t\cdot\textrm{motive}^{J}_{C}$ and $a_{1}:\mathop{\boxdot}{-}(t\cdot\textrm{motive}^{J}_{C})$ should not hold. $\blacksquare$

Before we introduce the calculus of our logic, which will allow us to draw conclusions from assertions like the ones in Example 2.3, let us define some useful notation. In the following, we will write

[TABLE]

to denote the map that assigns to each set of assertions the set of elements of $X_{A}$ that occur in it; mutatis mutandis for ${\textrm{var}}_{T}:\wp L_{P}\to\wp X_{T}$ and ${\textrm{var}}_{P}:\wp L_{P}\to\wp P$. We may confuse a singleton set with its unique element. Given $P^{\prime}\subseteq P$, $X^{\prime}_{A}\subseteq X_{A}$ and $X^{\prime}_{T}\subseteq X_{T}$, we write $L_{P^{\prime}}^{X^{\prime}_{A},X^{\prime}_{T}}$ to denote the subset of $L_{P}$ including all the assertions using only symbols in $P^{\prime}$ and variables in $X^{\prime}_{A}$ and $X^{\prime}_{T}$.

3 The Calculus of Time-Stamped Claim Logic

Let us begin by recalling what is a sequent and an inference rule. Let $P$ be a non-empty set of propositional symbols. A sequent over $P$ is a pair $(\Gamma,\Delta)$ and is denoted by

[TABLE]

where $\Gamma$ and $\Delta$ are finite multisets of formulas in $L_{P}$. An inference rule over $P$ is of the form

[TABLE]

where $F$ is a set of fresh variables with at most a variable in $X_{A}$.

For convenience, below, we will sometimes write

[TABLE]

to mean $t\cdot p$ and vice-versa, in order to avoid the replication of rules NS, NK, SCR, SCL, SKR, and SKL.

Definition 3.1

The calculus over $P$ is composed by the following inference rules:

• •

Axiom* (Ax):*

[TABLE]

where $\beta$ is of the form $a:\phi$, $t_{1}\cong t_{2}$ or $a_{1}\mathbin{\trianglelefteq}_{p}a_{2}$

• •

Cut* (Cut):*

[TABLE]

where $\beta$ is of the form $a:\phi$, $t_{1}\cong t_{2}$ or $a_{1}\mathbin{\trianglelefteq}_{p}a_{2}$

• •

Reflexivity of $\cong$* (ER):*

[TABLE]

• •

Symmetry of $\cong$* (ES):*

[TABLE]

• •

Transitivity of $\cong$* (ET):*

[TABLE]

• •

Congruence of $\cong$* (EC):*

[TABLE]

where $[a:\phi]^{t_{1}}_{t_{2}}$ is a formula obtained from $a:\phi$ by replacing $t_{1}$ by $t_{2}$

• •

Agent preference transitivity* (AT):*

[TABLE]

• •

Agent preference reflexivity* (AR):*

[TABLE]

• •

Agent preference congruence* (AC):*

[TABLE]

where $[a:\phi]^{a_{1}}_{a_{2}}$ is a formula obtained from $a:\phi$ by replacing $a_{1}$ by $a_{2}$

• •

Agent preference maximum on the right* (AMR):*

[TABLE]

• •

Agent preference maximum on the left* (AML):*

[TABLE]

• •

Negative statement* (NS):*

[TABLE]

• •

Negative knowledge* (NK):*

[TABLE]

• •

Statement propagation over time* (SP):*

[TABLE]

• •

Knowledge propagation time* (KP):*

[TABLE]

• •

Statement confirmation on the right* (SCR):*

[TABLE]

• •

Statement confirmation on the left* (SCL):*

[TABLE]

• •

Extracting knowledge from statement on the right* (SKR):*

[TABLE]

• •

Extracting knowledge on the left* (KL):*

[TABLE]

• •

Extracting knowledge from statement on the left* (SKL):*

[TABLE]

• •

Conditional reasoning on the right* (CR1):*

[TABLE]

• •

Conditional reasoning on the left* (CR2):*

[TABLE]

Most of the rules are self-explanatory, so let us briefly explain only some of them.

The rule $(\textrm{NS})$ states that the claims of an agent are not contradictory, in the sense that an agent cannot claim $\phi$ and $-\phi$. Observe that we do not have the right counterpart of NS that introduces $-$ in the right hand side. This is because the logic is not bivalent since there is a third truth-value $\frac{1}{2}$. Therefore, $-$ is not a classical negation.

The rule $(\textrm{SP})$ states that in order to conclude that an agent does not state a certain claim at a particular time it is enough to show that he states the opposite claim at a different time.

The rule $(\textrm{SCR})$ states that it is possible to conclude $a:\mathop{\boxdot}\phi$ when there is no agent more trustworthy than $a$ that claims $-\phi$.

On the other hand, rule $(\textrm{SKR})$ states that in order to conclude $\phi$, it is enough to show that there is an agent stating $\phi$ that is not contradicted by a more trustworthy agent and that each agent stating the opposite claim is contradicted by a more trustworthy agent.

We say that a sequent $\Gamma\to\Delta$ is a theorem, written

[TABLE]

if there is a finite sequence of sequents

[TABLE]

such that:

• •

$\Gamma_{1}\to\Delta_{1}$ is $\Gamma\to\Delta$,

• •

for each $i$,

• –

either $\Gamma_{i}\to\Delta_{i}$ is the conclusion of a rule without premises,

• –

or $\Gamma_{i}\to\Delta_{i}$ is the conclusion of a rule where each premise is a sequent $\Gamma_{j}\to\Delta_{j}$ in the sequence with $j>i$.

In this case, the sequence is said to be a derivation for $\Gamma\to\Delta$ and $\Gamma\to\Delta$ is said to be derivable.

The notion of derivable can be brought to the realm of formulas. For $\Psi\cup\{\alpha\}\subseteq L_{P}$, we say that $\alpha$ is derivable from $\Psi$, denoted by

[TABLE]

whenever there is a finite set $\Gamma\subseteq\Psi$ such that $\vdash\Gamma\to\alpha$.

For the sake of readability, in the derivations that we give below we underline the principal formula(s) of the rule/axiom that is applied.

Example 3.2

Let us return to the crime situation described in Example 2.3. Let $P$ be the set composed by the following propositional symbols: $\textrm{inplace}^{J}_{C}$, $\textrm{capable}^{J}_{C}$, $\textrm{motive}^{J}_{C}$, $\textrm{culprit}^{J}_{C}$, $\textrm{divergence}^{J}_{C}$, $\textrm{poor}^{J}$, $\textrm{friend}^{J}$, $\textrm{guilty}^{J}_{C^{\prime}}$ and $\textrm{similar}^{C}_{C^{\prime}}.$ Let $\Gamma$ be the set containing the assertions

• •

$\psi_{1}=a_{1}::(t\cdot\textrm{inplace}^{J}_{C},t\cdot\textrm{capable}^{J}_{C}\;/\;t\cdot\textrm{culprit}^{J}_{C})$

• •

$\psi_{2}=a_{2}::(t\cdot\textrm{motive}^{J}_{C}\;/\;t\cdot\textrm{culprit}^{J}_{C})$

• •

$\psi_{3}=a_{3}::({-}(t\cdot\textrm{capable}^{J}_{C}),t\cdot\textrm{poor}^{J}\;/\;{-}(t\cdot\textrm{culprit}^{J}_{C}))$

• •

$\psi_{4}=a_{4}::(t\cdot\textrm{inplace}^{J}_{C},t\cdot\textrm{friend}^{J}\;/\;{-}(t\cdot\textrm{culprit}^{J}_{C}))$

• •

$\psi_{5}=a_{5}::(t^{\prime}\cdot\textrm{guilty}^{J}_{C^{\prime}},t\cdot\textrm{similar}^{C}_{C^{\prime}}\;/\;t\cdot\textrm{capable}^{J}_{C})$

• •

$\psi_{6}=a_{6}::(t^{\prime}\cdot\textrm{guilty}^{J}_{C^{\prime}},{-}(t\cdot\textrm{similar}^{C}_{C^{\prime}})\;/\;{-}(t\cdot\textrm{capable}^{J}_{C}))$

• •

$\psi_{7}=a_{7}::(t\cdot\textrm{divergence}^{J}_{C}\;/\;t\cdot\textrm{motive}^{J}_{C})$

• •

$\psi_{8}=a_{8}:t\cdot\textrm{divergence}^{J}_{C}$

• •

$\delta_{1}=\forall x.\,x\mathbin{\trianglelefteq}_{\textrm{motive}^{\textrm{J}}_{\textrm{C}}}a_{7}$

• •

$\delta_{2}=\forall x.\,x\mathbin{\trianglelefteq}_{\textrm{divergence}^{\textrm{J}}_{\textrm{C}}}a_{8}$

and let $\Delta$ be the singleton set with the assertion $a_{2}:t\cdot\textrm{culprit}^{J}_{C}$. The derivation in Figure 1 establishes that $\Gamma\to\Delta$ is derivable. The subderivation of $(*)$ is in Figure 2.

$\blacksquare$

We will show the use of Time-Stamped Claim Logic with a more complex case study in Section 7.

4 The Semantics of Time-Stamped Claim Logic

In this section, we define the semantics of the Time-Stamped Claim Logic. In the following sections, we will then prove the soundness and completeness of the sequent calculus with respect to this semantics. We start by introducing the notion of interpretation structure, which has a modal and many-valued flavour.

Definition 4.1

An interpretation structure over a non-empty set $P$ of propositional symbols is a tuple

[TABLE]

such that

• •

$D_{A}$* and $D_{T}$ are non-empty sets,*

• •

$\cong^{I}$* is a reflexive, symmetric and transitive relation over $D_{T}$,*

• •

$\mathbin{\trianglelefteq}_{p}^{I}$* is a transitive and reflexive binary relation over $D_{A}$ for each $p\in P$,*

• •

$V:P\times D_{A}\times D_{T}\to\{0,1,\frac{1}{2}\}$* such that for every $p\in P$, $d\in D_{A}$ and $n,n^{\prime}\in D_{T}$,*

• –

if $V(p,d,n)=1$, then $V(p,d,m)=0$ for every $m\in D_{T}$ such that $m\not\cong^{I}n$,

• –

$V(p,d,n)=V(p,d,n^{\prime})$* whenever $n\cong^{I}n^{\prime}$,*

• –

$V(p,d,n)=V(p,d^{\prime},n)$* whenever $d\mathbin{\trianglelefteq}_{p}^{I}d^{\prime}$ and $d^{\prime}\mathbin{\trianglelefteq}_{p}^{I}d$.*

In an interpretation structure, $V(p,d,n)=1$ means that agent $d$ claims that $p$ occurred at time $n$, $V(p,d,n)=0$ means that agent $d$ claims that $p$ does not occur at time $n$ and $V(p,d,n)=\frac{1}{2}$ means that agent $d$ does not have an opinion about the occurrence of $p$ at time $n$.

An assignment $\rho$ over $I$ is a pair $(\rho_{A},\rho_{T})$ such that $\rho_{A}:X_{A}\to D_{A}$ and $\rho_{T}:X_{T}\to D_{T}$ are maps. Moreover, we say that assignments $\rho$ and $\rho^{\prime}$ are equivalent up to $b\in X_{A}$, written

[TABLE]

whenever $\rho^{\prime}_{T}=\rho_{T}$ and $\rho^{\prime}_{A}(a)=\rho_{A}(a)$ for every $a\in X_{A}\setminus\{b\}$.

Given an interpretation structure $I$ over $P$ and an assignment $\rho$ over $I$, satisfaction of an assertion $\alpha$ by $I$ and $\rho$, denoted by

[TABLE]

is defined as follows

• •

$I\rho\Vdash t_{1}\cong t_{2}$* whenever $\rho_{T}(t_{1}){\cong}^{I}\rho_{T}(t_{2})$,*

• •

$I\rho\Vdash a_{1}\mathbin{\trianglelefteq}_{p}a_{2}$* whenever $\rho_{A}(a_{1})\mathbin{\trianglelefteq}_{p}^{I}\,\rho_{A}(a_{2})$,*

• •

$I\rho\Vdash\forall x.\,x\mathbin{\trianglelefteq}_{p}a$* whenever $d\mathbin{\trianglelefteq}_{p}^{I}\rho_{A}(a)$ for every $d\in D_{A}$,*

• •

$I\rho\Vdash a:\phi$* whenever $V(p,\rho_{A}(a),\rho_{T}(t))=\begin{cases}1&\text{if }\phi\text{ is }t\cdot p\\ 0&\text{if }\phi\text{ is }{-}(t\cdot p)\,,\end{cases}$*

• •

$I\rho\Vdash a:\mathop{\boxdot}\phi$* whenever, for each assignment $\rho^{\prime}$ and $b\in X_{A}$ such that $\rho^{\prime}\equiv^{A}_{b}\rho$, if $I\rho^{\prime}\Vdash a\mathbin{\trianglelefteq}_{{\textrm{var}}_{P}(\phi)}b$ then $I\rho^{\prime}\not\Vdash b:{-}\phi$,*

• •

$I\rho\Vdash\phi$* whenever*

• –

for each assignment $\rho^{\prime}$ and $b\in X_{A}$ with $\rho^{\prime}\equiv^{A}_{b}\rho$, if $I\rho^{\prime}\Vdash b:{-}\phi$ then $I\rho^{\prime}\not\Vdash b:\mathop{\boxdot}{-}\phi$,

• –

there are assignment $\rho^{\prime}$ and $a\in X_{A}$ with $\rho^{\prime}\equiv^{A}_{a}\rho$, $I\rho^{\prime}\Vdash a:\phi$ and $I\rho^{\prime}\Vdash a:\mathop{\boxdot}\phi$,

• •

$I\rho\Vdash a::(\phi_{1},\,\dots,\,\phi_{n}/\phi)$* whenever if $I\rho\Vdash\phi_{i}$ for $i=1,\dots,n$ then $I\rho\Vdash a:\phi$. $\blacksquare$*

Note that in the definition of satisfaction the truth-value $\frac{1}{2}$ does not play an explicit role. However, it allows the following to be possible:

[TABLE]

To simplify the presentation, given a set $\Gamma\subseteq L_{P}$, we will write

[TABLE]

whenever $I\rho\Vdash\gamma$ for each $\gamma\in\Gamma$.

Definition 4.2

Given $\Psi\subseteq L_{P}$ and $\alpha\in L_{P}$, we say that $\Psi$ entails $\alpha$, denoted by

[TABLE]

whenever for every interpretation structure $I$ and assignment $\rho$ over $I$ we have

[TABLE]

$\blacksquare$**

5 Soundness

In this section, we prove that the theorems derived using the calculus of the Time-Stamped Claim Logic introduced in Section 3 are valid according to the semantics introduced in Section 4. We start by providing some relevant semantic notions related to sequents.

Definition 5.1

We say that an interpretation structure $I$ and an assignment $\rho$ satisfy a sequent $\Gamma\to\Delta$, denoted by

[TABLE]

whenever $I\rho\Vdash\delta$ for some $\delta\in\Delta$ if $I\rho\Vdash\Gamma$. We say that a sequent $\Gamma\to\Delta$ is valid, denoted by

[TABLE]

whenever it is satisfied by every interpretation structure $I$ and assignment $\rho$. We say that $I$ and $\rho$ satisfy a rule with a fresh variable $b$,

[TABLE]

whenever $I\rho\Vdash\Gamma\to\Delta$ if $I\rho^{\prime}\Vdash\Gamma_{i}\to\Delta_{i}$ for $i=1,\dots,n$ for every $\rho^{\prime}$ such that $\rho^{\prime}\equiv^{A}_{b}\rho$. We say that $I$ and $\rho$ satisfy a rule without fresh variables,

[TABLE]

whenever $I\rho\Vdash\Gamma\to\Delta$ if $I\rho\Vdash\Gamma_{i}\to\Delta_{i}$ for $i=1,\dots,n$. Finally, we say that a rule is sound whenever it is satisfied by every interpretation structure and assignment. $\blacksquare$

The proof of the following result is in Appendix A.

Proposition 5.2

The rules of the sequent calculus are sound.

The soundness of the rules can be used to show the soundness of deductive consequences.

Proposition 5.3

Let $\Gamma\to\Delta$ be a sequent over $P$. Then $\vDash\Gamma\to\Delta$ whenever $\vdash\Gamma\to\Delta$.

• Proof: The proof is by induction on the length of a derivation $\Gamma_{1}\to\Delta_{1}\cdots\Gamma_{n}\to\Delta_{n}$ of $\Gamma\to\Delta$. The base case follows straightforwardly by Proposition 5.2.

For the step case, assume that $\Gamma_{1}\to\Delta_{1}$ follows from rule $u$ of the calculus applied to sequents $\Gamma_{i_{j}}\to\Delta_{i_{j}}$ for $j=1,\dots,k$. Then $\vdash\Gamma_{i_{j}}\to\Delta_{i_{j}}$ for $j=1,\dots,k$. Hence, by the induction hypothesis, $\vDash\Gamma_{i_{j}}\to\Delta_{i_{j}}$ for $j=1,\dots,k$. Let $I$ be an interpretation structure, $\rho$ an assignment and $\rho^{\prime}$ an assignment equivalent modulo the fresh variables of $u$ to $\rho$. Then $I\rho^{\prime}\Vdash\Gamma_{i_{j}}\to\Delta_{i_{j}}$ for $j=1,\dots,k$ since $\vDash\Gamma_{i_{j}}\to\Delta_{i_{j}}$ for $j=1,\dots,k$. Taking into account that $u$ is sound, by Proposition 5.2, we conclude that $I\rho\Vdash\Gamma_{1}\to\Delta_{1}$. QED

Capitalizing on the soundness at the sequent level, we can establish soundness at the level of assertions.

Proposition 5.4

Let $\Psi\subseteq L_{P}$ and $\alpha\in L_{P}$. Then $\Psi\vDash\alpha$ whenever $\Psi\vdash\alpha$.

• Proof: Assume that $\Psi\vdash\alpha$. Then there is a finite set $\Gamma\subseteq\Psi$ such that $\vdash\Gamma\to\alpha$. Thus, by Proposition 5.3, $\vDash\Gamma\to\alpha$. Let $I$ be an interpretation structure and $\rho$ an assignment such that $I\rho\Vdash\Psi$. Therefore, $I\rho\Vdash\Gamma$ and so $I\rho\Vdash\alpha$. QED

6 Completeness

In this section, we show that the Time-Stamped Claim Logic is complete using a Hintikka style technique. We consider Hintikka pairs instead of just Hintikka sets since the logic does not have a classical negation over all assertions.

Definition 6.1

A Hintikka pair over $P^{\prime}\subseteq P$, $X^{\prime}_{A}\subseteq X_{A}$ and $X^{\prime}_{T}\subseteq X_{T}$ is a pair $(\Psi_{L},\Psi_{R})$ of sets of assertions in $L_{P^{\prime}}^{X^{\prime}_{A},X^{\prime}_{T}}$ such that:

• •

either $\beta\notin\Psi_{L}$ or $\beta\notin\Psi_{R}$ for each $\beta\in L_{P^{\prime}}^{X^{\prime}_{A},X^{\prime}_{T}}$ of the form $a:\phi$, $t_{1}\cong t_{2}$ and $a_{1}\mathbin{\trianglelefteq}_{p}a_{2}$,

• •

either $\beta\in\Psi_{L}$ or $\beta\in\Psi_{R}$ for each $\beta\in L_{P^{\prime}}^{X^{\prime}_{A},X^{\prime}_{T}}$ of the form $a:\phi$, $t_{1}\cong t_{2}$ and $a_{1}\mathbin{\trianglelefteq}_{p}a_{2}$,

• •

$t\cong t\notin\Psi_{R}$* and similarly for $\mathbin{\trianglelefteq}_{p}$,*

• •

if $t_{1}\cong t_{2}\in\Psi_{L}$ then $t_{2}\cong t_{1}\notin\Psi_{R}$,

• •

if $t_{1}\cong t_{2},t_{2}\cong t_{3}\in\Psi_{L}$ then $t_{1}\cong t_{3}\notin\Psi_{R}$ and similarly for $\mathbin{\trianglelefteq}_{p}$,

• •

if $t_{1}\cong t_{2},[a:\phi]^{t_{1}}_{t_{2}}\in\Psi_{L}$ then $a:\phi\notin\Psi_{R}$,

• •

if $a_{1}\mathbin{\trianglelefteq}_{p}a_{2},a_{2}\mathbin{\trianglelefteq}_{p}a_{1},[a:\phi]^{a_{1}}_{a_{2}}\in\Psi_{L}$ then $a:\phi\notin\Psi_{R}$,

• •

if $\forall x.\,x\mathbin{\trianglelefteq}_{p}a\in\Psi_{R}$ then there is $a^{\prime}\in X^{\prime}_{A}$ such that $a^{\prime}\mathbin{\trianglelefteq}_{p}a\in\Psi_{R}$,

• •

if $\forall x.\,x\mathbin{\trianglelefteq}_{p}a\in\Psi_{L}$ then $a_{1}\mathbin{\trianglelefteq}_{p}a\in\Psi_{L}$ for each $a_{1}\in X^{\prime}_{A}$,

• •

if $a:\phi\in\Psi_{L}$ then $a:{-}\phi\in\Psi_{R}$,

• •

if $t_{1}\cong t_{2},a:{-}(t_{1}\cdot p)\in\Psi_{R}$ then $a:t_{2}\cdot p\in\Psi_{R}$,

• •

if $a:\mathop{\boxdot}\phi\in\Psi_{R}$ then there is $a^{\prime}\in X^{\prime}_{A}$ such that $a\mathbin{\trianglelefteq}_{{\textrm{var}}(\phi)}a^{\prime},a^{\prime}:{-}\phi\in\Psi_{L}$,

• •

if $a:\mathop{\boxdot}\phi\in\Psi_{L}$ then, for each $a^{\prime}\in X^{\prime}_{A}$ either $a\mathbin{\trianglelefteq}_{{\textrm{var}}(\phi)}a^{\prime}\in\Psi_{R}$ or $a^{\prime}:{-}\phi\in\Psi_{R}$,

• •

if $\phi\in\Psi_{R}$ then either there exists $a^{\prime}\in X^{\prime}_{A}$ such that $a^{\prime}:{-}\phi,a^{\prime}:\mathop{\boxdot}{-}\phi\in\Psi_{L}$ or for each $a\in X^{\prime}_{A}$ either $a:\phi\in\Psi_{R}$ or $a:\mathop{\boxdot}\phi\in\Psi_{R}$,

• •

if $\phi\in\Psi_{L}$ then there is $a^{\prime}\in X^{\prime}_{A}$ such that $a^{\prime}:\phi,a^{\prime}:\mathop{\boxdot}\phi\in\Psi_{L}$ and for each $a\in X^{\prime}_{A}$ either $a:{-}\phi\in\Psi_{R}$ or $a:\mathop{\boxdot}{-}\phi\in\Psi_{R}$,

• •

if $a::(\phi_{1},\dots,\phi_{n}/\phi)\in\Psi_{R}$ then if $\phi_{1},\dots,\phi_{n}\in\Psi_{L}$ then $a:\phi\in\Psi_{R}$,

• •

if $a::(\phi_{1},\dots,\phi_{n}/\phi)\in\Psi_{L}$ then either $\phi_{i}\in\Psi_{R}$ for some $i=1,\dots,n$ or $a:\phi\in\Psi_{L}$. $\blacksquare$

We now show that for each Hintikka pair there are an interpretation structure and an assignment satisfying all the assertions in the first component of the pair and not satisfying each assertion in the second component.

The proof of the next result can be found in Appendix A.

Proposition 6.2

Let $H=(\Psi_{L},\Psi_{R})$ be a Hintikka pair over $P^{\prime}$, $X^{\prime}_{A}$ and $X^{\prime}_{T}$. Then there are an interpretation structure $I_{H}$ over $P^{\prime}$ and an assignment $\rho$ over $I_{H}$ such that $I_{H}\rho\Vdash\psi$ for each $\psi\in\Psi_{L}$ and $I_{H}\rho\not\Vdash\psi$ for each $\psi\in\Psi_{R}$.

The main objective now is to show that if a sequent is not derivable then there is an interpretation structure that falsifies it. For this purpose, we must introduce the concept of (deductive) expansion of a sequent.

Definition 6.3

An expansion of a sequent $\Gamma\to\Delta$ is a (finite or infinite) sequence of sequents $\Gamma_{1}\to\Delta_{1}\ \cdots$ such that:

• •

$\Gamma_{1}\to\Delta_{1}$* is $\Gamma\to\Delta$;*

• •

for each $i\neq 1$, $\Gamma_{i}\to\Delta_{i}$ is a premise of a rule with conclusion $\Gamma_{j}\to\Delta_{j}$ with $j<i$ and all the other premises of the rule occur in the sequence.

$\blacksquare$**

Observe that every derivation is an expansion but not vice versa. From an expansion fulfilling conditions described below, we will define an interpretation structure that falsifies the first sequent in the expansion. We need first to introduce the concept of branch.

Definition 6.4

A branch of the expansion $\Gamma_{1}\to\Delta_{1}\ \cdots$ starting at sequent $\Gamma_{i}\to\Delta_{i}$ is a subsequence $\Gamma_{i_{1}}\to\Delta_{i_{1}}\ \cdots$ of the expansion such that:

• •

$\Gamma_{i_{1}}\to\Delta_{i_{1}}$* is $\Gamma_{i}\to\Delta_{i}$,*

• •

for each $j>1$, $\Gamma_{i_{j}}\to\Delta_{i_{j}}$ is a premise of the rule used in the expansion to justify $\Gamma_{i_{j-1}}\to\Delta_{i_{j-1}}$ (the conclusion of the rule),

• •

for each $j\geq 1$ if $\Gamma_{i_{j}}\to\Delta_{i_{j}}$ is the conclusion of a rule in the expansion then there $k>j$ such $\Gamma_{i_{k}}\to\Delta_{i_{k}}$ is a premise of the rule in the expansion.

For simplicity, we present a branch as a sequence $\Gamma^{\prime}_{1}\to\Delta^{\prime}_{1}\ \Gamma^{\prime}_{2}\to\Delta^{\prime}_{2}\ \cdots$ instead of using the numbering of each sequent of the branch in the expansion. When $\Gamma^{\prime}_{1}\to\Delta^{\prime}_{1}$ is $\Gamma_{1}\to\Delta_{1}$ we say that the branch is rooted. $\blacksquare$

Definition 6.5

We say that a finite branch $\Gamma^{\prime}_{1}\to\Delta^{\prime}_{1}\cdots\Gamma^{\prime}_{n}\to\Delta^{\prime}_{n}$ of an expansion $\Gamma_{1}\to\Delta_{1}\ \cdots$ is analytical whenever it is possible to inductively define the families of sets

[TABLE]

such that

[TABLE]

and for $j=2,\dots,n$,

[TABLE]

and if $\Gamma^{\prime}_{j}\to\Delta^{\prime}_{j}$ is a premise of a rule $u$, then

either there is a side formula in the left hand side of a premise of $u$ in the expansion which does not occur in $(i_{L})_{j-1}$ not involving fresh variables or there is a side formula in the right hand side of a premise of $u$ in the expansion which does not occur in $(i_{R})_{j-1}$ not involving fresh variables; 2. 2.

the non fresh variables of $u$ in ${\textrm{var}}_{A}((\Gamma^{\prime}_{j}\setminus\Gamma^{\prime}_{j-1})\cup(\Delta^{\prime}_{j}\setminus\Delta^{\prime}_{j-1}))$ are in ${\textrm{var}}_{A}((i_{L})_{j-1}\cup(i_{R})_{j-1})$ and similarly for ${\textrm{var}}_{T}$ and ${\textrm{var}}_{P}$; 3. 3.

the fresh variables of $u$ in ${\textrm{var}}_{A}((\Gamma^{\prime}_{j}\setminus\Gamma^{\prime}_{j-1})\cup(\Delta^{\prime}_{j}\setminus\Delta^{\prime}_{j-1}))$ are not in ${\textrm{var}}_{A}(\Gamma^{\prime}_{j-1}\cup\Delta^{\prime}_{j-1})$ and similarly for ${\textrm{var}}_{T}$ and ${\textrm{var}}_{P}$.

An analytical branch $\Gamma^{\prime}_{1}\to\Delta^{\prime}_{1}\cdots\Gamma^{\prime}_{n}\to\Delta^{\prime}_{n}$ is exhausted whenever each branch that results from applying a rule to $\Gamma^{\prime}_{n}\to\Delta^{\prime}_{n}$ is not analytical in the augmented expansion. An analytical exhausted branch is closed whenever the last sequent is the conclusion of a rule without premises. Otherwise, it is said to be open. An expansion is open when it has an open analytical exhausted branch. $\blacksquare$

The proof of the next result is in Appendix A.

Proposition 6.6

Let $\Gamma^{\prime}_{1}\to\Delta^{\prime}_{1}\cdots\Gamma^{\prime}_{n}\to\Delta^{\prime}_{n}$ be a rooted open analytical exhausted branch of an expansion $\Gamma_{1}\to\Delta_{1}\ \cdots$. Then

[TABLE]

is an Hintikka pair over ${\textrm{var}}_{P}(\Gamma^{\prime}_{n}\cup\Delta^{\prime}_{n})$, ${\textrm{var}}_{A}(\Gamma^{\prime}_{n}\cup\Delta^{\prime}_{n})$ and ${\textrm{var}}_{T}(\Gamma^{\prime}_{n}\cup\Delta^{\prime}_{n})$.

Proposition 6.7

If a sequent is not a theorem then it has an expansion with a rooted open analytical exhausted branch.

• Proof: It is straightforward to see that every sequent has an expansion where all rooted branches are analytical and exhausted. Furthermore, if all the rooted branches in that expansion are not open then the expansion is a derivation. QED

Capitalizing on the previous results in this section, we are able to establish the completeness result at the level of sequents.

Proposition 6.8

If a sequent is valid then it is a theorem.

• Proof: Assume that the sequent $\Gamma\to\Delta$ is not a theorem. Then, by Proposition 6.7, it has an expansion with a rooted open analytical exhausted branch. So, by Proposition 6.6, there is an Hintikka pair $H=(\Psi_{L},\Psi_{R})$ over ${\textrm{var}}_{P}(\Gamma^{\prime}_{n}\cup\Delta^{\prime}_{n})$, ${\textrm{var}}_{A}(\Gamma^{\prime}_{n}\cup\Delta^{\prime}_{n})$ and ${\textrm{var}}_{T}(\Gamma^{\prime}_{n}\cup\Delta^{\prime}_{n})$ such that $\Gamma\subseteq\Psi_{L}$ and $\Delta\subseteq\Psi_{R}$. Hence, by Proposition 6.2, there are an interpretation structure $I_{H}$ over ${\textrm{var}}_{P}(\Gamma^{\prime}_{n}\cup\Delta^{\prime}_{n})$ and an assignment $\rho$ over $I_{H}$ such that $I_{H}\rho\Vdash\Gamma$ and $I_{H}\rho\not\Vdash\delta$ for each $\delta\in\Delta$. Let $I$ be an interpretation structure over $P$ such that $I_{H}$ is the reduct of $I$ to ${\textrm{var}}_{P}(\Gamma^{\prime}_{n}\cup\Delta^{\prime}_{n})$. Observe that $\rho$ is also an assignment over $I$. Hence, $I\rho\Vdash\Gamma$ and $I\rho\not\Vdash\delta$ for each $\delta\in\Delta$. Thus, $I\rho\not\Vdash\Gamma\to\Delta$ and so $\Gamma\to\Delta$ is not valid. QED

Finally, we can show that the Time-Stamped Claim Logic is complete.

Proposition 6.9

Let $\Gamma\subseteq L_{P}$ be a finite set and $\alpha\in L_{P}$. Then $\Gamma\vdash\alpha$ whenever $\Gamma\vDash\alpha$.

• Proof: Assume that $\Gamma\vDash\alpha$. Then $\vDash\Gamma\to\alpha$. Thus, by Proposition 6.8, $\vdash\Gamma\to\alpha$ and so $\Gamma\vdash\alpha$. QED

7 A Concrete Case Study in Cyber-Attack Attribution

In order to show how Time-Stamped Claim Logic works, we consider a concrete case study inspired by the Ukraine Power Grid Attack that occurred in December 2015 [11]. For the sake of simplicity, we removed the references to the real actors involved in the attack and substituted them with generic ones. A good part of the provided evidence will be similar to the one found for this attack — we just carried out some simplifications for the sake of understandability.

7.1 The Set-Up

We will denote the analyzed attack with PGA and its victim with U. We have 11 agents/sources that provides information about this attack: $\mathrm{SC_{1}}$, $\mathrm{SC_{2}}$ and $\mathrm{SC_{3}}$ are three different security companies; $\mathrm{SD}$ is the security department of an impartial country; $\mathrm{SA_{1}}$ and $\mathrm{SA_{2}}$ are two sources with connections with country $\mathrm{A}$; $\mathrm{Ag}$ is a well-known international news agency; $\mathrm{NV}$ is a non-verified source; $\mathrm{F_{1}}$ is the forensics investigator hired by the victim; $\mathrm{F_{2}}$ is the forensics investigator of company $\mathrm{SC_{2}}$; $\mathrm{Bl}$ is an analyst that writes blog posts related to cyber-attacks. Furthermore, $\mathrm{A}$ is a country, and $\mathrm{HG}$ denotes a famous group of hackers.

For what concerns time, $t^{\prime}$ is Spring 2015, $t^{\prime\prime}$ is December 2015, whereas $t$ is a more general instant of time that can spread from Spring 2015 to (including) December 2015.

7.2 The Evidence

In the following, we list the evidence provided by the analyst. We start with the given evidence and later provide the given derived evidence.

$\mathrm{SC_{1}}$ states that the IPs from where the attack was originated are geolocated in $\mathrm{A}$ (geoSourceIP).

[TABLE]

$\mathrm{SC_{1}}$ and $\mathrm{SC_{2}}$ both state that the used malware (usedMalware) in this attack (PGA) was a version of the BlackEnergy malware, BE3, whereas $\mathrm{SA_{1}}$ states that the malware used in the attack was not BE3 but KillDisk. The provided information holds as different attackers can use different malware or pieces of software for the same attack.

[TABLE]

Source $\mathrm{SC_{2}}$ states that KillDisk was used during the attack, as it found traces of the KillDisk malware when analysing the infected system. $\mathrm{SD}$ and $\mathrm{SC_{1}}$ both state that BE3 is similar to its previous version BE2, whereas $\mathrm{SA_{1}}$ denies this statement.

[TABLE]

Furthermore, at $\mathrm{SD}$’s website is stated that BE2 is used mainly (usedBy) by a group of attackers denoted by $\mathrm{HG}$. $\mathrm{SC_{1}}$ states that $\mathrm{HG}$ targeted in the past mainly victims (targetVictim) that have shown some form of opposition against $\mathrm{A}$, its government, or its economical interest, denoted by $\mathrm{A}\_\textrm{Opponent}$.

[TABLE]

Let us now introduce the evidence related the negative consequences of the attack PGA. $\mathrm{SA_{1}}$ states that the victim suffered from economical losses from the attack (econLoss), while the news agency $\mathrm{Ag}$ states that the main losses were in reputation with respect to the citizens (repLoss). Other agents like $\mathrm{SC_{2}}$ states that the damages of PGA were limited (limitedDamage), whereas U states that this assertion is not true.

[TABLE]

Further information were provided by the victim’s forensics investigator $\mathrm{F_{1}}$, which states that he found, in the victim’s email server, phishing emails containing BE3, dated in Spring 2015, denoted by $t^{\prime}$. Furthermore, $\mathrm{F_{1}}$ states that in $t^{\prime}$ there was a campaign of phishing emails (spearPhishing) and the infection with BE3 happened through those phishing emails. $\mathrm{SC_{2}}$ states that BE3 is able to create a backdoor to the victim’s system. The statement about the infection was also confirmed by investigator $\mathrm{F_{2}}$, who states also that the infection with BE3 did not happened by exploiting the Human Machine Interaction (HMI) vulnerabilities, and this vulnerabilities were not exploited (exploitedVuln). This last statement is provided also by $\mathrm{F_{1}}$.

[TABLE]

There are more information about how U was infected. In particular, $\mathrm{SC_{2}}$ states that BE2 infection occurs using HMI vulnerabilities, whereas $\mathrm{SA_{2}}$ states that BE3 infection did not occurred using phishing emails. $\mathrm{SC_{2}}$ states that KillDisk is used by $\mathrm{HG}$, while $\mathrm{SA_{1}}$ states the opposite, and $\mathrm{SA_{2}}$ states that KillDisk is used by $\mathrm{A}$. The news agency, $\mathrm{Ag}$, states the news about the blackout of the victim in December 2015, denoted by $t^{\prime\prime}$, and that there was a political conflict (polConflict) between the victim and country $\mathrm{A}$ in that period.

[TABLE]

Let us now introduce the provided derived evidence for this cyber-attack. The sources provide discordant derived evidence with respect to the motives of the attack, whether the attack had or not economical motives. In particular, $\mathrm{SC_{2}}$ states that attacker did not have economical motives (econMotives) to perform the attack as there were not considerable economical losses (econLoss) since the damages caused by the attack to the victim were limited (limitedDamage). On the other hand, $\mathrm{SA_{1}}$ states that the attacker was pushed by economical motives because it caused to the victim economical losses and reputation losses (repLoss).

[TABLE]

There are discordant derived evidence also about how the attacker got access to the victim system (victimAccess). $\mathrm{SC_{3}}$ states that the attacker got access by exploiting the HMI vulnerabilities (HMIvuln), as during the attack the BE3 malware was used, and this is similar to BE2, which usually infects (infection) the system by exploiting the HMI vulnerabilities. $\mathrm{SC_{2}}$ states that the access to the victim system was done using phishing emails (phishEmails) and not through the exploitation of HMI vulnerabilities, because phishing emails were found in the victim system, thus there was a spear-phishing campaign (spearPhishing), the BE3 malware was found in the phishing emails (found), and the system was infected by BE3 through the emails. $\mathrm{SC_{1}}$ states as well that the victim’s system was not accessed using HMI vulnerabilities, as the system was not infected by BE3 through these vulnerabilities, and they were not exploited (exploitedVuln).

[TABLE]

The derived evidence provided by the various sources have discordances also for the starting date of the attack. In particular, $\mathrm{SC_{2}}$ states that the attack started in Spring 2015, denoted by $t^{\prime}$, as in that period there was a spear-phishing campaign, the system was infected with BE3 through the phishing emails, and a backdoor was created to the victim’s system. $\mathrm{SA_{1}}$ instead states that the attack started in December 2015, denoted by $t^{\prime\prime}$, as the news about the victim’s blackout dates to that period. $\mathrm{SC_{1}}$ contradicts $\mathrm{SA_{1}}$, by stating that the attack did not start in $t^{\prime\prime}$, as the infection occurred in $t^{\prime}$, and the news about the attack spread in $t^{\prime\prime}$. $\mathrm{SC_{2}}$ states the same derived evidence as $\mathrm{SC_{1}}$, but based on the evidence that the attack started in $t^{\prime}$ and that $t^{\prime}$ is different from $t^{\prime\prime}$.

[TABLE]

The last discordance arises about the possible culprit of the attack. $\mathrm{SC_{1}}$ states that the group of attackers $\mathrm{HG}$ is a possible culprit, as malware BE3 was used during PGA, which is similar to malware BE2 that is used by $\mathrm{HG}$. $\mathrm{SA_{1}}$ states that the possible culprit of the attack is not country $\mathrm{A}$, as the used malware was KillDisk and KillDisk is not used neither by $\mathrm{HG}$ nor by $\mathrm{A}$. Source $\mathrm{Bl}$ states that the possible culprit of the attack is country $\mathrm{A}$, as there was a political conflict in that period between $\mathrm{A}$ and the victim U. The attack was political, as U did not suffer from economical losses and the source IPs of the attack were geolocated in country $\mathrm{A}$.

[TABLE]

Let us now introduce the relations of trust the analyst has with respect to the sources that provided the above evidence. In particular, the analyst trusts: $\mathrm{SC_{2}}$ more than $\mathrm{SA_{1}}$ about the economical losses of U from PGA; $\mathrm{SA_{2}}$ more than $\mathrm{F_{1}}$ and $\mathrm{F_{2}}$ more than $\mathrm{SA_{2}}$ for how the PGA was able to infect U, (infection); $\mathrm{SC_{2}}$ more than $\mathrm{SA_{1}}$ for when the attack started; $\mathrm{SA_{2}}$ and $\mathrm{SC_{2}}$ more than $\mathrm{SA_{1}}$ about who has used a particular malware in the past; and $\mathrm{SC_{1}}$ more than $\mathrm{Bl}$ about who is a possible culprit of PGA:

[TABLE]

Moreover: $\mathrm{SC_{2}}$ is the most trusted agent about how the attacker accessed the victim’s system, the economical losses, the economical motives and the limited damages; $\mathrm{Ag}$ is the most trusted about identifying political conflict between entities; $\mathrm{SD}$ is the most trusted about the similarities between malware and used malware in attacks; $\mathrm{SC_{1}}$ is the most trusted about geolocating the source IPs of an attack; $\mathrm{SC_{1}}$ is the most trusted regarding the statement that BE3 and BE2 are similar between each other.

[TABLE]

7.3 The Conclusions of the Analyst

In the following, we show how the analyst can use the Time-Stamped Claim Logic to draw some interesting conclusions from the collected evidence.

Consider the following assertions:

[TABLE]

We start by giving the derivation in Figure 3 of

[TABLE]

from the assumptions $\psi_{1}$ and $\delta_{2}$. We can then show that

[TABLE]

is derived from $\psi_{1}$, $\psi_{2}$ and $\delta_{2}$ as can be seen in Figure 4. The derivation in Figure 5 infers

[TABLE]

from $\psi_{1}$, $\psi_{2}$, $\delta_{1}$ and $\delta_{2}$. From $\psi_{1}$, $\psi_{2}$, $\psi_{3}$, $\delta_{1}$ and $\delta_{2}$, we can also derive

[TABLE]

as can be seen in Figure 6.

From $\psi_{1}$, $\psi_{2}$, $\psi_{3}$, $\delta_{1}$, $\delta_{2}$ and $\delta_{3}$ we can derive

[TABLE]

as can be seen in Figure 7.

From

[TABLE]

we can conclude

[TABLE]

as can be seen in Figure 8.

Finally, it is not difficult to conclude

[TABLE]

from

[TABLE]

and some of the above results. However, thanks to the trust relation

[TABLE]

which says that the analyst trusts $\mathrm{SC_{1}}$ more than $\mathrm{Bl}$ for what concerns the possible culprit of the attack, the analyst’s final result will discard $\mathrm{Bl}$’s statement, and the analyst will conclude that the possible culprit of the attack is $\mathrm{HG}$.

7.4 Summary

In this case study, one of the forensics analyst’s conclusions is that a possible culprit of the attack is the group of hackers denoted by $\mathrm{HG}$. This conclusion was derived using the analyst’s relation of trust, where the analyst trusts the security company $\mathrm{SC_{1}}$ more than $\mathrm{Bl}$. Given the set of evidence collected, our Time-Stamped Claim Logic allows the analyst to filter the conflicting evidence by using his relations of trust. This reduces the number of evidence that the analyst needs to consider during the analysis phase. Furthermore, the set of evidence that the analyst obtains in this way is consistent, as all the conflicting pieces of evidence are removed (assuming that the analyst has provided all the required trust relations).

Our Time-Stamped Claim Logic provides to the forensics analyst with a sound and complete means to reduce the size of the collected set of evidence and remove inconsistencies, i.e., the logic ensures that the result is consistent with respect to the trust relations that the analyst considers to hold. In other words, the logic uses the evidence and the derivation of evidence of trusted sources together with the analyst’s relations of trust to remove the inconstancies and provide to the analyst only evidence that is trustworthy (from his point of view). Furthermore, the logic is able to provide to the analyst new evidence derived using the given set of evidence. The derived evidence can be general evidence that is always true or statements that sources have made and that the analyst trusts.

8 Related Work

In this section, we discuss the logics and approaches that are most closely related to our Time-Stamped Claim Logic.

We begin by pointing out that there are a number of recent works on reasoning about claims from different logical points of view, namely Justification Logics (see [4, 13, 8]), which capitalizes on the Logic of Proofs (see [3]), Modal Evidence Logic (see [28, 27, 6]) and a logical account of Formal Argumentation (see [9]). A recent work presents a paraconsistent logic able to reason about preservation of evidence and of truth (see [10]).

In Justification Logics [4, 13, 8] propositional formulas are labeled with justification terms built from variables and constants using several operations. The semantics is provided by Kripke structures enriched with an evidence function that associates a set of worlds to each propositional formula and justification term. Justifications in this logic are seen as the strongest form of evidence providing a direct proof of the truth of an assertion.

More specifically, Justification Logics are enrichments of classical propositional logic with assertions of the form

[TABLE]

where $s$ is a term and $F$ is a propositional formula, meaning that $s$ is a justification for $F$. The operations allowed on the labels express the possible interactions that justifications may have. The logic we propose differs significantly from Justification Logics since our main goal is to address distributed time-stamped claims instead of justifications. Reflecting this different goal, the labels in the Time-Stamped Claim Logic are an agent and/or a time-stamp. Furthermore, our logic includes explicit constructions for expressing trust relations between agents with respect to relevant evidence. On the other hand, Justification Logics may allow nesting of labels which our logic currently does not support. Both Justification Logics and Time-Stamped Claim Logic allow reasoning about labeled formulas and formulas without labels. However, the relationship between these formulas is made clear at the meta-level in Justification Logics, whereas in the calculus of Time-Stamped Claim Logic this relationship is internalized.

The Modal Evidence Logic [28, 27, 6] provides a way to model epistemic agents when dealing with evidence from different sources. It is a multi-modal logic that comprises three modal like operators: one for representing that an agent has evidence for a formula, another for stating that an agent believes a formula to be true and a last one asserting that a formula is true in every world. Neighborhood semantics is adopted.

An important difference between Modal Evidence Logic and our Time-Stamped Claim Logic is that Modal Evidence Logic is not a labeled logic. Consequently, no explicit reasoning about agents is possible in Modal Evidence Logic contrarily to what happens in our logic. Moreover, in Modal Evidence Logic there is no specific mechanism for dealing with time-stamped claims.

Formal argumentation has been investigated since the early 1990s but it was the landmark work in [12] that started an abstract perspective on argumentation. A logic foundation of formal argumentation was proposed in [9] using classical logic as well as modal logic to characterize different extensions for argumentation. The main difference between that work and Time-Stamped Claim Logic is that the former is related to arguments and the latter is concerned with agent claims. So, naturally, there is an attack relation between arguments in Formal Argumentation, whereas there is a trustful relationship between agents with respect to a given subject in Time-Stamped Claim Logic. In both Formal Argumentation and Time-Stamped Claim Logic, there are three possibilities for the valuation of both an argument and a claim. Hence, both have three-valued interpretations. In Formal Argumentation, an argument can be explicitly accepted (truth value in), explicitly rejected (truth value out) or neither explicitly accepted nor explicitly rejected (truth value undec). In our logic, either an agent $d$ claims that $p$ occurred at time $n$ (truth value $1$), or an agent $d$ claims that $p$ did not occur at time $n$ (truth value [math]) or an agent $d$ does not have an opinion about the occurrence of $p$ at time $n$ (truth value $\frac{1}{2}$).

Digital forensics techniques suffer from quantity and complexity problems [7] due to the necessity to handle an enormous amount of pieces of evidence and to the low format of the collected evidence. In this work, we proposed a solution that deals with the quantity problem: Time-Stamped Claim Logic reduces drastically the number of given evidence using the relations of trust of the analyst. Our logic allows the forensics team to decrease the resources spent on the analysis, which is usually a human-based process, and to arrive to a swift conclusion. Filtering the evidence reduces the chances of human error as the analyst needs to deal with a considerably lower number of pieces of evidence during the analysis phase.

The gathered pieces of evidence can be in conflict with each other because they are collected from difference sources and because of the anti-forensics [16, 30] and deception techniques [1, 2] used by the attackers to hide their traces. Digital forensics techniques are able to deal with conflicting information [5, 14, 18, 20], but without taking into account the analyst’s relations of trust. Our logic solves the conflicts by using in the derivations only trusted pieces of evidence, thus providing as conclusions only consistent sets of pieces of evidence.

Filtering the evidence of the attack using the Time-Stamped Claim Logic helps the analyst to swiftly identify who has performed the attack with a higher level of confidence. In particular, the results of the filtering process can be used by the analyst during the attribution phase [20]: the analyst can then deal only with trusted evidence and has a higher level of confidence for the given result. Using this filtering process would reduce the resources and time spent during the attribution phase, which is a crucial aspect of digital forensics investigations.

In [19], the authors have proposed another formal solution for filtering the evidence of cyber-attacks. They introduced the Evidence Logic (EL), which is based on an enriched Linear Temporal Logic and represents the evidence (simple and derived), the sources, the reasonings, the instants of time, and the analyst’s relations of trust with respect to the sources and the used reasoning. EL and Time-Stamped Claim Logic obviously share some similarities, starting with the objective of providing security analysts with the formal means to reduce the size of the collected set of evidence and remove inconsistencies. There are also some fundamental differences, though. Most notably, EL is based on a monotonic-reasoning procedure that rewrites the pieces of evidence with the use of tableau rules, but the rewriting system and algorithm that govern the inferences lack a completeness proof. There are also differences in the expressive power of the two logics. In particular, EL has a restrictive constraint, where an evidence is either given or derived, whereas the Time-Stamped Claim Logic is more expressive, as it permits one to represent the same evidence as given and derived (for instance, in the case study in Section 7, the evidence econLoss is both given and derived). The Time-Stamped Claim Logic permits one to better represent real evidence that can be both given and derived by other evidence. Moreover, the Time-Stamped Claim Logic uses in its reasonings only trusted evidence, whereas EL has a more credulous nature, where it considers in its reasoning also the simple evidence used by the sources to derive new evidence.

There are differences also at the level of trust relations. The trust relations in EL are binary relations between two different sources, whereas the Time-Stamped Claim Logic has also universal trust relations, where a certain source is the most trusted for a particular evidence ($\forall x.\,x\mathbin{\trianglelefteq}_{p}a$ and $a:\mathop{\boxdot}\phi$). EL is able to represent the relation $\forall x.\,x\mathbin{\trianglelefteq}_{p}a$ by introducing all the needed binary relations of trust (if there are a finite number of sources), but in case new evidence is added, it needs to add new trust relations as well. However, EL is not able to represent the $a:\mathop{\boxdot}\phi$ relation.

EL represents the reasonings followed by the source to derive an evidence, as well as the trust relations between reasonings. The reasonings can be applied by different sources to derive the same conclusion, using the same premises. The Time-Stamped Claim Logic does not represent the reasonings or their trust relations, instead, it uses the trust relations between sources. The use of the reasonings and their trust relations in EL permits it to be more generic, whereas the use of trust relations between sources for the derived evidence gives a higher level of specificity to the Time-Stamped Claim Logic.

Finally, it is interesting to note that, for all these reasons, EL is not able to handle the case study that we considered in this paper in the same way as the Time-Stamped Claim Logic. In order to allow an analyst to derive the same conclusions we obtained here, EL would need to undergo some changes which would come at the cost of losing expressivity.

9 Concluding Remarks and Future Work

We proposed a logic for reasoning about time-stamped claims by presenting a Gentzen calculus and a semantics, and proved soundness and completeness. We also showed how it can be applied concretely to a case study in cyber-security attribution. There are several directions for future work. The first is to provide automated support for our calculus (e.g., by implementing it in a logical framework such as Isabelle or as a tableaux system) in order to avoid having to carry out the derivations by hand. We also intend to investigate whether the logic is decidable [24] and whether the logic has Craig interpolation [26]. Moreover, it would be interesting to generalize the language of the logic in order to address other general claims as well as to enrich the logic with dynamic features [29]. It also seems natural and worthwhile to incorporate probabilistic primitives and reasoning in the logic [22, 21, 25, 17]. Finally, it seems worthwhile to investigate the combination of this logic with logics addressing different aspects in order to obtain a logic with a broader applicability [15, 23].

Acknowledgments

João Rasga and Cristina Sernadas deeply acknowledge the National Funding from FCT (Fundação para a Ciência e a Tecnologia) under the project UID/MAT/04561/2019 granted to CMAFcIO (Centro de Matemática, Aplicações Fundamentais e Investigação Operacional) of Universidade de Lisboa. Erisa Karafili was supported by the European Union’s H2020 research and innovation programme under the Marie Curie grant agreement No. 746667.

Appendix A Some Proofs of Sections 5 and 6

Proposition A.1** (a.k.a. Proposition 5.2)**

The rules of the sequent calculus are sound.

• Proof: It is quite straightforward to see that the rules Ax, Cut, ER, ES and ET are sound.

$(\textrm{EC})$ Assume that $I\rho\Vdash t_{1}\cong t_{2}$, $I\rho\Vdash[\psi]^{t_{1}}_{t_{2}}$ and $I\rho\Vdash\Gamma$. When ${\textrm{var}}_{T}(\psi)$ is not $t_{1}$ then $\psi$ is $[\psi]^{t_{1}}_{t_{2}}$ and so the thesis follows immediately. Otherwise, if $\psi$ is $a:\phi$, then the result is immediate by definition of $I$.

$(\textrm{AT})$ Assume that $I\rho\Vdash a_{1}\mathbin{\trianglelefteq}_{p}a_{2}$, $I\rho\Vdash a_{2}\mathbin{\trianglelefteq}_{p}a_{3}$ and $I\rho\Vdash\Gamma$. The thesis follows immediately by the definition of interpretation structure since $\mathbin{\trianglelefteq}_{p}^{I}$ is transitive.

$(\textrm{AR})$ Observe that $I\rho\Vdash a\mathbin{\trianglelefteq}_{p}a$ since $\mathbin{\trianglelefteq}_{p}^{I}$ is reflexive.

$(\textrm{AC})$ Assume that $I\rho\Vdash a_{1}\mathbin{\trianglelefteq}_{p}a_{2}$, $I\rho\Vdash a_{2}\mathbin{\trianglelefteq}_{p}a_{1}$, $I\rho\Vdash[a:\phi]^{a_{1}}_{a_{2}}$ and $I\rho\Vdash\Gamma$. When $a$ is not $a_{1}$ then $[a:\phi]^{a_{1}}_{a_{2}}$ is $a:\phi$ and so the thesis follows immediately. Otherwise, the result is obtained by the definition of $I$.

$(\textrm{AMR})$ Assume that $I\rho^{\prime}\Vdash\Gamma\to\Delta,b\mathbin{\trianglelefteq}_{p}a$ for every $\rho^{\prime}$ such that $\rho^{\prime}\equiv^{A}_{b}\rho$ and $I\rho\Vdash\Gamma$. Suppose that there is no $\delta\in\Delta$ such that $I\rho\Vdash\delta$. Then $I\rho^{\prime}\Vdash b\mathbin{\trianglelefteq}_{p}a$ for every $\rho^{\prime}$ such that $\rho^{\prime}\equiv^{A}_{b}\rho$. Hence, $d\mathbin{\trianglelefteq}_{p}^{I}\rho_{a}(a)$ for each $d\in D_{A}$, and so $I\rho\Vdash\forall x.\,x\mathbin{\trianglelefteq}_{p}a$.

$(\textrm{AML})$ Assume that $I\rho\Vdash a^{\prime}\mathbin{\trianglelefteq}_{p}a,\forall x.\,x\mathbin{\trianglelefteq}_{p}a,\Gamma\to\Delta$, $I\rho\Vdash\forall x.\,x\mathbin{\trianglelefteq}_{p}a$ and $I\rho\Vdash\Gamma$. Then $d\mathbin{\trianglelefteq}_{p}^{I}\rho_{A}(a)$ for every $d\in D_{A}$. Hence, in particular, $\rho_{A}(a^{\prime})\mathbin{\trianglelefteq}_{p}^{I}\rho_{A}(a)$ and so $I\rho\Vdash a^{\prime}\mathbin{\trianglelefteq}_{p}a$. Therefore, by the hypothesis, there is $\delta\in\Delta$ such that $I\rho\Vdash\delta$.

$(\textrm{NS})$ Assume that $I\rho\Vdash a:{-}\phi,\Gamma\to\Delta,a:\phi$, $I\rho\Vdash\Gamma$ and $I\rho\Vdash a:{-}\phi$. We just consider the case that $\phi$ is $t\cdot p$. Thus $V(p,\rho_{A}(a),\rho_{T}(t))=0$. Therefore, $I\rho\not\Vdash a:\phi$ and so, by the hypothesis, there is $\delta\in\Delta$ such that $I\rho\Vdash\delta$.

$(\textrm{NK})$ Assume that $I\rho\Vdash{-}\phi,\Gamma\to\Delta,\phi$, $I\rho\Vdash\Gamma$ and $I\rho\Vdash{-}\phi$. Then there is an assignment $\rho^{\prime}$ such that $\rho^{\prime}\equiv^{A}_{a}\rho$, $I\rho^{\prime}\Vdash a:{-}\phi$ and $I\rho^{\prime}\Vdash a:\mathop{\boxdot}{-}\phi$. Thus we can conclude immediately that $I\rho\not\Vdash\phi$. Therefore, by the hypothesis, there is $\delta\in\Delta$ such that $I\rho\Vdash\delta$.

$(\textrm{SP})$ Assume that $I\rho\Vdash\Gamma\to\Delta,t_{1}\cong t_{2},a:{-}(t_{1}\cdot p),a:t_{2}\cdot p$ and $I\rho\Vdash\Gamma$. Assume, by contradiction, that there is no $\psi\in\Delta\cup\{t_{1}\cong t_{2},a:{-}(t_{1}\cdot p)\}$ such that $I\rho\Vdash\psi$. Then, $I\rho\Vdash a:t_{2}\cdot p$, that is, $V(p,\rho_{A}(a),\rho_{T}(t_{2}))=1$. If $I\rho\Vdash t_{1}\cong t_{2}$ the thesis follows immediately. Otherwise, $\rho_{T}(t_{1})\not\cong^{I}\rho_{T}(t_{2})$. Then, by definition of $V$, $V(p,\rho_{A}(a),\rho_{T}(t_{1}))=0$. So $I\rho\Vdash a:{-}(t_{1}\cdot p)$ contradicting the assumption.

$(\textrm{KP})$ Assume that $I\rho\Vdash\Gamma\to\Delta,t_{1}\cong t_{2},{-}(t_{1}\cdot p),t_{2}\cdot p$ and $I\rho\Vdash\Gamma$. Assume, by contradiction that there is no $\psi\in\Delta\cup\{t_{1}\cong t_{2},{-}(t_{1}\cdot p)\}$ such that $I\rho\Vdash\psi$. Then, $I\rho\Vdash t_{2}\cdot p$. We now show that $I\rho\Vdash{-}(t_{1}\cdot p)$ which leads to a contradiction. Let $\rho^{\prime}$ be such that $\rho^{\prime}\equiv^{A}_{b}\rho$ and $I\rho^{\prime}\Vdash b:t_{1}\cdot p$. Then $V(p,\rho^{\prime}_{A}(b),\rho_{T}(t_{1}))=1$ and so $V(p,\rho^{\prime}_{A}(b),\rho_{T}(t_{2}))=0$ since $\rho_{T}(t_{1})\not\cong^{I}\rho_{T}(t_{2})$. Hence, $I\rho^{\prime}\Vdash b:{-}(t_{2}\cdot p)$. Then $I\rho^{\prime}\not\Vdash b:\mathop{\boxdot}{-}(t_{2}\cdot p)$ by definition of $I\rho\Vdash t_{2}\cdot p$. Therefore, there is $\rho^{\prime\prime}\equiv^{A}_{b^{\prime}}\rho^{\prime}$ such that $I\rho^{\prime\prime}\Vdash b\mathbin{\trianglelefteq}_{p}b^{\prime}$ and $I\rho^{\prime\prime}\Vdash b^{\prime}:t_{2}\cdot p$. Then $V(p,\rho^{\prime\prime}_{A}(b^{\prime}),\rho_{T}(t_{2}))=1$ and so $V(p,\rho^{\prime\prime}_{A}(b^{\prime}),\rho_{T}(t_{1}))=0$. Thus, $I\rho^{\prime\prime}\Vdash b^{\prime}:{-}(t_{1}\cdot p)$ and so $I\rho^{\prime}\not\Vdash b:\mathop{\boxdot}t_{1}\cdot p$. With respect to the other condition, since $I\rho\Vdash t_{2}\cdot p$, let $\rho^{\prime}\equiv^{A}_{a}\rho$ be such that $I\rho^{\prime}\Vdash a:t_{2}\cdot p$ and $I\rho^{\prime}\Vdash a:\mathop{\boxdot}t_{2}\cdot p$. Thus $I\rho^{\prime}\Vdash a:{-}(t_{1}\cdot p)$. It remains to show that $I\rho^{\prime}\Vdash a:\mathop{\boxdot}{-}(t_{1}\cdot p)$. Let $\rho^{\prime\prime}\equiv^{A}_{b}\rho^{\prime}$ be such that $I\rho^{\prime\prime}\Vdash a\mathbin{\trianglelefteq}_{p}b$. Thus, $I\rho^{\prime\prime}\not\Vdash b:{-}(t_{2}\cdot p)$. Hence, $I\rho^{\prime\prime}\not\Vdash b:t_{1}\cdot p$.

$(\textrm{SCR})$ Assume that $I\rho^{\prime}\Vdash b:{-}\phi,a\mathbin{\trianglelefteq}_{{\textrm{var}}_{P}(\phi)}b,\Gamma\to\Delta$ for every $\rho^{\prime}$ such that $\rho^{\prime}\equiv^{A}_{b}\rho$, $I\rho\Vdash\Gamma$ and that there is no $\delta\in\Delta$ such that $I\rho\Vdash\delta$. We now show that $I\rho\Vdash a:\mathop{\boxdot}\phi$. Let $\sigma$ be such that $\sigma\equiv^{A}_{b}\rho$ and $I\sigma\Vdash a\mathbin{\trianglelefteq}_{{\textrm{var}}_{P}(\phi)}b$. Observe that $I\sigma\Vdash b:\phi,a\mathbin{\trianglelefteq}_{{\textrm{var}}_{P}(\phi)}b,\Gamma\to\Delta$, $I\sigma\Vdash\Gamma$ and there is no $\delta\in\Delta$ such that $I\sigma\Vdash\delta$. Then $I\sigma\not\Vdash b:{-}\phi$.

$(\textrm{SCL})$ Assume that $I\rho\Vdash a:\mathop{\boxdot}\phi,\Gamma\to\Delta,a\mathbin{\trianglelefteq}_{{\textrm{var}}_{P}(\phi)}a^{\prime}$, $I\rho\Vdash a:\mathop{\boxdot}\phi,\Gamma\to\Delta,a^{\prime}:{-}\phi$, $I\rho\Vdash\Gamma$ and $I\rho\Vdash a:\mathop{\boxdot}\phi$. Suppose, by contradiction, that there is no $\delta\in\Delta$ such that $I\rho\Vdash\delta$. Then $I\rho\Vdash a\mathbin{\trianglelefteq}_{{\textrm{var}}_{P}(\phi)}a^{\prime}$ and $I\rho\Vdash a^{\prime}:{-}\phi$. These facts contradict the hypothesis that $I\rho\Vdash a:\mathop{\boxdot}\phi$.

$(\textrm{SKR})$ Assume that $I\rho^{\prime}\Vdash b:{-}\phi,b:\mathop{\boxdot}{-}\phi,\Gamma\to\Delta$ for every $\rho^{\prime}\equiv^{A}_{b}\rho$, $I\rho\Vdash\Gamma\to\Delta,\phi,a:\phi$, $I\rho\Vdash\Gamma\to\Delta,\phi,a:\mathop{\boxdot}\phi$ and $I\rho\Vdash\Gamma$. Assume, by contradiction, that there is no $\psi\in\Delta\cup\{\phi\}$ such that $I\rho\Vdash\psi$. Then $I\rho\Vdash a:\phi$ and $I\rho\Vdash a:\mathop{\boxdot}\phi$. We now show that $I\rho\Vdash\phi$ leading to a contradiction. Let $\sigma\equiv^{A}_{b}\rho$ be such that $I\sigma\Vdash b:{-}\phi$. Taking $\rho^{\prime}$ as $\sigma$, by hypothesis, $I\sigma\not\Vdash b:\mathop{\boxdot}{-}\phi$. With respect to the second condition it is enough to take $\rho^{\prime}$ as $\rho$.

$(\textrm{KL})$ Assume that $I\rho^{\prime}\Vdash b:\phi,b:\mathop{\boxdot}\phi,\Gamma\to\Delta$ for every $\rho^{\prime}\equiv^{A}_{b}\rho$, $I\rho\Vdash\Gamma$ and $I\rho\Vdash\phi$. Assume, by contradiction, that there is no $\delta\in\Delta$ such that $I\rho\Vdash\delta$. Then, for every $\rho^{\prime}\equiv^{A}_{b}\rho$ either $I\rho^{\prime}\not\Vdash b:\phi$ or $I\rho^{\prime}\not\Vdash b:\mathop{\boxdot}\phi$. Since $I\rho\Vdash\phi$ then there is $\sigma^{\prime}\equiv^{A}_{a}\rho$ such that $I\sigma^{\prime}\Vdash a:\phi$ and $I\sigma^{\prime}\Vdash a:\mathop{\boxdot}\phi$ which contradicts the facts above.

$(\textrm{SKL})$ Assume that $I\rho\Vdash\phi,\Gamma\to\Delta,a:{-}\phi$, $I\rho\Vdash\phi,\Gamma\to\Delta,a:\mathop{\boxdot}{-}\phi$, $\rho\Vdash\Gamma$ and $I\rho\Vdash\phi$. Assume, by contradiction, that there is no $\delta\in\Delta$ such that $I\rho\Vdash\delta$. Thus $I\rho\Vdash a:{-}\phi$ and $I\rho\Vdash a:\mathop{\boxdot}{-}\phi$ contradicting the fact that $I\rho\Vdash\phi$.

$(\textrm{CR}1)$ Assume that $I\rho\Vdash\phi_{1},\,\dots,\,\phi_{n},\Gamma\to\Delta,a::\phi$ and $I\rho\Vdash\Gamma$. If there is no $\delta\in\Delta$ such that $I\rho\Vdash\delta$ then $I\rho\Vdash a:\phi$ and so the thesis follows by definition.

$(\textrm{CR}2)$ Assume that $I\rho\Vdash\Gamma\to\Delta,\phi_{i}$ for $i=1,\dots,n$, $I\rho\Vdash a:\phi,\Gamma\to\Delta$, $I\rho\Vdash\Gamma$ and $I\rho\Vdash a::(\phi_{1},\,\dots,\,\phi_{n}/\phi)$. Suppose, by contradiction, that there is no $\delta\in\Delta$ such that $I\rho\Vdash\delta$. Hence, $I\rho\not\Vdash a:\phi$. Moreover, $I\rho\Vdash\phi_{i}$ for $i=1,\dots,n$. So, by hypothesis, $I\rho\Vdash a:\phi$ which is a contradiction. QED

Proposition A.2** (a.k.a. Proposition 6.2)**

Let $H=(\Psi_{L},\Psi_{R})$ be a Hintikka pair over $P^{\prime}$, $X^{\prime}_{A}$ and $X^{\prime}_{T}$. Then there are an interpretation structure $I_{H}$ over $P^{\prime}$ and an assignment $\rho$ over $I_{H}$ such that $I_{H}\rho\Vdash\psi$ for each $\psi\in\Psi_{L}$ and $I_{H}\rho\not\Vdash\psi$ for each $\psi\in\Psi_{R}$.

• Proof: Let $H=(\Psi_{L},\Psi_{R})$ be a Hintikka pair. Consider the interpretation structure $I_{H}$ over $P^{\prime}$ defined as follows:

• –

the domain $D_{A}$ is $X^{\prime}_{A}$, that is, ${\textrm{var}}_{A}(\Psi_{L}\cup\Psi_{R})$,

• –

the domain $D_{T}$ is $X^{\prime}_{T}$, that is, ${\textrm{var}}_{T}(\Psi_{L}\cup\Psi_{R})$,

• –

$(t_{1},t_{2})\in\;\cong^{I_{H}}\quad\text{iff}\quad t_{1}\cong t_{2}\in\Psi_{L}$,

• –

$(a_{1},a_{2})\in\mathbin{\trianglelefteq}_{p}^{I_{H}}\quad\text{iff}\quad a_{1}\mathbin{\trianglelefteq}_{p}a_{2}\in\Psi_{L}$,

• –

$V(p,a,t)=\begin{cases}1&\textrm{if }a:t\cdot p\in\Psi_{L}\\[2.84526pt] 0&\textrm{if }a:{-}(t\cdot p)\in\Psi_{L}\\[2.84526pt] \frac{1}{2}&\textrm{otherwise.}\end{cases}$

Consider also an assignment $\rho$ such that $\rho_{A}$ and $\rho_{T}$ are identities. We show that for every $\psi\in L_{P^{\prime}}^{X^{\prime}_{A},X^{\prime}_{T}}$ we have

[TABLE]

$\psi$ is $t_{1}\cong t_{2}$.

1. (a)

Assume that $t_{1}\cong t_{2}\in\Psi_{L}$. Then $(t_{1},t_{2})\in\;\cong^{I_{H}}$ and so $I_{H}\rho\Vdash t_{1}\cong t_{2}$. 2. (b)

Assume that $t_{1}\cong t_{2}\in\Psi_{R}$. Then $(t_{1},t_{2})\in\;\cong^{I_{H}}$ and so $I_{H}\rho\not\Vdash t_{1}\cong t_{2}$. 2. 2.

$\psi$ is $a_{1}\mathbin{\trianglelefteq}_{p}a_{2}$.

1. (a)

Assume that $a_{1}\mathbin{\trianglelefteq}_{p}a_{2}\in\Psi_{L}$. Then $(a_{1},a_{2})\in\mathbin{\trianglelefteq}_{p}^{I_{H}}$ and so $I_{H}\rho\Vdash a_{1}\mathbin{\trianglelefteq}_{p}a_{2}$. 2. (b)

Assume that $a_{1}\mathbin{\trianglelefteq}_{p}a_{2}\in\Psi_{R}$. Then $(a_{1},a_{2})\notin\mathbin{\trianglelefteq}_{p}^{I_{H}}$ and so $I_{H}\rho\not\Vdash a_{1}\mathbin{\trianglelefteq}_{p}a_{2}$. 3. 3.

$\psi$ is $\forall x.\,x\mathbin{\trianglelefteq}_{p}a$.

1. (a)

Assume that $\forall x.\,x\mathbin{\trianglelefteq}_{p}a\in\Psi_{L}$. Then for each $a_{1}\in X^{\prime}_{A}$ we have $a_{1}\mathbin{\trianglelefteq}_{p}a\in\Psi_{L}$. Hence, $I_{H}\rho\Vdash a_{1}\mathbin{\trianglelefteq}_{p}a$ for each $a_{1}\in D_{A}$ and so $I\rho\Vdash\forall x.\,x\mathbin{\trianglelefteq}_{p}a$. 2. (b)

Assume that $\forall x.\,x\mathbin{\trianglelefteq}_{p}a\in\Psi_{R}$. Then there is $a^{\prime}\in X^{\prime}_{A}$ such that $a^{\prime}\mathbin{\trianglelefteq}_{p}a\in\Psi_{R}$. Therefore, $I\rho\not\Vdash a^{\prime}\mathbin{\trianglelefteq}_{p}$ and so $I\rho\not\Vdash\forall x.\,x\mathbin{\trianglelefteq}_{p}a$. 4. 4.

$\psi$ is $a:t\cdot p$.

1. (a)

Assume that $a:t\cdot p\in\Psi_{L}$. Then $V(p,a,t)=1$ and $I_{H}\rho\Vdash a:t\cdot p$. 2. (b)

Assume that $a:t\cdot p\in\Psi_{R}$. Then $V(p,a,t)\in\{0,\frac{1}{2}\}$ and so $I_{H}\rho\not\Vdash a:t\cdot p$. 5. 5.

$\psi$ is $a:{-}(t\cdot p)$.

1. (a)

Assume that $a:{-}(t\cdot p)\in\Psi_{L}$. Then $V(p,a,t)=0$. Hence $I_{H}\rho\Vdash a:{-}(t\cdot p)$. 2. (b)

Assume that $a:{-}(t\cdot p)\in\Psi_{R}$. Then $V(p,a,t)\in\{1,\frac{1}{2}\}$ and so $I_{H}\rho\not\Vdash a:{-}(t\cdot p)$. 6. 6.

$\psi$ is $a:\mathop{\boxdot}\phi$.

1. (a)

Assume that $a:\mathop{\boxdot}\phi\in\Psi_{L}$. Then, for each $a^{\prime}\in X^{\prime}_{A}$ either $a\mathbin{\trianglelefteq}_{{\textrm{var}}(\phi)}a^{\prime}\in\Psi_{R}$ or $a^{\prime}:{-}\phi\in\Psi_{R}$. Hence, by the induction hypothesis, for each $a^{\prime}\in X^{\prime}_{A}$ either $I_{H}\rho\not\Vdash a\mathbin{\trianglelefteq}_{{\textrm{var}}(\phi)}a^{\prime}$ or $I_{H}\rho\not\Vdash a^{\prime}:{-}\phi$. Hence for each $a^{\prime}\in X^{\prime}_{A}$ if $I_{H}\rho\Vdash a\mathbin{\trianglelefteq}_{{\textrm{var}}(\phi)}a^{\prime}$ then $I_{H}\rho\not\Vdash a^{\prime}:{-}\phi$. Let $\rho^{\prime}$ be an assignment such that $\rho^{\prime}\equiv^{A^{\prime}}_{b}\rho$ and $I_{H}\rho^{\prime}\Vdash a\mathbin{\trianglelefteq}_{{\textrm{var}}(\phi)}b$. Thus $I_{H}\rho\Vdash a\mathbin{\trianglelefteq}_{{\textrm{var}}(\phi)}\rho^{\prime}(b)$. Therefore, $I_{H}\rho\not\Vdash\rho^{\prime}(b):{-}\phi$ and so $I_{H}\rho^{\prime}\not\Vdash b:{-}\phi$. 2. (b)

Assume that $a:\mathop{\boxdot}\phi\in\Psi_{R}$. Then there is $a^{\prime}\in X^{\prime}_{A}$ such that $a\mathbin{\trianglelefteq}_{{\textrm{var}}(\phi)}a^{\prime},a^{\prime}:{-}\phi\in\Psi_{L}$. So, by the induction hypothesis, there is $a^{\prime}\in X^{\prime}_{A}$ such that $I_{H}\rho\Vdash a\mathbin{\trianglelefteq}_{{\textrm{var}}(\phi)}a^{\prime}$ and $I_{H}\rho\Vdash a^{\prime}:{-}\phi$. Let $\rho^{\prime}\equiv^{A^{\prime}}_{b}\rho$ be such that $\rho^{\prime}(b)=a^{\prime}$. Then $I_{H}\rho^{\prime}\Vdash a\mathbin{\trianglelefteq}_{{\textrm{var}}(\phi)}b$ and $I_{H}\rho^{\prime}\Vdash b:{-}\phi$. Therefore, $I\rho\not\Vdash a:\mathop{\boxdot}\phi$. 7. 7.

$\psi$ is $\phi\in K_{P}$.

1. (a)

Assume that $\phi\in\Psi_{L}$. Then there is $a^{\prime}\in X^{\prime}_{A}$ such that $a^{\prime}:\phi,a^{\prime}:\mathop{\boxdot}\phi\in\Psi_{L}$ and for every $a\in X^{\prime}_{A}$ either $a:{-}\phi\in\Psi_{R}$ or $a:\mathop{\boxdot}{-}\phi\in\Psi_{R}$. Thus, by the induction hypothesis, there is $a^{\prime}\in X^{\prime}_{A}$ such that $I_{H}\rho\Vdash a^{\prime}:\phi$ and $I_{H}\rho\Vdash a^{\prime}:\mathop{\boxdot}\phi$ and for each $a\in X^{\prime}_{A}$ either $I_{H}\rho\not\Vdash a:{-}\phi$ or $I_{H}\rho\not\Vdash a:\mathop{\boxdot}{-}\phi$. We now show that $I_{H}\rho\Vdash\phi$. Let $\rho^{\prime}\equiv^{A^{\prime}}_{b}\rho$ be such that $I_{H}\rho^{\prime}\Vdash b:{-}\phi$. Then $I_{H}\rho\Vdash\rho^{\prime}(b):{-}\phi$. Hence $I_{H}\rho\not\Vdash\rho^{\prime}(b):\mathop{\boxdot}{-}\phi$, by hypothesis. Therefore $I_{H}\rho^{\prime}\not\Vdash b:\mathop{\boxdot}{-}\phi$. The other condition follows straightforwardly taking into account one of the assumptions. 2. (b)

Assume that $\phi\in\Psi_{R}$. Then either there exists $a^{\prime}\in X^{\prime}_{A}$ such that $a^{\prime}:{-}\phi,a^{\prime}:\mathop{\boxdot}{-}\phi\in\Psi_{L}$ or for each $a\in X^{\prime}_{A}$ either $a:\phi\in\Psi_{R}$ or $a:\mathop{\boxdot}\phi\in\Psi_{R}$. Hence, by the induction hypothesis, either there exists $a^{\prime}\in X^{\prime}_{A}$ such that $I_{H}\rho\Vdash a^{\prime}:{-}\phi$ and $I_{H}\rho\Vdash a^{\prime}:\mathop{\boxdot}{-}\phi$ or for each $a\in X^{\prime}_{A}$ either $I_{H}\rho\not\Vdash a:\phi$ or $I_{H}\rho\not\Vdash a:\mathop{\boxdot}\phi$. We now show that $I_{H}\rho\not\Vdash\phi$. Assume that for each assignment $\rho^{\prime}$ such that $\rho^{\prime}\equiv^{A}_{b}\rho$, if $I_{H}\rho^{\prime}\Vdash b:{-}\phi$ then $I_{H}\rho^{\prime}\not\Vdash b:\mathop{\boxdot}{-}\phi$. Then for each $a\in X^{\prime}_{A}$ either $I_{H}\rho\not\Vdash a:\phi$ or $I_{H}\rho\not\Vdash a:\mathop{\boxdot}\phi$. Then for each $\rho^{\prime}$ such that $\rho^{\prime}\equiv^{A}_{a}\rho$ and $I_{H}\rho^{\prime}\Vdash a:\phi$ we have $I_{H}\rho^{\prime}\not\Vdash a:\mathop{\boxdot}\phi$. 8. 8.

$\psi$ is $a::(\phi_{1},\dots,\phi_{n}/\phi)$.

1. (a)

Assume that $a::(\phi_{1},\dots,\phi_{n}/\phi)\in\Psi_{L}$. Then either $\phi_{i}\in\Psi_{R}$ for some $i=1,\dots,n$ or $a:\phi\in\Psi_{L}$. Then, by the induction hypothesis, either $I_{H}\rho\not\Vdash\phi_{i}$ for some $i=1,\dots,n$ or $I_{H}\rho\Vdash a:\phi$. Therefore, $I_{H}\rho\Vdash a::(\phi_{1},\dots,\phi_{n}/\phi)$. 2. (b)

Assume that $a::(\phi_{1},\dots,\phi_{n}/\phi)\in\Psi_{R}$. Then if $\phi_{1},\dots,\phi_{n}\in\Phi_{L}$ then $a:\phi\in\Psi_{R}$. So, by the induction hypothesis, if $I_{H}\rho\Vdash\phi_{1},\cdots,I\rho\Vdash\phi_{n}$ then $I_{H}\rho\not\Vdash a:\phi$. Hence, $I_{H}\rho\not\Vdash a::(\phi_{1},\dots,\phi_{n}/\phi)$.

QED

Proposition A.3** (a.k.a. Proposition 6.6)**

Let $\Gamma^{\prime}_{1}\to\Delta^{\prime}_{1}\cdots\Gamma^{\prime}_{n}\to\Delta^{\prime}_{n}$ be a rooted open analytical exhausted branch of an expansion $\Gamma_{1}\to\Delta_{1}\ \cdots$. Then

[TABLE]

is an Hintikka pair over ${\textrm{var}}_{P}(\Gamma^{\prime}_{n}\cup\Delta^{\prime}_{n})$, ${\textrm{var}}_{A}(\Gamma^{\prime}_{n}\cup\Delta^{\prime}_{n})$ and ${\textrm{var}}_{T}(\Gamma^{\prime}_{n}\cup\Delta^{\prime}_{n})$.

• Proof: In the sequel, we denote by $\Psi_{L}$ and $\Psi_{R}$ the left and the right hand side of the pair. We now show that this pair fullfils the conditions to be a Hintikka pair:

Either $\beta\notin\Psi_{L}$ or $\beta\notin\Psi_{R}$ where $\beta$ is of the form $a:\phi$, $t_{1}\cong t_{2}$ and $a_{1}\mathbin{\trianglelefteq}_{p}a_{2}$. Assume by contradiction that $\beta\in\Psi_{L}$ and $\beta\in\Psi_{R}$. Hence, there are $1\leq i,j\leq n$ such that $\beta\in\Gamma^{\prime}_{i}$ and $\beta\in\Delta^{\prime}_{j}$. Observe that any rule preserves $\beta$. Therefore, $\beta\in\Gamma^{\prime}_{n}\cap\Delta^{\prime}_{n}$ and so $\Gamma^{\prime}_{n}\to\Delta^{\prime}_{n}$ is an axiom contradicting the hypothesis that the branch is open. 2. 2.

Either $\beta\in\Psi_{L}$ or $\beta\in\Psi_{R}$ where $\beta$ is of the form $a:\phi$, $t_{1}\cong t_{2}$ and $a_{1}\mathbin{\trianglelefteq}_{p}a_{2}$. Assume, by contradiction, that $\beta$ is not in $\Psi_{L}\cup\Psi_{R}$. Consider the branch $\Gamma^{\prime}_{1}\to\Delta^{\prime}_{1}\cdots\Gamma^{\prime}_{n}\to\Delta^{\prime}_{n}\ \Gamma^{\prime}_{n}\to\Delta^{\prime}_{n},\beta$ using the cut rule in the last step. Observe that this branch is still analytical. Indeed $\beta$ does not occur in $(i_{R})_{n}$ and no fresh variables are involved. Hence we get a contradiction since the given branch is analytical and exhausted. 3. 3.

$t\cong t\notin\Psi_{R}$. Immediate by rule $(\textrm{ER})$ since the branch is open.  Similarly for $\mathbin{\trianglelefteq}_{p}$ 4. 4.

If $t_{1}\cong t_{2}\in\Psi_{L}$ then $t_{2}\cong t_{1}\notin\Psi_{R}$. Suppose that $t_{1}\cong t_{2}\in\Psi_{L}$. Then if $t_{2}\cong t_{1}\in\Psi_{R}$ we could conclude that the branch was not open using rule $(\textrm{ES})$. 5. 5.

If $t_{1}\cong t_{2},t_{2}\cong t_{3}\in\Psi_{L}$ then $t_{1}\cong t_{3}\notin\Psi_{R}$ and similarly for $\mathbin{\trianglelefteq}_{p}$. Suppose that $t_{1}\cong t_{2},t_{2}\cong t_{3}\in\Psi_{L}$. Then if $t_{1}\cong t_{3}\in\Psi_{R}$ we could conclude that the branch was not open using rule $(\textrm{ET})$. 6. 6.

If $t_{1}\cong t_{2},[a:\phi]^{t_{1}}_{t_{2}}\in\Psi_{L}$ then $a:\phi\notin\Psi_{R}$. Suppose that $t_{1}\cong t_{2},[a:\phi]^{t_{1}}_{t_{2}}\in\Psi_{L}$. Then if $a:\phi\in\Psi_{R}$ we could conclude that the branch was not open using rule $(\textrm{EC})$. 7. 7.

If $a_{1}\mathbin{\trianglelefteq}_{p}a_{2},a_{2}\mathbin{\trianglelefteq}_{p}a_{1},[a:\phi]^{a_{1}}_{a_{2}}\in\Psi_{L}$ then $a:\phi\notin\Psi_{R}$. The proof is similar to the one of (6). 8. 8.

If $\forall x.\,x\mathbin{\trianglelefteq}_{p}a\in\Psi_{R}$ then there is $a^{\prime}\in X^{\prime}_{A}$ such that $a^{\prime}\mathbin{\trianglelefteq}_{p}a\in\Psi_{R}$. Assume that $\forall x.\,x\mathbin{\trianglelefteq}_{p}a\in\Psi_{R}$. Suppose, by contradiction, that for every $a^{\prime}\in X^{\prime}_{A}$, $a^{\prime}\mathbin{\trianglelefteq}_{p}a\notin\Psi_{R}$. Then, rule (AMR) was not applied to $\forall x.\,x\mathbin{\trianglelefteq}_{p}a$ and so $\forall x.\,x\mathbin{\trianglelefteq}_{p}a\in\Delta^{\prime}_{n}$. Consider the branch $\Gamma^{\prime}_{1}\to\Delta^{\prime}_{1}\cdots\Gamma^{\prime}_{n}\to\Delta^{\prime}_{n}\ \Gamma^{\prime}_{n}\to(\Delta^{\prime}_{n}\setminus\{\forall x.\,x\mathbin{\trianglelefteq}_{p}a\}),b\mathbin{\trianglelefteq}_{p}a$ using in the last step the rule $(\textrm{AMR})$ where $b$ is not in $\Gamma^{\prime}_{n}\cup\Delta^{\prime}_{n}$. Observe that this branch is still analytical. So the original branch is not exhausted which contradicts the hypothesis. 9. 9.

If $\forall x.\,x\mathbin{\trianglelefteq}_{p}a\in\Psi_{L}$ then $a_{1}\mathbin{\trianglelefteq}_{p}a\in\Psi_{L}$ for each $a_{1}\in X^{\prime}_{A}$. Assume that $\forall x.\,x\mathbin{\trianglelefteq}_{p}a\in\Psi_{L}$. Suppose, by contradiction, that there is $a_{1}\in X^{\prime}_{A}$ such that $a_{1}\mathbin{\trianglelefteq}_{p}a\notin\Psi_{L}$. Observe that $\forall x.\,x\mathbin{\trianglelefteq}_{p}a$ is in $\Gamma^{\prime}_{n}$. Consider the branch $\Gamma^{\prime}_{1}\to\Delta^{\prime}_{1}\cdots\Gamma^{\prime}_{n}\to\Delta^{\prime}_{n}\ a_{1}\mathbin{\trianglelefteq}_{p}a,\Gamma^{\prime}_{n}\to\Delta^{\prime}_{n}$ using in the last step the rule $(\textrm{AML})$. Observe that this branch is still analytical. So the original branch is not exhausted which contradicts the hypothesis. 10. 10.

If $a:\phi\in\Psi_{L}$ then $a:{-}\phi\in\Psi_{R}$. Suppose that $a:\phi\in\Psi_{L}$. Assume, by contradiction that $a:{-}\phi\notin\Psi_{R}$. Consider the branch $\Gamma^{\prime}_{1}\to\Delta^{\prime}_{1}\cdots\Gamma^{\prime}_{n}\to\Delta^{\prime}_{n}\ \Gamma^{\prime}_{n}\to\Delta^{\prime}_{n},a:{-}\phi$ using in the last step the rule $(\textrm{NS})$. Observe that this branch is still analytical. Indeed $a:{-}\phi$ does not occur in $(i_{R})_{n}$ and no fresh variables are involved. Hence we get a contradiction since the given branch is analytical and exhausted. 11. 11.

If $t_{1}\cong t_{2},a:{-}(t_{1}\cdot p)\in\Psi_{R}$ then $a:t_{2}\cdot p\in\Psi_{R}$. The proof is similar to one of (10). 12. 12.

If $a:\mathop{\boxdot}\phi\in\Psi_{R}$ then, there is $a^{\prime}\in X^{\prime}_{A}$ such that $a\mathbin{\trianglelefteq}_{{\textrm{var}}(\phi)}a^{\prime},a^{\prime}:{-}\phi\in\Psi_{L}$. Assume that $a:\mathop{\boxdot}\phi\in\Psi_{R}$. Suppose, by contradiction, that for every $a^{\prime}\in X^{\prime}_{A}$ either $a\mathbin{\trianglelefteq}_{{\textrm{var}}(\phi)}a^{\prime}\notin\Psi_{L}$ or $a^{\prime}:{-}\phi\notin\Psi_{L}$. In both cases, rule $(\textrm{SCR})$ was not applied to $a:\mathop{\boxdot}\phi$. Then $a:\mathop{\boxdot}\phi$ is in $\Delta^{\prime}_{n}$. Consider the branch $\Gamma^{\prime}_{1}\to\Delta^{\prime}_{1}\cdots\Gamma^{\prime}_{n}\to\Delta^{\prime}_{n}\ a\mathbin{\trianglelefteq}_{{\textrm{var}}(\phi)}b,b:{-}\phi,\Gamma^{\prime}_{n}\to(\Delta^{\prime}_{n}\setminus\{a:\mathop{\boxdot}\phi\})$ using in the last step the rule $(\textrm{SCR})$ where $b$ is not in $\Gamma^{\prime}_{n}\cup\Delta^{\prime}_{n}$. Observe that this branch is still analytical. So the original branch is not exhausted which contradicts the hypothesis. 13. 13.

If $a:\mathop{\boxdot}\phi\in\Psi_{L}$ then, for each $a^{\prime}\in X^{\prime}_{A}$ either $a\mathbin{\trianglelefteq}_{{\textrm{var}}(\phi)}a^{\prime}\in\Psi_{R}$ or $a^{\prime}:{-}\phi\in\Psi_{R}$. Assume that $a:\mathop{\boxdot}\phi\in\Psi_{L}$. Suppose, by contradiction, that there is $a^{\prime}\in X^{\prime}_{A}$ such that $a\mathbin{\trianglelefteq}_{{\textrm{var}}(\phi)}a^{\prime}\notin\Psi_{R}$ and $a^{\prime}:{-}\phi\notin\Psi_{R}$. Observe that $a:\mathop{\boxdot}\phi$ is in $\Gamma^{\prime}_{n}$. Consider the branch $\Gamma^{\prime}_{1}\to\Delta^{\prime}_{1}\cdots\Gamma^{\prime}_{n}\to\Delta^{\prime}_{n}\ \Gamma^{\prime}_{n}\to\Delta^{\prime}_{n},a\mathbin{\trianglelefteq}_{{\textrm{var}}(\phi)}a^{\prime}$ using in the last step the rule $(\textrm{SCL})$. Observe that this branch is still analytical. So the original branch is not exhausted which contradicts the hypothesis. 14. 14.

If $\phi\in\Psi_{R}$ then either there exists $a^{\prime}\in X^{\prime}_{A}$ such that $a^{\prime}:{-}\phi,a^{\prime}:\mathop{\boxdot}{-}\phi\in\Psi_{L}$ or for each $a\in X^{\prime}_{A}$ either $a:\phi\in\Psi_{R}$ or $a:\mathop{\boxdot}\phi\in\Psi_{R}$. Suppose that $\phi\in\Psi_{R}$. Assume, by contradiction, that the thesis does not hold. Then, $\phi\in\Delta^{\prime}_{n}$ since rule $(\textrm{SKR})$ was not applied to $\phi$ in the branch. Consider the branch $\Gamma^{\prime}_{1}\to\Delta^{\prime}_{1}\cdots\Gamma^{\prime}_{n}\to\Delta^{\prime}_{n}\ b:{-}\phi,b:\mathop{\boxdot}{-}\phi,\Gamma^{\prime}_{n}\to\Delta^{\prime}_{n}$ using in the last step the rule $(\textrm{SKR})$ where $b$ is not in $\Gamma^{\prime}_{n}\cup\Delta^{\prime}_{n}$. Observe that this branch is still analytical. So the original branch is not exhausted which contradicts the hypothesis. 15. 15.

If $\phi\in\Psi_{L}$ then there is $a^{\prime}\in X^{\prime}_{A}$ such that $a^{\prime}:\phi,a^{\prime}:\mathop{\boxdot}\phi\in\Psi_{L}$ and for each $a\in X^{\prime}_{A}$ either $a:{-}\phi\in\Psi_{R}$ or $a:\mathop{\boxdot}{-}\phi\in\Psi_{R}$. Assume that $\phi\in\Psi_{L}$. Suppose, by contradiction and with no loss of generality, that for every $a^{\prime}\in X^{\prime}_{A}$, either $a^{\prime}:\phi\notin\Psi_{L}$ or $a^{\prime}:\mathop{\boxdot}\phi\notin\Psi_{L}$. Then rule $(\textrm{KL})$ was not applied in the branch to $\phi$. Hence, $\phi$ is in $\Gamma^{\prime}_{n}$. Consider the branch $\Gamma^{\prime}_{1}\to\Delta^{\prime}_{1}\cdots\Gamma^{\prime}_{n}\to\Delta^{\prime}_{n}\ b:\phi,b:\mathop{\boxdot}\phi,\Gamma^{\prime}_{n}\to\Delta^{\prime}_{n}$ using in the last step the rule $(\textrm{KL})$ where $b$ is not in $\Gamma^{\prime}_{n}\cup\Delta^{\prime}_{n}$. Observe that this branch is still analytical. So the original branch is not exhausted which contradicts the hypothesis. 16. 16.

If $a::(\phi_{1},\dots,\phi_{n}/\phi)\in\Psi_{R}$ then if $\phi_{1},\dots,\phi_{n}\in\Psi_{L}$ then $a:\phi\in\Psi_{R}$. Assume that $a::(\phi_{1},\dots,\phi_{n}/\phi)\in\Psi_{R}$ and $\phi_{1},\dots,\phi_{n}\in\Psi_{L}$. Assume, by contradiction, that $a:\phi\notin\Psi_{R}$. Then rule $(\textrm{CR}1)$ was not applied in the branch to $a::(\phi_{1},\dots,\phi_{n}/\phi)$. Hence, $a::(\phi_{1},\dots,\phi_{n}/\phi)$ is in $\Delta^{\prime}_{n}$. Consider the branch $\Gamma^{\prime}_{1}\to\Delta^{\prime}_{1}\cdots\Gamma^{\prime}_{n}\to\Delta^{\prime}_{n}\ \phi_{1},\dots,\phi_{n},\Gamma^{\prime}_{n}\to\Delta^{\prime}_{n},a:\phi$ using in the last step the rule $(\textrm{CR}1)$. Observe that this branch is still analytical. So the original branch is not exhausted which contradicts the hypothesis. 17. 17.

If $a::(\phi_{1},\dots,\phi_{n}/\phi)\in\Psi_{L}$ then either $\phi_{i}\in\Psi_{R}$ for some $i=1,\dots,n$ or $a:\phi\in\Psi_{L}$. Suppose that $a::(\phi_{1},\dots,\phi_{n}/\phi)\in\Psi_{L}$. Assume, by contradiction, that $\phi_{i}\notin\Psi_{R}$ for every $i=1,\dots,n$ and $a:\phi\notin\Psi_{L}$. Then rule $(\textrm{CR}2)$ was not applied in the branch to $a::(\phi_{1},\dots,\phi_{n}/\phi)$. Hence, $a::(\phi_{1},\dots,\phi_{n}/\phi)$ is in $\Gamma^{\prime}_{n}$. Consider the branch $\Gamma^{\prime}_{1}\to\Delta^{\prime}_{1}\cdots\Gamma^{\prime}_{n}\to\Delta^{\prime}_{n}\ \Gamma^{\prime}_{n}\to\Delta^{\prime}_{n},\phi_{1}$ using in the last step the rule $(\textrm{CR}2)$. Observe that this branch is still analytical. So the original branch is not exhausted which contradicts the hypothesis.

QED