Stateful applied pi calculus: observational equivalence and labelled bisimilarity

DOI10.1016/J.JLAMP.2017.03.001MaRDI QIDQ2397042zbMATH OpenOpenAlexFDO

Authors Myrto Arapinis, Jia Liu, Eike Ritter, M. D. Ryan

Publication date 29 May 2017

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://research.birmingham.ac.uk/portal/en/publications/stateful-applied-pi-calculus-observational-equivalence-and-labelled-bisimilarity(15668517-8fc0-4fde-8bc2-527a787f4b9c).html

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Symbolic Bisimulation for the Applied Pi Calculus
• A theory of bisimulation for the -calculus
• A pure labeled transition semantics for the applied pi calculus
• Behavioural equivalences of a probabilistic pi-calculus
• scientific article; zbMATH DE number 1223732
• A complete symbolic bisimulation for full applied pi-calculus
• Compositional analysis of protocol equivalence in the applied \(\pi \)-calculus using quasi-open bisimilarity
• Computing bisimulations for finite-control \(\pi\)-calculus

Cites work

• A complete symbolic bisimulation for full applied pi calculus
• A relational modal logic for higher-order stateful ADTs
• Automated verification of equivalence properties of cryptographic protocols
• Automating security analysis: symbolic equivalence of constraint systems
• Deciding equivalence-based properties using constraint solving
• Deciding knowledge in security protocols under equational theories
• Mobile values, new names, and secure communication
• Private authentication
• Psi-calculi: a framework for mobile processes with nominal data and logic
• Relating two standard notions of secrecy
• State and progress in strand spaces: proving fair exchange
• The \(\pi\)-calculus: A theory of mobile processes
• Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency
• YAPA: a generic tool for computing intruder knowledge

Cited in

(3)

• States in process calculi
• When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied \(\pi\)-calculus
• A pure labeled transition semantics for the applied pi calculus

Describes a project that uses

Uses Software

• Akiss
• YAPA

This page was built for publication: Stateful applied pi calculus: observational equivalence and labelled bisimilarity

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