Trace Equivalence and Epistemic Logic to Express Security Properties
This work addresses a foundational gap in formal verification of security properties for process algebras, though it appears incremental as it builds on existing trace equivalence and epistemic logic frameworks.
The paper tackles the problem of unclear equivalence relations for expressing security properties in process algebras by proving trace equivalence is congruent and constructing an epistemic logic for the applied pi calculus, showing its logical equivalence agrees with trace equivalence and that trace equivalence is pertinent with non-adaptive attackers.
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.