# Trace Equivalence and Epistemic Logic to Express Security Properties

Kiraku Minami

► To cite this version:

Kiraku Minami. Trace Equivalence and Epistemic Logic to Express Security Properties. 40th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2020, Valletta, Malta. pp.115-132, 10.1007/978-3-030-50086-3_7. hal-03283228

HAL Id: hal-03283228

https://inria.hal.science/hal-03283228

Submitted on 9 Jul 2021

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Trace Equivalence and Epistemic Logic to Express Security Properties*

Kiraku Minami$^{[0000-0002-4434-4222]}$

Kyoto University, Kyoto 606-8502, Japan
kminami@kurims.kyoto-u.ac.jp

**Abstract.** In process algebra, we can express security properties using an equivalence on processes. However, it is not clear which equivalence is the most suitable for the purpose. Indeed, several definitions of some properties are proposed. For example, the definition of privacy is not unique. This situation means that we are not certain how to express an intuitive security notion. Namely, there is a gap between an intuitive security notion and the formulation. Proper formalization is essential for verification, and our purpose is to bridge this gap.

In the case of the applied pi calculus, an outputted message is not explicitly expressed. This feature suggests that trace equivalence appropriately expresses indistinguishability for attackers in the applied pi calculus. By chasing interchanging bound names and scope extrusions, we prove that trace equivalence is a congruence. Therefore, a security property expressed using trace equivalence is preserved by application of contexts. Moreover, we construct an epistemic logic for the applied pi calculus. We show that its logical equivalence agrees with trace equivalence. It means that trace equivalence is suitable in the presence of a non-adaptive attacker. Besides, we define several security properties to use our epistemic logic.

**Keywords:** Applied pi calculus · Trace equivalence · Epistemic logic

# 1 Introduction

## 1.1 Background

In modern society, information technology is indispensable to our daily lives, and many communication protocols are developed to transmit data securely. Verification of security properties of each protocol is essential, but it is not easy.

In the first place, how to formalize security notions is not clear. Various definitions of the same security property have been proposed, we will show an example later. One of our goals is to provide foundations to express these properties in a rigorous way. Besides, how to model communication and concurrency is also not clear; many such models have also been developed. In this work, we focus on process algebra because it allows us to handle parallel composition naturally.

<footnote>* This work was partly supported by JST ERATO Grant Number JPMJER1603, Japan.</footnote>
In process calculi, common confidentiality properties such as secrecy are represented to use an equivalence on processes. Many equivalences exist (cf. [18]), but which is the most suitable for expressing confidentiality is not clear. For instance, Delaune et al. [13] defined privacy in electronic voting in terms of the applied pi calculus [1] as follows.

**Definition 1** ([13, Definition 9]). A voting protocol respects vote-privacy (or just privacy) if

$$S[V_A\{a/v\}|V_B\{b/v\}] \approx_l S[V_A\{b/v\}|V_B\{a/v\}]$$

for all possible votes a and b.

$V_A$ and $V_B$ denote the voters containing the free variable $v$. $S$ is an evaluation context. $S$ denotes other voters and authorities. Intuitively, when the protocol respects privacy, this definition states that an attacker cannot distinguish two situations where votes are swapped. Note that indistinguishability is expressed to use labeled bisimilarity $\approx_l$ in this definition. Is it the most suitable? This question is nontrivial. Indeed, Chadha et al. [7] gave another definition and claimed that trace equivalence is more suitable than bisimilarity to model privacy. We also claim that trace equivalence is more suitable to express security properties in the presence of non-adaptive attackers. Similar arguments are not abundant in previous work.

In the applied pi calculus, a process can send not only names but also terms, but we do not explicitly express sent messages. We indirectly represent them to use alias variables. This feature enables us to handle cryptographic protocols naturally and suggests that trace equivalence means indistinguishability for attackers. This is because attackers whom we consider can observe only labeled transitions. We recall the syntax and semantics of the applied pi calculus in §2.

Both bisimilarity and trace equivalence on labeled transition systems (LTSs) are well studied. However, trace equivalence in the applied pi calculus (and other variants of the pi calculus [26, 27]) has not drawn much attention. This is perhaps because trace equivalence is the coarsest among commonly used equivalences. However, security properties sometimes require that different processes are regarded as the same. For example, consider secrecy. We want to make two processes that send different messages indistinguishable. In the case, trace equivalence is enough, but bisimilarity is not always optimal because it is too strong. Bisimilarity requires that possible actions for each process are the same. However, a non-adaptive attacker cannot detect a difference in feasibility. Here, “non-adaptive” means that the attacker cannot control participants. Thereby, a fine equivalence such as bisimilarity is not always adequate. Bisimilarity is probably suitable for more powerful attackers.

Epistemic logic is often used to express confidentiality directly (e.g. [7, 25, 32]). For example, when a message $M$ sent by an agent $a$ is anonymous, we might say that an adversary cannot know who sent $M$. In epistemic logic, we can express it with a formula such as $\neg KSend(a, M)$. This logical formulation is close to our intuition. Nevertheless, research into an epistemic logic for the applied pi calculus is not abundant.
In this paper, we assume that attackers can observe only labeled transitions. Especially, they cannot observe what action participants' can do. This assumption is natural because attackers in this paper are non-adaptive. We also assume that an attacker can send messages to participants.

## 1.2 Contributions

We prove that trace equivalence for the applied pi calculus is a congruence in §3. Second, we give an epistemic logic that characterizes trace equivalence in §4. Besides, we define security properties such as role-interchangeability, secrecy [25, 32], and openness, using our epistemic logic. Moreover, we show that parallel composition does not generally preserve secrecy and openness.

Whereas, trace equivalence characterizes total secrecy, so application of contexts preserves it. We omit many proofs. See [28] for details.

Our results suggest that trace equivalence is more suitable to express (non-probabilistic) security notions than bisimilarity.

# 2 The Applied Pi Calculus

The applied pi calculus [1] is an extension of the pi-calculus [26, 27]. We can handle cryptographic protocols naturally to use it.

## 2.1 Syntax

Let $\Sigma$ be a signature equipped with an equational theory. Terms are made from names, variables, and function symbols. A term is ground when it contains no variables. We recall the syntax of the applied pi-calculus. Here, $M, N...$ range over terms, while $n$ on names and $x$ on variables.

$$ P, Q ::= 0 \mid \overline{M\langle N \rangle}.P \mid M(x).P \mid \nu n.P \mid \\ \text{if } M = N \text{ then } P \text{ else } Q \mid P + Q \mid P|Q \mid !P \\ A, B ::= P \mid \nu n.A \mid \nu x.A \mid A|B \mid \{M/x\} $$

$P, Q, ...$ are plain processes. $\nu$ is a binding operator. $|$ is a parallel composition operator. $+$ is a nondeterministic choice operator. Plain processes are similar to pi-calculus processes, but they are not the same. A pi-calculus process can send only a name. On the other hand, an applied pi calculus process can send a term. Besides, a channel consists of a term. An object of an input prefix is a variable, so names do not change while the process runs.

$A, B, ...$ are extended processes. We call $\{M/x\}$ an active substitution. This notion is peculiar to the applied pi calculus. An active substitution $\{M/x\}$ substitutes $M$ for $x$ in a neighbor process.

$fn(A)$ and $bn(A)$ denote the sets of free names and bound names of a process $A$, respectively. $fv$ and $bv$ are similar to them. If $fn(A) \cap bn(A) = \emptyset$ and no bound
names are restricted twice, we say that A is name-distinct. Variable-distinctness is defined similarly. n(M) denotes the set of names that appear in a term M. v(M) is similar to it.

