## Abstract

We prove that three semantics for the applied π-calculus coincide – a testing semantics, a labelled equivalence, and a modal logic – and explain how design decisions in each of these semantics are objectively supported by this convergence. Each of these semantics has a distinct role when verifying security protocols. Testing semantics are suited to security and privacy problems expressed in terms of a process equivalence problem, where tests define the space of attack strategies. A labelled equivalence is suited to proving the given equivalence problem when such security and privacy properties hold; while, dually, the modal logic describes attacks when such security or privacy properties are violated. For this particular investigation into this good-practice design pattern, we select what is perhaps the most powerful (interleaving) testing semantics: open barbed bisimilarity. Selecting open barbed bisimilarity comes with the bonus that it is a congruence hence is suited to compositional reasoning. This reference testing semantics leads to a notion of quasi-open bisimilarity and an intuitionistic modal logic for the applied π-calculus. We argue that, since we characterise the finest (interleaving) testing semantics and tests are attack strategies, our intuitionistic modal logic can describe all attacks whenever a privacy property expressed as an equivalence problem fails.

Original language | English |
---|---|

Article number | 113842 |

Number of pages | 42 |

Journal | Theoretical Computer Science |

Volume | 959 |

Early online date | 17 Apr 2023 |

DOIs | |

Publication status | Published - 30 May 2023 |

## Keywords

- bisimilarity
- compositionality
- cryptographic calculi
- intuitionistic modal logic
- privacy
- security