key: cord-0045074-kprvifq2
authors: Minami, Kiraku
title: Trace Equivalence and Epistemic Logic to Express Security Properties
date: 2020-05-13
journal: Formal Techniques for Distributed Objects, Components, and Systems
DOI: 10.1007/978-3-030-50086-3_7
sha: 4488a07d6d10ea96e8c2c95ecf0d7d61d7baa99c
doc_id: 45074
cord_uid: kprvifq2

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.

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 This work was partly supported by JST ERATO Grant Number JPMJER1603, Japan. 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.

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.

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 ≈ 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 Sect. 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, "nonadaptive" 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 ¬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.

We prove that trace equivalence for the applied pi calculus is a congruence in Sect. 3. Second, we give an epistemic logic that characterizes trace equivalence in Sect. 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 (nonprobabilistic) security notions than bisimilarity.

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

Let Σ 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.

.. are plain processes. ν 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)∩bn(A) = ∅ 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.

A context is an expression containing one hole. An evaluation context is a context 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:

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

Internal reduction → is the smallest relation on extended processes closed under structural equivalence and application of evaluation contexts, such that:

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.

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 νx.M x .

A frame is an extended process generated from 0 and active substitutions to use restriction and parallel composition. 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 fr(A) is a list of outputted messages.

μ is an action. We define =⇒ as the transitive reflexive closure of −→, and

μ =⇒ is the former when μ is silent and is the latter otherwise.

and Mσ = Nσ where ϕ ≡ ν n.σ and n ∩ n(M, N ) = ∅ for some names n and active substitutions σ.

(M = N )ϕ means that an attacker cannot distinguish M and N to use ϕ.

for closed frames ϕ and ψ. The static equivalence on closed processes is given by

for closed processes A and B.

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

= A 0 μ1 =⇒ ... μn =⇒ A n such that every A i is closed and fv(μ i ) ⊆ dom(A i−1 ) for all i. If A n can perform no actions,

The length of the trace tr is denoted by |tr| = n. 

Let A and B be two processes. Let σ be a map that maps variables in (fv(A) \ dom(A)) ∪ (fv(B) \ dom(B)) to ground terms. When Aσ ≈ t Bσ holds for every such σ, we also denote it as A ≈ t B.

A ⊆ 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 Σ is a subterm convergent destructor rewriting system, trace equivalence is coNEXP complete [9] .

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.

We consider pi-calculus. We put P = z(z )|yy .ww , Q = z(z ).yy .ww + yy .z(z ).ww + yy .ww .z(z ).

Then, x(z).P and x(z).Q are trace equivalent, but xy|x(z).P and 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.

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] .

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 ν r s.(ν x.(σ|P )ρ | ν y.(ρ|Q)σ), where σ and ρ are (active) substitutions. Terms sent by the left process are accumulated in σ. Bound names sent by the left process P are accumulated in 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 ∼ t t .

Third, given a concurrent normal trace tr of A|C, we prove that we can construct traces of A and C which each process in them is of the form ν s.(σ|P )ρ or ν r.(ρ|Q)σ.

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

2

νm.a(x).x m | νn.a n .n(y).b y ≈ t νm.a(x).x h(m) | νn.a n .n(y).b y is shown as follows.

We arbitrarily take a trace tr of the left hand side. We consider tr :νm.a(x).x m | νn.a n .n(y).b y

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

tr :νm.a(x).x m | νn.a n .n(y).b y

Next, we decompose it into traces of component processes. 

x h(m) holds, we can take a trace of νm.a(x).x h(m) which is statically equivalent to the former.

Finally, we compose tr 2 and tr 3 and obtain a desired trace tr 4 .

Cheval et al. [10] established congruence property of trace equivalence for image-finite processes. They proved that trace equivalence is equivalent to maytesting 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.

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.

where M 1 , M 2 and M are terms, and μ is an action. We call δ a static formula and ϕ a modal formula. A static formula δ mentions equality of terms. A modal formula ϕ mentions traces.

μ − ϕ states that the previous action is μ, and ϕ holds just before observing μ. F ϕ states that ϕ holds some time or other. The operator K expresses an attacker's knowledge, i.e., Kϕ means an attacker knows that ϕ holds.

Our logic is an LTL-like logic with an epistemic operator. Let A be a namevariable-distinct process that fv(A) \ dom(A) = x, ρ be an assignment which maps x to ground terms, tr ∈ tr(Aρ), 0 ≤ i ≤ |tr|, and M 1 and M 2 be terms. Please remember that fr(A) is a frame of A.

We suppose that δ and ϕ contain no variables other than x ∪ dom(tr[i]). We omit semantics of logical operators. They are defined as expected.

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 ∀ρ . 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 y = dom(tr[i]). We suppose that ϕ contains no variables other than x, y, and z.

where 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(ρ) is a domain of definition of ρ.

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

We prove that trace equivalent processes satisfy the same formulas. dom(B) ).

∀ρ ∀tr ∈ tr(Aρ), tr ∈ tr(Bρ);

where D(ρ) = x, by induction on the syntax of formulas. 2) We arbitrarily take an assignment ρ and tr ∈ tr(Aρ).

By

Then, we can prove tr ∼ t tr . By arbitrariness of tr, it immediately follows that

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

In this subsection, we often use abbreviations. Notably, P expresses ¬K¬, and G expresses ¬F ¬. P ϕ means that an attacker does not know ϕ does not hold. In other words, the attacker thinks that the possibility that ϕ holds remains. We define minimal secrecy. We regard it as generalized minimal anonymity [25] .

This definition means that attackers cannot know that δ(x) holds. This property is very weak. For instance, although x is minimally secret with respect to a nontrivial formula δ, x is not always minimally secret with respect to ¬δ. Hereafter, we often omit objects.