The domain dom(A) of an extended process A is inductively defined below. If variables in neighbor concurrently running processes are in dom(A), the process A affects those variables. If fv(A) = dom(A), we say that A is closed.

$$
\begin{align*}
\operatorname{dom}(P) &= \emptyset, \quad \operatorname{dom}(\nu n.A) = \operatorname{dom}(A), \quad \operatorname{dom}(\nu x.A) = \operatorname{dom}(A) \setminus \{x\}, \\
\operatorname{dom}(A|B) &= \operatorname{dom}(A) \cup \operatorname{dom}(B), \quad \operatorname{dom}(\{M/x\}) = \{x\}
\end{align*}
$$

2.2 Semantics

A context is an expression containing one hole. An evaluation context is a con-
text whose hole is neither under a replication, a conditional branch, nor an
action prefix. Structural equivalence ≡ is the smallest equivalence relation on
extended processes that is closed under application of evaluation contexts and
α-conversion, such that:

$$
\begin{align*}
& A|0 \equiv A \quad (A|B)|C \equiv A|(B|C) \quad A|B \equiv B|A \\
& (\nu u.A)|B \equiv \nu u.(A|B) \quad \text{if } u \notin \text{fn}(B) \cup \text{fv}(B) \quad \nu u.\nu v.A \equiv \nu v.\nu u.A \quad !P \equiv P!P \\
& P+Q \equiv Q+P \quad \nu x.\{M/x\} \equiv 0 \quad A|\{M/x\} \equiv A[M/x]|\{M/x\} \\
& \phantom{P+Q \equiv} \{M/x\} \equiv \{N/x\} \quad \text{if } \Sigma \vdash M = N
\end{align*}
$$

The second from the last represents how an active substitution {$M/x$} acts.

**Definition 2.** *Internal reduction* $\rightarrow$ *is the smallest relation on extended processes closed under structural equivalence and application of evaluation contexts, such that:*

$$
\text{if } M = N \text{ then } P \text{ else } Q \to P \quad \text{when } \Sigma \vdash M = N
$$

$$
\text{if } M = N \text{ then } P \text{ else } Q \to Q \quad \text{when } \Sigma \nvdash M = N
$$

$P + Q \to P$

