Automated verification of selected equivalences for security protocols
From MaRDI portal
Publication:2474047
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
Cites work
- scientific article; zbMATH DE number 1251177 (Why is no real title available?)
- scientific article; zbMATH DE number 1948406 (Why is no real title available?)
- scientific article; zbMATH DE number 1487486 (Why is no real title available?)
- A calculus for cryptographic protocols: The spi calculus
- Abstracting cryptographic protocols with tree automata.
- Analysing password protocol security against off-line dictionary attacks
- Analyzing security protocols with secrecy types and logic programs
- Automated verification of selected equivalences for security protocols
- CONCUR 2004 - Concurrency Theory
- Deciding knowledge in security protocols under equational theories
- Deciding the word problem in the union of equational theories.
- Foundations of Software Science and Computation Structures
- Information flow inference for ML
- Just fast keying
- Logic for Programming, Artificial Intelligence, and Reasoning
- Mobile values, new names, and secure communication
- On bisimulations for the spi calculus
- Programming Languages and Systems
- Proof techniques for cryptographic processes
- Rewriting
- Secrecy by typing in security protocols
- Security protocols: from linear to classical logic by abstract interpretation
- Static analysis for the \(\pi\)-calculus with applications to security
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
- A process calculus for privacy-preserving protocols in location-based service systems
- Trace equivalence and epistemic logic to express security properties
- Deciding knowledge in security protocols under equational theories
- Tree automata for detecting attacks on protocols with algebraic cryptographic primitives
- DeepSec: deciding equivalence properties for security protocols -- improved theory and practice
- Encoding cryptographic primitives in a calculus with polyadic synchronisation
- From security protocols to pushdown automata
- Compositional analysis of protocol equivalence in the applied \(\pi \)-calculus using quasi-open bisimilarity
- Automatic verification of security protocols in the symbolic model: the verifier ProVerif
- scientific article; zbMATH DE number 7559487 (Why is no real title available?)
- Automatic verification of cryptographic protocols with SETHEO
- Emerging issues and trends in formal methods in cryptographic protocol analysis: twelve years later
- 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
- 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
- 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
- Computing strong and weak bisimulations for psi-calculi
- Analysing privacy-type properties in cryptographic protocols (invited talk)
- One vote is enough for analysing privacy
- scientific article; zbMATH DE number 7806140 (Why is no real title available?)
- Synthesis of opaque systems with static and dynamic masks
- A game-theoretic framework for specification and verification of cryptographic protocols
- Efficiently deciding equivalence for standard primitives and phases
- 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
- Challenges in the Automated Verification of Security Protocols
- Automating security analysis: symbolic equivalence of constraint systems
- 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
- Rewriting Privacy
- A complete symbolic bisimulation for full applied pi calculus
- Causality, behavioural equivalences, and the security of cyberphysical systems
- Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories
- A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols
- Beyond Subterm-Convergent Equational Theories in Automated Verification of Stateful 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
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)
