When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied -calculus

DOI10.1016/J.TCS.2023.113842MaRDI QIDQ6041667FDOQ6041667

Authors: Ross Horne, Sjouke Mauw, Semen Yurkov 

Publication date: 12 May 2023

Published in: Theoretical Computer Science (Search for Journal in Brave)

Recommendations

• Symbolic Bisimulation for the Applied Pi Calculus
• A pure labeled transition semantics for the applied pi calculus
• Bisimulations respecting duration and causality for the non-interleaving applied \(\pi\)-calculus
• Stateful applied pi calculus: observational equivalence and labelled bisimilarity
• Proof system for applied pi calculus

zbMATH Keywords

securitycompositionalityprivacyintuitionistic modal logicbisimilaritycryptographic calculi

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Cites Work

• Abella: a system for reasoning about relational specifications
• SPEC: an equivalence checker for security protocols
• The linear time -- branching time spectrum. I: The semantics of concrete, sequential processes.
• Algebraic laws for nondeterminism and concurrency
• Title not available (Why is that?)
• Stochastic Relations: Congruences, Bisimulations and the Hennessy--Milner Theorem
• Title not available (Why is that?)
• Modal logics for mobile processes
• A new approach to abstract syntax with variable binding
• A calculus of mobile processes. I
• Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes.
• Psi-calculi: a framework for mobile processes with nominal data and logic
• Mobile values, new names, and secure communication
• Refinement of actions and equivalence notions for concurrent systems
• A Unification Algorithm for Associative-Commutative Functions
• Automated verification of equivalence properties of cryptographic protocols
• Title not available (Why is that?)
• On the bisimulation proof method
• The \(\pi\)-calculus: A theory of mobile processes
• Title not available (Why is that?)
• Barbed bisimulation
• A logic for true concurrency
• Three logics for branching bisimulation
• Title not available (Why is that?)
• Private authentication
• Automated verification of selected equivalences for security protocols
• Proof techniques for cryptographic processes
• Deciding knowledge in security protocols under equational theories
• Programming Languages and Systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• A theory of bisimulation for the \(\pi\)-calculus
• Computing strong and weak bisimulations for psi-calculi
• CONCUR 2004 - Concurrency Theory
• Deducibility constraints and blind signatures
• Title not available (Why is that?)
• A Trace Based Bisimulation for the Spi Calculus: An Extended Abstract
• Title not available (Why is that?)
• A complete symbolic bisimilarity for an extended spi calculus
• Sequent calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS
• On bisimulations for the spi calculus
• Title not available (Why is that?)
• Associative-commutative unification
• Title not available (Why is that?)
• A proof theory for generic judgments
• Intruder deduction problem for locally stable theories with normal forms and inverses
• From rewrite rules to bisimulation congruences
• A complete symbolic bisimulation for full applied pi calculus
• A procedure for deciding symbolic equivalence between sets of constraint systems
• Processes against tests: on defining contextual equivalences
• A proof theory for model checking
• Analysing privacy-type properties in cryptographic protocols (invited talk)
• Modal logics for nominal transition systems
• The Applied Pi Calculus
• Title not available (Why is that?)
• A General Theory of Barbs, Contexts, and Labels
• Quasi-open bisimilarity with mismatch is intuitionistic
• Compositional analysis of protocol equivalence in the applied \(\pi \)-calculus using quasi-open bisimilarity
• Open bisimulation, revisited
• Title not available (Why is that?)
• A characterisation of open bisimilarity using an intuitionistic modal logic
• Title not available (Why is that?)
• Hennessy-Milner properties via topological compactness
• Title not available (Why is that?)
• Canonical form for graphs in quasipolynomial time: preliminary report

This page was built for publication: When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied \(\pi\)-calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6041667)