$$
\overline{M \langle N \rangle . P \mid M(x) . Q \to P \mid Q[N/x],
$$

where terms *M* and *N* in the second rule are ground.

The last line represents synchronous communication on a channel M. We
emphasize that an environment cannot observe what is interchanged.

Next, we recall labeled semantics and requisite equivalence relations.

$$
\begin{tikzcd}
& \overline{M(x).P \xrightarrow{M(N)} P[N/x]} \arrow[d, "x \notin \text{fv}(\overline{M\langle N \rangle}.P)"'] \\
A \arrow[r, "\alpha"'] & A' \arrow[r, "u"'] & u \text{ does not appear in } \alpha. \arrow[d, "\nu u.A \xrightarrow{\alpha} \nu u.A'"']
\end{tikzcd}
$$
$$ \frac{A \xrightarrow{\alpha} A' \quad \text{bv}(\alpha) \cap \text{fv}(B) = \emptyset}{A|B \xrightarrow{\alpha} A'|B} \qquad \frac{A \equiv A' \quad A' \xrightarrow{\alpha} B' \quad B' \equiv B}{A \xrightarrow{\alpha} B} $$

The second rule represents an output. Note that an active substitution {$N/x$} is generated. The term $N$ does not appear in the action label $\nu x. \overline{M}\langle x \rangle$.

A frame is an extended process generated from 0 and active substitutions to use restriction and parallel composition. $\text{fr}(A)$ denotes a process obtained by replacing plain processes in $A$ with 0, and we call it a frame of $A$. We can consider that $\text{fr}(A)$ is a list of outputted messages.

$\mu$ is an action. We define $\implies$ as the transitive reflexive closure of $\to$, and $\xrightarrow{\alpha}$ as $\implies \xrightarrow{\alpha} \implies$. $\xrightarrow{\mu}$ is the former when $\mu$ is silent and is the latter otherwise.

**Definition 3.** ($M = N$) $\varphi \stackrel{\text{def}}{\implies} \text{v}(M) \cup \text{v}(N) \subseteq \text{dom}(\varphi)$ and $M\sigma = N\sigma$ where $\varphi \equiv \nu \tilde{n}.\sigma$ and $\tilde{n} \cap n(M, N) = \emptyset$ for some names $\tilde{n}$ and active substitutions $\sigma$.

($M = N$) $\varphi$ means that an attacker cannot distinguish $M$ and $N$ to use $\varphi$.

**Definition 4.** The static equivalence on closed frames is given by

$$ \varphi \approx_s \psi \stackrel{\text{def}}{\implies} \text{dom}(\varphi) = \text{dom}(\psi) \text{ and } \forall M, N; (M = N) \varphi \Leftrightarrow (M = N) \psi $$

for closed frames $\varphi$ and $\psi$. The static equivalence on closed processes is given by

$$ A \approx_s B \stackrel{\text{def}}{\implies} \text{fr}(A) \approx_s \text{fr}(B) $$

for closed processes $A$ and $B$.

Static equivalence means that an attacker has the same information about which terms are equal.

**Definition 5.** A trace tr is a finite derivation tr = $A_0 \xrightarrow{\mu_1} \dots \xrightarrow{\mu_n} A_n$ such that every $A_i$ is closed and $\text{fv}(\mu_i) \subseteq \text{dom}(A_{i-1})$ for all $i$. If $A_n$ can perform no actions, the trace tr is said to be complete or maximal. Given a trace tr, let $\text{tr}[i]$ be its i-th process $A_i$, and $\text{tr}[i, j]$ be the trace $A_i \xrightarrow{\mu_{i+1}} \dots \xrightarrow{\mu_j} A_j$ where $0 \le i \le j \le n$. The length of the trace tr is denoted by $|\text{tr}| = n$.

**Definition 6.** Let tr be a trace $A_0 \xrightarrow{\mu_1} \dots \xrightarrow{\mu_n} A_n$ and tr' be a trace $B_0 \xrightarrow{\mu'_1} \dots \xrightarrow{\mu'_m} B_m$. Static equivalence between tr and tr' is defined as below:

$$ \text{tr} \sim_t \text{tr}' \stackrel{\text{def}}{\implies} n = m \text{ and } \mu_i = \mu'_i \text{ and } A_i \approx_s B_i \text{ for all } i. $$

An attacker cannot distinguish statically equivalent traces. $\text{tr}(A)$ is a set of traces of $A$. $\text{tr}_{\text{max}}(A)$ is a set of maximal traces of $A$.

**Definition 7.** Let $A$ and $B$ be closed processes.

$$ A \subseteq_t B \stackrel{\text{def}}{\implies} \forall \text{tr} \in \text{tr}(A) \exists \text{tr}' \in \text{tr}(B) \text{ s.t. } \text{tr} \sim_t \text{tr}', $$

$$ A \approx_t B \stackrel{\text{def}}{\implies} A \subseteq_t B \text{ and } B \subseteq_t A. $$

Let $A$ and $B$ be two processes. Let $\sigma$ be a map that maps variables in $(\text{fv}(A) \setminus \text{dom}(A)) \cup (\text{fv}(B) \setminus \text{dom}(B))$ to ground terms. When $A\sigma \approx_t B\sigma$ holds for every such $\sigma$, we also denote it as $A \approx_t B$.
$A \subseteq_t B$ means that each trace of A is imitated by some trace of B.

We later show that non-adaptive active attackers cannot distinguish trace equivalent processes.

Trace equivalence is undecidable. However, if processes contain no replications and the equational theory on $\Sigma$ is a subterm convergent destructor rewriting system, trace equivalence is coNEXP complete [9].

## 3 Congruency of Trace Equivalence

The theorem below is our main result. It holds that trace equivalence is a congruence even though trace equivalence for the pi-calculus is not a congruence. This is ascribed to the difference between the pi-calculus and the applied pi calculus, namely, to the fact that names and variables are distinguished in the applied pi calculus. This is why adding an input prefix does not break trace equivalence. Besides, a scheme of late instantiation for an input transition is used in pi-calculus [26, 27], so parallel composition may break trace equivalence. On the other hand, a scheme of early instantiation is used in the applied pi calculus. This scheme enables us to decompose a trace of a parallel composed process into traces of component processes.

**Example 1.** We consider pi-calculus. We put

$$P = z(z')|\bar{yy'}.\bar{w}w', \quad Q = z(z').\bar{yy'}.\bar{w}w' + \bar{yy'}.z(z').\bar{w}w' + \bar{yy'}.\bar{w}w'.z(z').$$

Then, $x(z).P$ and $x(z).Q$ are trace equivalent, but $\bar{xy}|x(z).P$ and $\bar{xy}|x(z).Q$ are not trace equivalent. On the other hand, $x(z).P$ and $x(z).Q$ are not trace equivalent in the applied pi calculus because instantiation is early.

Abadi et al. [1] defined partial normal forms to prove that labeled bisimilarity is closed by application of closing evaluation contexts. They gave an operational semantics on partial normal forms. They classified transitions between ordinal processes into six cases to use partial normal forms.

To prove the next theorem, we use partial normal forms and define concurrent normal forms of traces. Transitions in a concurrent normal trace have to be particular forms.

Abadi et al. [1] studied decomposition and composition of reductions on partial normal forms. We study decomposition and composition of concurrent normal traces.

**Theorem 1.** $\approx_t$ is a congruence.

The proof is very long and complicated, so we only present an outline of our proof for the proposition below. Other cases are easy. The proof is given in [28].

**Proposition 1.** $A \approx_t B \Rightarrow A|C \approx_t B|C$.

*Proof outline.* First, we define concurrent normal forms. A concurrent normal form is a particular form of a trace of a parallel composed process. A concurrent
normal trace captures changes of scopes of bound names. Each process in a concurrent normal trace is of the form $\nu\tilde{r}s.(\nu\tilde{x}.(\sigma|P)\rho | \nu\tilde{y}.(\rho|Q)\sigma)$, where $\sigma$ and $\rho$ are (active) substitutions. Terms sent by the left process are accumulated in $\sigma$. Bound names sent by the left process $P$ are accumulated in $\tilde{s}$. Symmetric cases are similar.

Second, for any trace $t$ of $A|C$, we prove that there exists a concurrent normal trace $t'$ of $A|C$ such that $t \sim_t t'$.

Third, given a concurrent normal trace $\mathbf{tr}$ of $A|C$, we prove that we can construct traces of $A$ and $C$ which each process in them is of the form $\nu\tilde{s}.(\sigma|P)\rho$ or $\nu\tilde{r}.(\rho|Q)\sigma$.

Finally, we take a trace $\mathbf{tr}'$ of $B$ which is statically equivalent to the extracted trace of $A$ as the above, combine it with $\mathbf{tr}'$, and prove that the result is statically equivalent to the given trace $\mathbf{tr}$. $\square$

**Example 2.** Let $h$ be a unary function symbol which cannot be inverted.

$$ \nu m.a(x).\bar{x}\langle m \rangle \approx_t \nu m.a(x).\bar{x}\langle h(m) \rangle \text{ holds. Then,} $$

$$ \nu m.a(x).\bar{x}\langle m \rangle | \nu n.\bar{a}\langle n \rangle.n(y).\bar{b}\langle y \rangle \approx_t \nu m.a(x).\bar{x}\langle h(m) \rangle | \nu n.\bar{a}\langle n \rangle.n(y).\bar{b}\langle y \rangle $$

is shown as follows.

We arbitrarily take a trace $\mathbf{tr}$ of the left hand side. We consider

$$ \mathbf{tr} : \nu m.a(x).\bar{x}\langle m \rangle | \nu n.\bar{a}\langle n \rangle.n(y).\bar{b}\langle y \rangle $$

$$ \xrightarrow{\nu z.\bar{a}\langle z \rangle} \nu m.a(x).\bar{x}\langle m \rangle | \nu n.(n(y).\bar{b}\langle y \rangle | \{n/z\}) $$

$$ \xrightarrow{a(z)} \nu mn.(\bar{n}\langle m \rangle | n(y).\bar{b}\langle y \rangle | \{n/z\}) $$

$$ \rightarrow \nu mn.(\bar{b}\langle m \rangle | \{n/z\}) $$

$$ \xrightarrow{\nu w.\bar{b}\langle w \rangle} \nu mn.\{n/z, m/w\} $$

as an example. We transform it into a concurrent normal form.

$$ \mathbf{tr}' : \nu m.a(x).\bar{x}\langle m \rangle | \nu n.\bar{a}\langle n \rangle.n(y).\bar{b}\langle y \rangle $$

$$ \xrightarrow{\nu z.\bar{a}\langle z \rangle} \nu n.((\nu m.a(x).\bar{x}\langle m \rangle)[n/z] | n(y).\bar{b}\langle y \rangle | \{n/z\}) $$

$$ \xrightarrow{a(z)} \nu n.((\nu m.\bar{z}\langle m \rangle)[n/z] | n(y).\bar{b}\langle y \rangle | \{n/z\}) $$

$$ \rightarrow \nu nm.((\nu v.\{m/v\})[n/z] | (\bar{b}\langle v \rangle | \{n/z\})[m/v]) $$

$$ \xrightarrow{\nu w.\bar{b}\langle w \rangle} \nu nm.((\nu v.\{m/v\})[n/z, v/w] | \{n/z, v/w\}[m/v]) $$

Next, we decompose it into traces of component processes.

$$ \mathbf{tr}_1 : \nu m.a(x).\bar{x}\langle m \rangle $$

$$ \xrightarrow{a(n)} (\nu m.\bar{z}\langle m \rangle)[n/z] $$

$$ \xrightarrow{\nu v.\bar{n}\langle v \rangle} (\nu m.\{m/v\})[n/z] $$

$$ \mathbf{tr}_2 : \nu n.\bar{a}\langle n \rangle.n(y).\bar{b}\langle y \rangle $$

$$ \xrightarrow{\nu z.\bar{a}\langle z \rangle} \nu n.(n(y).\bar{b}\langle y \rangle | \{n/z\}) $$

$$ \xrightarrow{z(m)} \nu n.(\bar{b}\langle v \rangle | \{n/z\})[m/v] $$

$$ \xrightarrow{\nu w.\bar{b}\langle w \rangle} \nu n.\{n/z, v/w\}[m/v] $$
Since $\nu m.a(x).\bar{x}\langle m\rangle \approx_t \nu m.a(x).\bar{x}\langle h(m)\rangle$ holds, we can take a trace of $\nu m.a(x).\bar{x}\langle h(m)\rangle$ which is statically equivalent to the former.

$$ \begin{aligned} \mathbf{tr}_3 : & \nu m.a(x).\bar{x}\langle h(m)\rangle \\ & \xrightarrow{a(n)} (\nu m.\bar{z}\langle h(m)\rangle)[n/z] \\ & \xrightarrow{\nu v.\bar{n}\langle v\rangle} (\nu m.\{h(m)/v\})[n/z] \end{aligned} $$

Finally, we compose $\mathbf{tr}_2$ and $\mathbf{tr}_3$ and obtain a desired trace $\mathbf{tr}_4$.

$$ \begin{aligned} \mathbf{tr}_4 : & \nu m.a(x).\bar{x}\langle h(m)\rangle | \nu n.\bar{a}\langle n\rangle.n(y).\bar{b}\langle y\rangle \\ & \xrightarrow{\nu z.\bar{a}\langle z\rangle} \nu n.((\nu m.a(x).\bar{x}\langle h(m)\rangle)[n/z] | n(y).\bar{b}\langle y\rangle | \{n/z\}) \\ & \xrightarrow{a(z)} \nu n.((\nu m.\bar{z}\langle h(m)\rangle)[n/z] | n(y).\bar{b}\langle y\rangle | \{n/z\}) \\ & \rightarrow \nu n.m.((\nu v.\{h(m)/v\})[n/z] | (\bar{b}\langle v\rangle | \{n/z\})[h(m)/v]) \\ & \xrightarrow{\nu w.\bar{b}\langle w\rangle} \nu n.m.((\nu v.\{h(m)/v\})[n/z, v/w] | \{n/z, v/w\}[h(m)/v]) \end{aligned} $$

Cheval et al. [10] established congruence property of trace equivalence for image-finite processes. They proved that trace equivalence is equivalent to may-testing equivalence for image-finite processes. On the other hand, taking all processes into account, may-testing equivalence does not imply trace equivalence. They gave a concrete counterexample. Thus, we cannot use the same technique.

# 4 An Epistemic Logic for the Applied Pi Calculus

## 4.1 Syntax

We propose an epistemic logic for the applied pi calculus. It was inspired by [7], but our logic is a bit different. We give syntax of formulas.

$$ \begin{aligned} \delta &::= \top | M_1 = M_2 | M \in \text{dom} | \delta_1 \lor \delta_2 | \neg \delta \\ \varphi &::= \delta | \varphi_1 \lor \varphi_2 | \neg \varphi | \langle \mu \rangle_{-} \varphi | F \varphi | K \varphi \end{aligned} $$

where $M_1, M_2$ and $M$ are terms, and $\mu$ is an action. We call $\delta$ a static formula and $\varphi$ a modal formula. A static formula $\delta$ mentions equality of terms. A modal formula $\varphi$ mentions traces.

$\langle \mu \rangle_{-} \varphi$ states that the previous action is $\mu$, and $\varphi$ holds just before observing $\mu$. $F\varphi$ states that $\varphi$ holds some time or other. The operator $K$ expresses an attacker's knowledge, i.e., $K\varphi$ means an attacker knows that $\varphi$ holds.

## 4.2 Semantics

Our logic is an LTL-like logic with an epistemic operator. Let $A$ be a name-variable-distinct process that $fv(A) \setminus \text{dom}(A) = \tilde{x}$, $\rho$ be an assignment which
maps $\tilde{x}$ to ground terms, $\mathbf{tr} \in \text{tr}(A\rho)$, $0 \le i \le |\mathbf{tr}|$, and $M_1$ and $M_2$ be terms.
Please remember that $\text{fr}(A)$ is a frame of $A$.

We suppose that $\delta$ and $\varphi$ contain no variables other than $\tilde{x} \cup \text{dom}(\mathbf{tr}[i])$. We omit semantics of logical operators. They are defined as expected.

$$A, \rho, \mathbf{tr}, i \models M_1 = M_2 \text{ iff } (M_1\rho = M_2\rho)\text{fr}(\mathbf{tr}[i])$$

$$A, \rho, \mathbf{tr}, i \models M \in \text{dom} \text{ iff } M \text{ is a variable } x, \text{ and } x \in \text{dom}(\mathbf{tr}[i])$$

$$A, \rho, \mathbf{tr}, i \models \langle\mu\rangle_{-\varphi} \text{ iff } \mathbf{tr}[i-1] \stackrel{\mu}{\Longrightarrow} \mathbf{tr}[i] \text{ in } \mathbf{tr} \text{ and } A, \rho, \mathbf{tr}, i-1 \models \varphi$$

$$A, \rho, \mathbf{tr}, i \models F\varphi \text{ iff } \exists j \ge i \text{ s.t. } A, \rho, \mathbf{tr}, j \models \varphi$$

$$A, \rho, \mathbf{tr}, i \models K\varphi \text{ iff } \forall \rho' \forall \mathbf{tr}' \in \text{tr}(A\rho'); \mathbf{tr}[0, i] \sim_t \mathbf{tr}'[0, i] \Rightarrow A, \rho', \mathbf{tr}', i \models \varphi$$

We suppose that an attacker does not know what terms are assigned to free variables before the process runs. Hence, the definition of $K$ contains a quantifier over assignments $\forall \rho'$. Recall that an attacker can observe only labeled transitions, so accessibility is defined based on static equivalence on traces.

We also define satisfiability of formulas containing free variables. We put $\tilde{y} = \text{dom}(\mathbf{tr}[i])$. We suppose that $\varphi$ contains no variables other than $\tilde{x}, \tilde{y}$, and $\tilde{z}$.

$$A, \rho, \mathbf{tr}, i \models \varphi(\tilde{x}, \tilde{y}, \tilde{z}) \text{ iff } \forall \tilde{M}; A, \rho, \mathbf{tr}, i \models \varphi(\tilde{x}, \tilde{y}, \tilde{M}),$$

where $\tilde{M}$ is a sequence of ground terms.

From now, we suppose that all processes are name-variable-distinct. We often omit restriction of a domain of definition. $D(\rho)$ is a domain of definition of $\rho$.

When a formula $\varphi$ is satisfied over all possible runs of a process $A$, we say that $A$ satisfies $\varphi$.

**Definition 8.** $A \models \varphi \stackrel{\text{def}}{\Longleftrightarrow} \forall \rho \forall \mathbf{tr} \in \text{tr}(A\rho); A, \rho, \mathbf{tr}, 0 \models \varphi$, where $D(\rho) = \text{fv}(A) \setminus \text{dom}(A)$.

**Definition 9.** $A \sqsubseteq_L B \stackrel{\text{def}}{\Longleftrightarrow} \forall \rho \forall \mathbf{tr} \in \text{tr}(A\rho) \exists \mathbf{tr}' \in \text{tr}(B\rho)$

$$\text{s.t. } \forall i \forall \varphi; [A, \rho, \mathbf{tr}, i \models \varphi \Leftrightarrow B, \rho, \mathbf{tr}', i \models \varphi],$$

$$\text{where } D(\rho) = (\text{fv}(A) \setminus \text{dom}(A)) \cup (\text{fv}(B) \setminus \text{dom}(B)).$$

$$A \equiv_L B \stackrel{\text{def}}{\Longleftrightarrow} A \sqsubseteq_L B \text{ and } B \sqsubseteq_L A.$$

## 4.3 Correspondence with trace equivalence

We prove that trace equivalent processes satisfy the same formulas.

**Theorem 2.** 1. $A \approx_t B \Rightarrow A \sqsubseteq_L B$; 2. $A \sqsubseteq_L B \Rightarrow A \sqsubseteq_t B$

*Proof.* Let $\tilde{x} = (\text{fv}(A) \setminus \text{dom}(A)) \cup (\text{fv}(B) \setminus \text{dom}(B))$.

1) We prove

$$\forall \rho \forall \mathbf{tr} \in \text{tr}(A\rho), \mathbf{tr}' \in \text{tr}(B\rho);$$

$$\mathbf{tr} \sim_t \mathbf{tr}' \Rightarrow \forall i \forall \varphi; [A, \rho, \mathbf{tr}, i \models \varphi \Leftrightarrow B, \rho, \mathbf{tr}', i \models \varphi],$$
where $D(\rho) = \tilde{x}$, by induction on the syntax of formulas.

2) We arbitrarily take an assignment $\rho$ and $\mathbf{tr} \in \text{tr}(A\rho)$.

By $A \sqsubseteq_L B, \exists \mathbf{tr}' \in \text{tr}(B\rho) \text{ s.t. } \forall i \forall \varphi; [A, \rho, \mathbf{tr}, i \models \varphi \Leftrightarrow B, \rho, \mathbf{tr}', i \models \varphi]$.

