Automated verification of selected equivalences for security protocols

DOI10.1016/j.jlap.2007.06.002zbMath1135.68007OpenAlexW2055259417MaRDI QIDQ2474047

Martín Abadi, Bruno Blanchet, Cédric Fournet

Publication date: 5 March 2008

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlap.2007.06.002

zbMATH Keywords

pi calculus ProVerif

Mathematics Subject Classification ID

Network design and communication in computer systems (68M10) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Network protocols (68M12)

Related Items

Compositional analysis of protocol equivalence in the applied \(\pi \)-calculus using quasi-open bisimilarity, From Security Protocols to Pushdown Automata, Causality, Behavioural Equivalences, and the Security of Cyberphysical Systems, Model Checking Security Protocols, SPEC: An Equivalence Checker for Security Protocols, Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories, Deciding knowledge in security protocols under equational theories, CoSMed: a confidentiality-verified social media platform, Modular verification of protocol equivalence in the presence of randomness, Efficiently deciding equivalence for standard primitives and phases, A game-theoretic framework for specification and verification of cryptographic protocols, A process calculus for privacy-preserving protocols in location-based service systems, Emerging Issues and Trends in Formal Methods in Cryptographic Protocol Analysis: Twelve Years Later, Deciding equivalence-based properties using constraint solving, When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied \(\pi\)-calculus, Unnamed Item, Security Protocol Analysis in Context: Computing Minimal Executions Using SMT and CPSA, Implementing Spi Calculus Using Nominal Techniques, One vote is enough for analysing privacy, Reducing equational theories for the decision of static equivalence, Decidability of equivalence of symbolic derivations, Computing knowledge in security protocols under convergent equational theories, Computing strong and weak bisimulations for psi-calculi, Synthesis of opaque systems with static and dynamic masks, Unnamed Item, Challenges in the Automated Verification of Security Protocols, Formal Analysis of a TTP-Free Blacklistable Anonymous Credentials System, Beyond Subterm-Convergent Equational Theories in Automated Verification of Stateful Protocols, On Communication Models When Verifying Equivalence Properties, A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols, Automated verification of selected equivalences for security protocols, A complete symbolic bisimulation for full applied pi calculus, Reducing protocol analysis with XOR to the XOR-free case in the Horn theory based approach, Encoding cryptographic primitives in a calculus with polyadic synchronisation, Tree Automata for Detecting Attacks on Protocols with Algebraic Cryptographic Primitives, A procedure for deciding symbolic equivalence between sets of constraint systems, Automating Security Analysis: Symbolic Equivalence of Constraint Systems, Unnamed Item, A spatial equational logic for the applied \(\pi \)-calculus, CoCon: a conference management system with formally verified document confidentiality, Probability timed automata for investigating communication processes, YAPA: A Generic Tool for Computing Intruder Knowledge, Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif, Formalizing provable anonymity in Isabelle/HOL

Uses Software

ProVerif

Cites Work