We consider a process if x = a then c else d. Then x is minimally secret with respect to δ, but not secret with respect to ¬δ.

Moreover, ∨ does not preserve minimally secret. However, ∧ 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. Then x is minimally secret with respect to δ in P + Q, but not secret in (P + Q)|(P + Q).

Example 5. We put δ(z) : z = a. Then, x is minimally secret with respect to δ in x + a, but not secret in νa.(x + 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.

where δ contains no variables other than ones in {z} ∪ z ∪ w and satisfies that ∀ N ∀ψ∃M : ground s.t. ψ |= ¬δ(M, N, w) . Besides, | y| = | z| and w∩({x}∪ y) = ∅. A(x, y) iff A(x, y) ≈ t A(x , y) .

There exist M 1 , M 2 and N that are ground such that N ) . Then, there exists tr ∈ tr (A(M 1 , N ) ) such that any trace of A(M 2 , N ) is not statically equivalent to tr.

We put δ(z, z) :

This contradicts total secrecy. ⇐) We arbitrarily take δ, ρ, tr and i, where δ meets the demand of Definition 11 and D(ρ) = {x} ∪ y.

We suppose that A(x, y), ρ, tr, i |= δ(x, y, w).

We take M such that fr(tr[i]) |= ¬δ(M, ρ( y), w). Let ρ be ρ (y) = M (y = x) ρ(y) (otherwise).

Hence, there exists tr ∈ tr(A(M, ρ( y))) such that tr ∼ t tr . Then, A(x, y), ρ , tr , i |= ¬δ(M, ρ( y), w). Therefore, A(x, y), ρ, tr, i |= P (¬δ(x, ρ( y), w)). Then, A(x, y) |= G(δ(x, y, w) → P (¬δ(x, ρ( y), w))).

Our framework can handle role interchangeability [25] . When x i satisfies a property δ k and x l satisfies a property δ j , an attacker thinks that it is possible that x l satisfies a property δ k and x i satisfies a property δ j . 

where y j ∩ {x 1 , ..., x p } = ∅ for all j ∈ J. A(x 1 , ..., x i , ..., x l , ..., x p ) ≈ t A(x 1 , ..., x l , ..., x i , ..., x p 

The converse holds only when p = 2. We give a counterexample for p = 3. A(x, y, z) 

Then, (x, δ k ) is role interchangeable regarding {δ j } in A for all {δ j } j∈J and k, but A(a, b, a) ≈ t A(b, a, a) . Thus, A(x, y, z) ≈ 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. 

where y j ∩ {x 1 , ..., x p } = ∅ for all j and each i k differs.

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

Example 7. We put Δ(z) : z = r ∨ z = s. We put P = if x = r then a n else b n , Q = if x = r then b n else a n .

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

Input: An extended process A, an assignment ρ, a trace tr ∈ tr(A), an integer 0 ≤ i ≤ |tr|, and a formula ϕ.

Question: Does A, ρ, tr, i |= ϕ hold?

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 |= ϕ iff ∀ρ ∀tr ∈ tr(Aρ); A, ρ, tr, 0 |= ϕ Now, we restrict ρ to be an assignment which maps free variables to only names and restrict inputted messages in 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.

Input: An extended process A and a formula ϕ. Question: Does A |= ϕ 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.

If the equational theory on Σ is a convergent subterm theory and A contains no replications, Problem 2 is decidable. 

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:

The consequence in G(...) implies that v i = v due to the antecedent condition, so we can rewrite the property.

Moreover, we take the contraposition in G.

This consequence is exactly minimal secrecy. Besides, minimal secrecy of voting implies privacy, so privacy and minimal secrecy of voting agree under the disagreement condition ∨ j,k v j = v k .

It was shown that V (0, 1) ≈ t V (1, 0) implies that V respects privacy, and the partial converse was given in [7] . We give several properties of minimal secrecy.

We assume that a voting process V is equivalent for aborts, and minimal secrecy of each vote in V (v 1 , ..., v m ) holds under the disagreement ..., v j , ..., v i , ..., v m ) does not always hold.

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 evt. Has directly represents attackers' knowledge, and 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 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 E is included in the set of behaviors of T 2 composed with E for every environment 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 distribution 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.

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.

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.

The applied pi calculus: mobile values, new names, and secure communication

Deciding knowledge in security protocols under equational theories

A calculus for cryptographic protocols: the spi calculus

Safe equivalences for security properties

Revisiting trace and testing equivalences for nondeterministic and probabilistic processes

Task-structured probabilistic i/o automata

Epistemic logic for the applied pi calculus

Making random choices invisible to the scheduler

DEEPSEC: deciding equivalence properties in security protocols theory and practice

Deciding equivalence-based properties using constraint solving

Temporal logics for hyperproperties

Verifying privacy-type properties of electronic voting protocols

On the security of public key protocols

Probabilistic bisimulation for realistic schedulers

Computing symbolic models for verifying cryptographic protocols

On the expressive power of schedulers in distributed probabilistic systems

The linear time -branching time spectrum

A probabilistic applied picalculus

On observing nondeterminism and concurrency

A bisimilarity congruence for the applied pi-calculus sufficiently coarse to verify privacy properties

Combining epistemic logic and hennessymilner logic

Spatial and epistemic modalities in constraint-based process calculi

Formal specification and verification of anonymity and privacy

Role interchange for anonymity and privacy of voting

A calculus of mobile processes

A calculus of mobile processes

Trace equivalence and epistemic logic to express security properties

Modal logics for nominal transition systems

A compositional trace-based semantics for probabilistic automata

A spatial-epistemic logic for reasoning about security protocols

On compositional reasoning about anonymity and privacy in epistemic logic

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