Then, we can prove $\mathbf{tr} \sim_t \mathbf{tr}'$.

By arbitrariness of $\mathbf{tr}$, it immediately follows that $A \sqsubseteq_L B \Rightarrow A \subseteq_t B$. $\square$

**Theorem 3.** $A \approx_t B \Leftrightarrow A \equiv_L B$.

This theorem suggests that trace equivalence is suitable to define security properties. We give Proposition 2 as an example in the next subsection.

## 4.4 Applications

In this subsection, we often use abbreviations. Notably, $P$ expresses $\neg K\neg$, and $G$ expresses $\neg F\neg$. $P\varphi$ means that an attacker does not know $\varphi$ does not hold. In other words, the attacker thinks that the possibility that $\varphi$ holds remains.

We define minimal secrecy. We regard it as generalized minimal anonymity [25].

**Definition 10.** A variable $x$ is minimally secret with respect to $\delta$ in A iff $A \models G(\delta(x) \rightarrow P(\neg\delta(x)))$.

This definition means that attackers cannot know that $\delta(x)$ holds.

This property is very weak. For instance, although $x$ is minimally secret with respect to a nontrivial formula $\delta$, $x$ is not always minimally secret with respect to $\neg\delta$. Hereafter, we often omit objects.

*Example 3.* We put $\delta(z) : z \neq a \wedge z \neq b$.

