When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied \(\pi\)-calculus
From MaRDI portal
Publication:6041667
DOI10.1016/j.tcs.2023.113842MaRDI QIDQ6041667
Semen Yurkov, Ross Horne, Sjouke Mauw
Publication date: 12 May 2023
Published in: Theoretical Computer Science (Search for Journal in Brave)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Computing strong and weak bisimulations for psi-calculi
- Deducibility constraints and blind signatures
- Intruder deduction problem for locally stable theories with normal forms and inverses
- Modal logics for mobile processes
- A new approach to abstract syntax with variable binding
- Deciding knowledge in security protocols under equational theories
- Associative-commutative unification
- A calculus of mobile processes. I
- Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes.
- A complete symbolic bisimulation for full applied pi calculus
- Sequent calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS
- Private authentication
- A theory of bisimulation for the \(\pi\)-calculus
- A procedure for deciding symbolic equivalence between sets of constraint systems
- Processes against tests: on defining contextual equivalences
- Compositional analysis of protocol equivalence in the applied \(\pi \)-calculus using quasi-open bisimilarity
- A proof theory for model checking
- Open bisimulation, revisited
- Automated verification of selected equivalences for security protocols
- Hennessy-Milner properties via topological compactness
- Proof Techniques for Cryptographic Processes
- A General Theory of Barbs, Contexts, and Labels
- Psi-calculi: a framework for mobile processes with nominal data and logic
- The Applied Pi Calculus
- SPEC: An Equivalence Checker for Security Protocols
- A Trace Based Bisimulation for the Spi Calculus: An Extended Abstract
- Algebraic laws for nondeterminism and concurrency
- A Unification Algorithm for Associative-Commutative Functions
- On the bisimulation proof method
- Three logics for branching bisimulation
- Divergence and unique solution of equations
- Quasi-Open Bisimilarity with Mismatch is Intuitionistic
- A Complete Symbolic Bisimilarity for an Extended Spi Calculus
- Mobile values, new names, and secure communication
- Abella: A System for Reasoning about Relational Specifications
- Barbed bisimulation
- Canonical form for graphs in quasipolynomial time: preliminary report
- A proof theory for generic judgments
- Automated Verification of Equivalence Properties of Cryptographic Protocols
- CONCUR 2004 - Concurrency Theory
- Programming Languages and Systems
- On bisimulations for the spi calculus
- Stochastic Relations: Congruences, Bisimulations and the Hennessy--Milner Theorem
- A Logic for True Concurrency
- Refinement of actions and equivalence notions for concurrent systems
- From rewrite rules to bisimulation congruences
