Automated verification of selected equivalences for security protocols
From MaRDI portal
Publication:2474047
DOI10.1016/J.JLAP.2007.06.002zbMATH Open1135.68007OpenAlexW2055259417MaRDI QIDQ2474047FDOQ2474047
Authors: Bruno Blanchet, Martín Abadi, 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
Recommendations
- Automatic verification of security protocols in the symbolic model: the verifier ProVerif
- Proving more observational equivalences with ProVerif
- Models and Proofs of Protocol Security: A Progress Report
- Security protocol verification: symbolic and computational models
- scientific article; zbMATH DE number 2087423
Specification and verification (program logics, model checking, etc.) (68Q60) Network design and communication in computer systems (68M10) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Network protocols (68M12)
Cites Work
- A calculus for cryptographic protocols: The spi calculus
- Mobile values, new names, and secure communication
- Rewriting
- Information flow inference for ML
- Automated verification of selected equivalences for security protocols
- Proof techniques for cryptographic processes
- Deciding knowledge in security protocols under equational theories
- Deciding the word problem in the union of equational theories.
- Analysing password protocol security against off-line dictionary attacks
- On bisimulations for the spi calculus
- Analyzing security protocols with secrecy types and logic programs
- CONCUR 2004 - Concurrency Theory
- Static analysis for the \(\pi\)-calculus with applications to security
- Secrecy by typing in security protocols
- Title not available (Why is that?)
- Foundations of Software Science and Computation Structures
- Title not available (Why is that?)
- Programming Languages and Systems
- Title not available (Why is that?)
- Logic for Programming, Artificial Intelligence, and Reasoning
- Security protocols: from linear to classical logic by abstract interpretation
- Abstracting cryptographic protocols with tree automata.
- Just fast keying
Cited In (53)
- Deciding equivalence-based properties using constraint solving
- Decidability of equivalence of symbolic derivations
- CoCon: a conference management system with formally verified document confidentiality
- Trace equivalence and epistemic logic to express security properties
- A process calculus for privacy-preserving protocols in location-based service systems
- Tree automata for detecting attacks on protocols with algebraic cryptographic primitives
- Deciding knowledge in security protocols under equational theories
- Encoding cryptographic primitives in a calculus with polyadic synchronisation
- From security protocols to pushdown automata
- Automatic verification of security protocols in the symbolic model: the verifier ProVerif
- Compositional analysis of protocol equivalence in the applied \(\pi \)-calculus using quasi-open bisimilarity
- Title not available (Why is that?)
- Automatic verification of cryptographic protocols with SETHEO
- Emerging issues and trends in formal methods in cryptographic protocol analysis: twelve years later
- When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied \(\pi\)-calculus
- YAPA: A Generic Tool for Computing Intruder Knowledge
- A spatial equational logic for the applied \(\pi \)-calculus
- Computing knowledge in security protocols under convergent equational theories
- Reducing equational theories for the decision of static equivalence
- Proving more observational equivalences with ProVerif
- Implementing Spi Calculus Using Nominal Techniques
- Automated Verification of Dynamic Root of Trust Protocols
- On Communication Models When Verifying Equivalence Properties
- Analysing privacy-type properties in cryptographic protocols (invited talk)
- One vote is enough for analysing privacy
- Computing strong and weak bisimulations for psi-calculi
- Synthesis of opaque systems with static and dynamic masks
- Efficiently deciding equivalence for standard primitives and phases
- A game-theoretic framework for specification and verification of cryptographic protocols
- Automated verification of selected equivalences for security protocols
- Probability timed automata for investigating communication processes
- A procedure for deciding symbolic equivalence between sets of constraint systems
- CoSMed: a confidentiality-verified social media platform
- Automating security analysis: symbolic equivalence of constraint systems
- Challenges in the Automated Verification of Security Protocols
- Modular verification of protocol equivalence in the presence of randomness
- Security Protocol Analysis in Context: Computing Minimal Executions Using SMT and CPSA
- Programming Languages and Systems
- Model Checking Security Protocols
- Cross-tool semantics for protocol security goals
- Causality, behavioural equivalences, and the security of cyberphysical systems
- A complete symbolic bisimulation for full applied pi calculus
- Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories
- Beyond Subterm-Convergent Equational Theories in Automated Verification of Stateful Protocols
- A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols
- Reducing protocol analysis with XOR to the XOR-free case in the Horn theory based approach
- Formalizing provable anonymity in Isabelle/HOL
- Automated verification of equivalence properties of cryptographic protocols
- Formal analysis of a TTP-free blacklistable anonymous credentials system
- SPEC: an equivalence checker for security protocols
- DeepSec: deciding equivalence properties for security protocols -- improved theory and practice
- Title not available (Why is that?)
- Rewriting Privacy
Uses Software
This page was built for publication: Automated verification of selected equivalences for security protocols
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2474047)