We consider a process if $x = a$ then $\bar{c}$ else $\bar{d}$. Then $x$ is minimally secret with respect to $\delta$, but not secret with respect to $\neg\delta$.

Moreover, $\vee$ does not preserve minimally secret. However, $\wedge$ preserves it.

Although $x$ is minimally secret in $A$, $x$ is not always secret in $A|A$. Besides, restriction does not always preserve minimal secrecy.

*Example 4.* We put $\delta(z) : z = a$. We put

$$P = \text{if } x = a \text{ then } (\bar{a}\langle s \rangle + \bar{b}\langle s \rangle) \text{ else } \bar{a}\langle s \rangle, Q = \text{if } x = b \text{ then } \bar{b}\langle s \rangle \text{ else } \bar{c}\langle s \rangle.$$

Then $x$ is minimally secret with respect to $\delta$ in $P + Q$, but not secret in $(P + Q)|(P + Q)$.

*Example 5.* We put $\delta(z) : z = a$. Then, $x$ is minimally secret with respect to $\delta$ in $\bar{x} + \bar{a}$, but not secret in $\nu a.(\bar{x} + \bar{a})$. Here, we omitted objects.

We define total secrecy. We can also regard it as generalized total anonymity [25]. Total secrecy states attackers can obtain no information about $x$.
**Definition 11.** $x$ is totally secret in $A(x, \tilde{y})$ iff

$$ \forall \delta(z, \tilde{z}, \tilde{w}); A(x, \tilde{y}) \models G(\delta(x, \tilde{y}, \tilde{w}) \rightarrow P(\neg \delta(x, \tilde{y}, \tilde{w}))) $$

where $\delta$ contains no variables other than ones in $\{z\} \cup \tilde{z} \cup \tilde{w}$ and satisfies that $\forall \tilde{N} \forall \psi \exists M : \text{ground s.t. } \psi \models \neg \delta(M, \tilde{N}, \tilde{w})$. Besides, $|\tilde{y}| = |\tilde{z}|$ and $\tilde{w} \cap (\{x\} \cup \tilde{y}) = \emptyset$.

**Proposition 2.** $x$ is totally secret in $A(x, \tilde{y})$ iff $A(x, \tilde{y}) \approx_t A(x', \tilde{y})$.

*Proof. ⇒)* We suppose for the sake of contradiction that $A(x, \tilde{y}) \not\approx_t A(x', \tilde{y})$.

There exist $M_1, M_2$ and $\tilde{N}$ that are ground such that $A(M_1, \tilde{N}) \not\approx_t A(M_2, \tilde{N})$.

We suppose that $A(M_1, \tilde{N}) \not\subseteq_t A(M_2, \tilde{N})$. Then, there exists $\mathbf{tr} \in \text{tr}(A(M_1, \tilde{N}))$ such that any trace of $A(M_2, \tilde{N})$ is not statically equivalent to $\mathbf{tr}$.

We put $\delta(z, \tilde{z}) : z \neq M_2 \lor \tilde{z} \neq \tilde{N}$. Then

$$ A(x, \tilde{y}), (x \mapsto M_1, \tilde{y} \mapsto \tilde{N}), \mathbf{tr}, |\mathbf{tr}| \models K\delta(x, \tilde{y}). $$

This contradicts total secrecy.

換) We arbitrarily take $\delta, \rho, \mathbf{tr}$ and $i$, where $\delta$ meets the demand of Definition 11 and $D(\rho) = \{x\} \cup \tilde{y}$.

We suppose that $A(x, \tilde{y}), \rho, \mathbf{tr}, i \models \delta(x, \tilde{y}, \tilde{w})$.

We take $M$ such that $\text{fr}(\mathbf{tr}[i]) \models \neg \delta(M, \rho(\tilde{y}), \tilde{w})$. Let $\rho'$ be

$$ \rho'(y) = \begin{cases} M & (y = x) \\ \rho(y) & (\text{otherwise}). \end{cases} $$

By assumption, $A(\rho(x), \rho(\tilde{y})) \approx_t A(M, \rho(\tilde{y}))$.

Hence, there exists $\mathbf{tr}' \in \text{tr}(A(M, \rho(\tilde{y})))$ such that $\mathbf{tr} \sim_t \mathbf{tr}'$.

Then, $A(x, \tilde{y}), \rho', \mathbf{tr}', i \models \neg \delta(M, \rho(\tilde{y}), \tilde{w})$.

Therefore, $A(x, \tilde{y}), \rho, \mathbf{tr}, i \models P(\neg \delta(x, \rho(\tilde{y}), \tilde{w}))$.

Then, $A(x, \tilde{y}) \models G(\delta(x, \tilde{y}, \tilde{w}) \rightarrow P(\neg \delta(x, \rho(\tilde{y}), \tilde{w})))$.

□

**Theorem 4.** If $x$ is totally secret in $A(x, \tilde{y})$, then $x$ is also totally secret in $E[A(x, \tilde{y})]$ for every context $E[\_]$ which does not contain $x$.

Our framework can handle role interchangeability [25]. When $x_i$ satisfies a property $\delta_k$ and $x_l$ satisfies a property $\delta_j$, an attacker thinks that it is possible that $x_l$ satisfies a property $\delta_k$ and $x_i$ satisfies a property $\delta_j$.

