# Trace Equivalence and Epistemic Logic to Express Security Properties

## TL;DR

This paper explores the use of trace equivalence and epistemic logic within process algebras to accurately formalize and verify security properties, bridging the gap between intuitive security notions and formal methods.

## Contribution

It demonstrates that trace equivalence is congruent and aligns with logical equivalence in epistemic logic, providing a formal foundation for security verification.

## Key findings

- Trace equivalence is congruent.
- Logical equivalence matches trace equivalence.
- Trace equivalence is relevant with non-adaptive attackers.

## Abstract

In process algebras, security properties are expressed as equivalences between processes, but which equivalence is suitable is not clear. This means that there is a gap between an intuitive security notion and the formulation. Appropriate formalization is essential for verification, and our purpose is bridging this gap. By chasing scope extrusions, we prove that trace equivalence is congruent. Moreover, we construct an epistemic logic for the applied pi calculus and show that its logical equivalence agrees with the trace equivalence. We use the epistemic logic to show that trace equivalence is pertinent in the presence of a non-adaptive attacker.