Skip to Main content Skip to Navigation
Conference papers

Trace Equivalence and Epistemic Logic to Express Security Properties

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.
Complete list of metadata

https://hal.inria.fr/hal-03283228
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Friday, July 9, 2021 - 5:53:26 PM
Last modification on : Friday, July 9, 2021 - 5:57:32 PM
Long-term archiving on: : Sunday, October 10, 2021 - 8:27:57 PM

File

 Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed until : 2023-01-01

Please log in to resquest access to the document

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

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⟩

Share

Metrics

Record views

16