**Definition 12.** We put $\text{fv}(A) \setminus \text{dom}(A) = \{x_1, ..., x_p\}$, $J = \{1, ..., q\}$, and $I = \{1, ..., p\}$. $(x_i, \delta_k)$ is role interchangeable regarding $\{\delta_j(z_j, \tilde{y}_j)\}_{j \in J}$ in A iff

$$ A(x_1, ..., x_p) \models G(\delta_k(x_i, \tilde{y}_k) \rightarrow \bigwedge_{l \in I} \bigwedge_{j \in J} (\delta_j(x_l, \tilde{y}_j) \rightarrow P(\delta_k(x_l, \tilde{y}_k) \wedge \delta_j(x_i, \tilde{y}_j)))) $$

where $\tilde{y}_j \cap \{x_1, ..., x_p\} = \emptyset$ for all $j \in J$.
**Proposition 3.**

$$ \forall \tilde{M} \quad \forall i \quad \forall \mathbf{tr} \in \mathrm{tr}(A(M_1, \dots, M_p)) $$

$$ \exists \tilde{N} \quad \exists \mathbf{tr}' \in \mathrm{tr}(A(M_i, N_2, \dots, N_{i-1}, M_1, N_{i+1}, \dots, N_p)) \quad \text{s.t. } \mathbf{tr} \sim_t \mathbf{tr}' $$

$\Leftrightarrow (x_1, \delta_k)$ is role interchangeable with respect to $\{\delta_j\}$ in A for all $\{\delta_j\}$ and k.

**Corollary 1.** $\forall l \in I \setminus \{i\}; A(x_1, \dots, x_i, \dots, x_l, \dots, x_p) \approx_t A(x_1, \dots, x_l, \dots, x_i, \dots, x_p) \Rightarrow (x_i, \delta_k)$ is role interchangeable with respect to $\{\delta_j\}$ in A for all $\{\delta_j\}$ and k.

The converse holds only when $p = 2$. We give a counterexample for $p = 3$.

*Example 6.* We put $A(x, y, z) = \begin{cases} x & \text{if } x = y \\ y & \text{if } x \neq y \end{cases}$ then $\bar{x} + \bar{z}$ else if $x = z$ then $\bar{x} + \bar{y}$ else $\bar{y} + \bar{z}$.

Then, $(x, \delta_k)$ is role interchangeable regarding $\{\delta_j\}$ in A for all $\{\delta_j\}_{j \in J}$ and $k$, but $A(a, b, a) \not\approx_t A(b, a, a)$. Thus, $A(x, y, z) \not\approx_t A(y, x, z)$.

We can also consider role permutativity. Mano [24] showed that it is strictly stronger than role interchangeability. Role permutativity states that even if $p$ values are swapped, an attacker cannot notice it.

**Definition 13.** We put $fv(A) \setminus \mathrm{dom}(A) = \{x_1, \dots, x_p\}$, $J = \{1, \dots, q\}$, and $I = \{1, \dots, p\}$. $\{\delta_j\}_{j \in J}$ is role permutable in A iff

$$ \forall n \le p \quad \forall \psi \in \mathfrak{S}_p; A(x_1, \dots, x_p) \models G\left(\bigwedge_{k \le n} \delta_{i_k}(x_{i_k}, \tilde{y}_k) \rightarrow P\left(\bigwedge_{k \le n} \delta_{i_k}(x_{i_{\psi(k)}}, \tilde{y}_k)\right)\right) $$

where $\tilde{y}_j \cap \{x_1, \dots, x_p\} = \emptyset$ for all $j$ and each $i_k$ differs.

**Proposition 4.** $\forall \psi \in \mathfrak{S}_p; A(x_1, \dots, x_p) \approx_t A(x_{\psi(1)}, \dots, x_{\psi(p)})$

$\Leftrightarrow \{\delta_j\}_{j \in J} \text{ is role permutable in A for all } \{\delta_j\}_{j \in J}.$

We define openness. We regard it as generalized identity [32]. Parallel composition does not preserve openness.

**Definition 14.** $x$ is open in A under $\Delta(x)$ iff

$$ \forall \rho \quad \forall \mathbf{tr} \in \mathrm{tr}_{\max}(A\rho); A, \rho, \mathbf{tr}, |\mathbf{tr}| \models \Delta(x) \rightarrow K(\Delta(x) \rightarrow (x = x\rho)). $$

*Example 7.* We put $\Delta(z) : z = r \lor z = s$. We put

$$ P = \begin{cases} \bar{a}\langle n \rangle & \text{if } x = r \\ \bar{b}\langle n \rangle & \text{if } x = s \end{cases} $$

Then $x$ is open in $P$ and $Q$ under $\Delta(x)$, but $x$ is not open in $P|Q$ under $\Delta(x)$.

**Problem 1.**

**Input:** An extended process $A$, an assignment $\rho$, a trace $\mathbf{tr} \in \mathrm{tr}(A)$, an integer $0 \le i \le |\mathbf{tr}|$, and a formula $\varphi$.

**Question:** Does $A, \rho, \mathbf{tr}, i \models \varphi$ hold?

**Proposition 5.** Even if the word problem in $\Sigma$ is decidable, Problem 1 can be undecidable.
Abadi and Cortier [2] proved that static equivalence can be undecidable even if the word problem in Σ is decidable. Proposition 5 follows from it.

We change semantics. We repeat the definition of satisfaction.

$$A \models \varphi \text{ iff } \forall \rho \ \forall \mathbf{tr} \in \mathrm{tr}(A\rho); A, \rho, \mathbf{tr}, 0 \models \varphi$$

Now, we restrict $\rho$ to be an assignment which maps free variables to only names and restrict inputted messages in $\mathbf{tr}$ to be only variables. That is, we assume that an attacker cannot tamper with a message. In other words, the attacker can only transfer messages without any change. Notably, the attacker cannot make a tuple of messages.

**Problem 2.**

**Input:** An extended process $A$ and a formula $\varphi$.

**Question:** Does $A \models \varphi$ hold?

A convergent subterm theory is an equational theory defined by finite equations whose each right-hand side is a proper subterm of the left-hand side.

**Proposition 6.** If the equational theory on $\Sigma$ is a convergent subterm theory and $A$ contains no replications, Problem 2 is decidable.

## 4.5 Comparison with the Work of Chadha et al.

Chadha et al. developed the definition of privacy in e-voting as follows. They considered protocol instances in which two voters Alice and Bob participate, and voting options are 0 and 1.

**Definition 15 ( [7, Definition 9]).** The voting process $V$ respects privacy if $V \models \mathbf{Aprivacy} \wedge \mathbf{Bprivacy}$ where

- $\mathbf{Aprivacy} \stackrel{\mathrm{def}}{=} \bigwedge_{v \in \{0,1\}} \Box (\mathbf{K}(\mathbf{Avote}(v)) \rightarrow \mathbf{Bvote}(v))$, and

- $\mathbf{Bprivacy} \stackrel{\mathrm{def}}{=} \bigwedge_{v \in \{0,1\}} \Box (\mathbf{K}(\mathbf{Bvote}(v)) \rightarrow \mathbf{Avote}(v))$.

$\mathbf{Avote}(v)$ means that Alice voted $v$, and $\mathbf{Bvote}(v)$ is similar.

Minimal secrecy of a vote never holds because an attacker trivially knows votes when all votes agree. We consider protocol instances in which $m$ voters participate and $n$ voting options exist. Let $v_i$ be a vote of $i$. We consider the property below:

$$\forall_{j,k} v_j \neq v_k \rightarrow \wedge_i \wedge_v G(K(v_i = v) \rightarrow v_1 = v \wedge \dots \wedge v_{i-1} = v \wedge v_{i+1} = v \wedge \dots \wedge v_m = v)$$

The consequence in $G(...)$ implies that $v_i \neq v$ due to the antecedent condition, so we can rewrite the property.

$$\forall_{j,k} v_j \neq v_k \rightarrow \wedge_i \wedge_v G(K(v_i = v) \rightarrow v_i \neq v)$$

Moreover, we take the contraposition in $G$.

$$\forall_{j,k} v_j \neq v_k \rightarrow \wedge_i \wedge_v G(v_i = v \rightarrow P(v_i \neq v))$$
This consequence is exactly minimal secrecy. Besides, minimal secrecy of vot-
ing implies privacy, so privacy and minimal secrecy of voting agree under the
disagreement condition $\vee_{j,k}v_j \neq v_k$.

It was shown that $V(\mathbf{0}, \mathbf{1}) \approx_t V(\mathbf{1}, \mathbf{0})$ implies that $\mathcal{V}$ respects privacy, and the
partial converse was given in [7]. We give several properties of minimal secrecy.

**Proposition 7.** We assume that a voting process $\mathcal{V}$ is equivalent for aborts, and minimal secrecy of each vote in $V(v_1, \dots, v_m)$ holds under the disagreement condition $\vee_{j,k}v_j \neq v_k$.

1. $m = 2 \Rightarrow V(v_1, v_2) \approx_t V(v_2, v_1)$.

2. $m = 3$ and $n = 2 \Rightarrow V(v_1, v_2, v_3) \approx_t V(v_2, v_1, v_3)$.

3. Otherwise, $V(v_1, \dots, v_i, \dots, v_j, \dots, v_m) \approx_t V(v_1, \dots, v_j, \dots, v_i, \dots, v_m)$ does not always hold.

# 5 Related Work

Logics about behavior of labeled transition systems originate from Hennessy-
Milner logic [20] that is a modal logic characterizing observational congruence.
That is, observational equivalent systems satisfy the same modal formulas when
these systems are image-finite.

Process algebra is a special LTS. The spi calculus [3] is an extension of the pi-calculus. It enables us to handle symmetric key encryption based on the Dolev-Yao model [14]. In the spi calculus, two ciphertexts obtained by encrypting two different plaintexts are indistinguishable unless an observer gets a secret key. Abadi and Gordon formalized security properties to use testing equivalence.

We focused on the applied pi calculus [1] because it is more powerful than the spi calculus. That is, we intend to handle more various security notions. In the calculus, a process can send not only names but also terms via alias variables. Due to this feature, we can handle not only secrecy but also stricter properties. The authors proved that observational equivalence and labeled bisimilarity correspond.

Chadha et al. [7] already developed an epistemic logic for the applied pi calculus. They defined formulas **Has** and $\hat{\text{evt}}$. **Has** directly represents attackers' knowledge, and $\hat{\text{evt}}$ means that a particular event had occurred. Temporal modalities were also used, but they do neither mention the just previous nor next action. The epistemic operator **K** was defined based on static equivalence on traces. Authors suggested that trace equivalence is more suitable than labeled bisimilarity when we consider privacy. However, a correspondent relation between logic and behavior of processes was not provided. As a matter of fact, α-equivalent processes do not always satisfy the same formulas in their framework because secret values are expressed as bound names or through events. In our framework, trace equivalent processes satisfy the same formulas.

Horne [21] introduced quasi-open bisimilarity, and he proved that it coincides open bisimilarity. Moreover, intuitionistic modal logic $\mathcal{FM}$ characterizes quasi-open bisimilarity. The law of excluded middle does not hold in the logic because processes containing a free variable are also considered.
Knight et al. [22] defined an epistemic logic for an LTS. This framework is based on Hennessy-Milner logic, and it handles multiple agents’ knowledge. They also proved weak completeness. However, compositionality was not discussed.

Process algebra is one of nominal transition systems. Parrow et al. [29] developed modal logic characterizing bisimilarity for a nominal transition system.

Toninho and Caires [31] proposed a dynamic spatial epistemic logic, which reasons what information a process can obtain. The epistemic operator means not only an attacker’s knowledge but also a participant’s knowledge, so, for example, the logic can reason a correspondence assertion.

Tsukada et al. [32] studied sequential and parallel compositionality of security notions to use an epistemic logic for a multiagent system. They proved that neither anonymity nor privacy is generally preserved by composition. They also gave a sufficient condition for preservation. However, this word “parallel” merely means that the same agent acts two actions in the paper. That is, concurrency was not considered.

Fiore and Abadi [16] developed symbolic models of processes. They gave a procedure to decide whether an environment can derive a message $M$. Their technique can be used for verification. However, equivalences on processes were not studied in the paper.

Clarkson and Schneider [12] generalized trace properties to hyperproperties, and Clarkson et al. [11] developed hyperLTL and hyperCTL* for hyperproperties. Hyperproperties can express security properties which cannot be expressed by trace properties. The authors regarded systems as sets of traces, so hyperproperties are properties about systems. Our security properties are also proper hyperproperties. The advantage of our work over these works is to relate trace equivalence to attackers’ knowledge. In [11, 12], the relation between the equivalence and knowledge is not clear.

Goubault-Larrecq et al. [19] proposed the probabilistic applied pi calculus. In this case, Theorem 1 no longer holds. It is known that trace distribution preorder [30] is not a congruence. On the other hand, it is shown in [5] that probabilistic trace equivalence for nondeterministic and probabilistic LTS is a congruence with respect to parallel composition. Probabilistic trace equivalence is coarser than trace distribution equivalence.

Canetti et al. [6] defined implementation for task-PIOAs. According to their definition, $T_1$ implements $T_2$ iff the set of behaviors of $T_1$ composed with $\mathcal{E}$ is included in the set of behaviors of $T_2$ composed with $\mathcal{E}$ for every environment $\mathcal{E}$. Here, behavior is the set of trace distributions. The implementation relation is preserved by parallel composition.

Giro and D’Argenio [17] pointed out that ordinary schedulers may give rise to unnatural behavior. A scheduler may leak information if it can look at the whole of the system. To solve this problem, they provided several reasonable subclasses of schedulers. The problem of the scheduler in the formalization of security properties was also pointed out in [4, 8], which proposed other approaches.

Eisentraut et al. [15] also studied subclasses of schedulers for probabilistic automata. They defined late distribution bisimulation and proved that late dis-
tribution bisimulation with respect to distributed schedulers is compositional. We may need to specify subclasses of schedulers to state a probabilistic variant of Theorem 1.

Knight et al. [23] developed spatial and epistemic process calculus. Their study is for concurrent constraint programming, so their processes can add constraints. They proved that observational equivalence is a congruence. Their processes do not have labeled actions, so observational equivalence means that equivalent processes provide the same results. On the other hand, in the applied pi calculus, trace equivalent processes provide equivalent traces and indistinguishable information.

In this paper, we characterized trace equivalence in terms of our epistemic logic. That is, we showed that a non-adaptive active intruder cannot distinguish trace equivalent processes. We also focused on how composition of systems affects security properties. We proved that any composition preserves total secrecy and role permutativity. This is because trace equivalence is a congruence.

# 6 Conclusion

## 6.1 Summary

In this paper, we provided an epistemic logic for the applied pi calculus. This logic is an LTL-like logic, so we can describe security notions. We formulated secrecy, role-interchangeability, and openness. These are generalized security properties regarding multiagent systems.

Moreover, we associated trace equivalence with total secrecy. Application of context does not preserve minimal secrecy, but total secrecy is preserved because trace equivalence is a congruence. We also give a necessary and sufficient condition for role-interchangeability.

We conclude that trace equivalence is suitable to express non-probabilistic indistinguishability in the view of security in the presence of a non-adaptive active adversary.

## 6.2 Future Work

First, our epistemic logic states an adversary's knowledge. We intend to construct a logic for a process's knowledge. It will bridge a gap between multiagent systems and process calculi.

Second, formalizations of other security properties such as non-malleability are also the next topics.

Finally, what logic is suitable for security in the presence of an adaptive attacker is still open.

# Acknowledgments

The author thanks Prof. M. Hasegawa and Prof. N. Yoshida for discussions. He also thanks the anonymous reviewers for helpful comments and suggestions.
References

1. Abadi, M., Blanchet, B., Fournet, C.: The applied pi calculus: Mobile values, new names, and secure communication. J. ACM 65(1), 1–41 (2017). https://doi.org/10.1145/3127586

2. Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theoretical Computer Science 367(1-2), 2–32 (2006). https://doi.org/10.1016/j.tcs.2006.08.032

3. Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. Information and computation 148(1), 1–70 (1999). https://doi.org/10.1006/inco.1998.2740

4. Alvim, M.S., Andrés, M.E., Palamidessi, C., van Rossum, P.: Safe equivalences for security properties. In: Calude, C.S., Sassone, V. (eds.) TCS 2010. IFIPAICT, vol. 323, pp. 55–70. Springer, Berlin, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15240-5_5

5. Bernardo, M., De Nicola, R., Loreti, M.: Revisiting Trace and Testing Equivalences for Nondeterministic and Probabilistic Processes. Logical Methods in Computer Science 10(1) (2014). https://doi.org/10.2168/LMCS-10(1:16)2014

6. Canetti, R., Cheung, L., Kaynar, D., Liskov, M., Lynch, N., Pereira, O., Segala, R.: Task-structured probabilistic i/o automata. Journal of Computer and System Sciences 94, 63 – 97 (2018). https://doi.org/10.1016/j.jcss.2017.09.007

7. Chadha, R., Delaune, S., Kremer, S.: Epistemic logic for the applied pi calculus. In: Lee, D., Lopes, A., Poetzsch-Heffter, A. (eds.) FMOODS/FORTE 2009. LNCS, vol. 5522, pp. 182–197. Springer, Berlin, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02138-1_12

8. Chatzikokolakis, K., Palamidessi, C.: Making random choices invisible to the scheduler. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 42–58. Springer, Berlin, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74407-8_4

9. Cheval, V., Kremer, S., Rakotonirina, I.: Deepsec: Deciding equivalence properties in security protocols theory and practice. In: SP 2018. pp. 529–546 (2018). https://doi.org/10.1109/SP.2018.00033

10. Cheval, V., Cortier, V., Delaune, S.: Deciding equivalence-based properties using constraint solving. Theoretical Computer Science 492, 1 – 39 (2013). https://doi.org/10.1016/j.tcs.2013.04.016

11. Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., Sánchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 265–284. Springer, Berlin, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54792-8_15

12. Clarkson, M.R., Schneider, F.B.: Hyperproperties. Journal of Computer Security 18(6), 1157–1210 (2010). https://doi.org/10.3233/JCS-2009-0393

13. Delaune, S., Kremer, S., Ryan, M.: Verifying privacy-type properties of electronic voting protocols. Journal of Computer Security 17(4), 435–487 (2009). https://doi.org/10.3233/JCS-2009-0340

14. Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983). https://doi.org/10.1109/TIT.1983.1056650

15. Eisentraut, C., Godskesen, J.C., Hermanns, H., Song, L., Zhang, L.: Probabilistic bisimulation for realistic schedulers. In: Bjørner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 248–264. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-19249-9_16
16. Fiore, M., Abadi, M.: Computing symbolic models for verifying cryptographic protocols. In: CSFW-14. pp. 160–173 (2001). https://doi.org/10.1109/CSFW.2001.930144

17. Giro, S., D'Argenio, P.: On the expressive power of schedulers in distributed probabilistic systems. Electronic Notes in Theoretical Computer Science 253(3), 45 – 71 (2009). https://doi.org/10.1016/j.entcs.2009.10.005

18. van Glabbeek, R.J.: The linear time - branching time spectrum. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 278–297. Springer, Berlin, Heidelberg (1990). https://doi.org/10.1007/BFb0039066

19. Goubault-Larrecq, J., Palamidessi, C., Troina, A.: A probabilistic applied pi-calculus. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 175–190. Springer, Berlin, Heidelberg (2007). https://doi.org/10.1007/978-3-540-76637-7_12

20. Hennessy, M., Milner, R.: On observing nondeterminism and concurrency. In: de Bakker, J., van Leeuwen, J. (eds.) Automata, Languages and Programming. LNCS, vol. 85, pp. 299–309. Springer, Berlin, Heidelberg (1980). https://doi.org/10.1007/3-540-10003-2_79

21. Horne, R.: A bisimilarity congruence for the applied pi-calculus sufficiently coarse to verify privacy properties. arXiv:1811.02536 (2018)

22. Knight, S., Mardare, R., Panangaden, P.: Combining epistemic logic and hennessy-milner logic. In: Constable, R.L., Silva, A. (eds.) Logic and Program Semantics, LNCS, vol. 7230, pp. 219–243. Springer, Berlin, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29485-3_14

23. Knight, S., Palamidessi, C., Panangaden, P., Valencia, F.D.: Spatial and epistemic modalities in constraint-based process calculi. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 317–332. Springer, Berlin, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32940-1_23

24. Mano, K.: Formal Specification and Verification of Anonymity and Privacy. Ph.D. thesis, Nagoya University (2013)

25. Mano, K., Kawabe, Y., Sakurada, H., Tsukada, Y.: Role interchange for anonymity and privacy of voting. Journal of Logic and Computation 20(6), 1251–1288 (2010). https://doi.org/10.1093/logcom/exq013

26. Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, i. Inf. Comput. 100(1), 1–40 (1992). https://doi.org/10.1016/0890-5401(92)90008-4

27. Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, ii. Inf. Comput. 100(1), 41–77 (1992). https://doi.org/10.1016/0890-5401(92)90009-5

28. Minami, K.: Trace equivalence and epistemic logic to express security properties. arXiv:1903.03719 (2019)

29. Parrow, J., Borgström, J., Eriksson, L.H., Gutkovas, R., Weber, T.: Modal Logics for Nominal Transition Systems. In: CONCUR 2015. LIPIcs, vol. 42, pp. 198–211. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2015). https://doi.org/10.4230/LIPIcs.CONCUR.2015.198

30. Segala, R.: A compositional trace-based semantics for probabilistic automata. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 234–248. Springer, Berlin, Heidelberg (1995). https://doi.org/10.1007/3-540-60218-6_17

31. Toninho, B., Caires, L.: A spatial-epistemic logic for reasoning about security protocols. In: SecCo 2010. EPTCS, vol. 51, pp. 1–15. Open Publishing Association (2011). https://doi.org/10.4204/EPTCS.51.1

32. Tsukada, Y., Sakurada, H., Mano, K., Manabe, Y.: On compositional reasoning about anonymity and privacy in epistemic logic. Annals of Mathematics and Artificial Intelligence 78(2), 101–129 (2016). https://doi.org/10.1007/s10472-016-9516-8