Towards an automatic analysis of security protocols in first-order logic
From MaRDI portal
Cited in
(30)- A domain-specific language for cryptographic protocols based on streams
- Deciding H₁ by resolution
- Security protocols: from linear to classical logic by abstract interpretation
- Verification of cryptographic protocols: tagging enforces termination
- On the symbolic reduction of processes with cryptographic functions.
- Secrecy types for asymmetric communication.
- Extending H₁-clauses with disequalities
- SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment
- Finite reasons for safety. Parameterized verification by finite model finding
- On the relationships between models in protocol verification
- Crossing the syntactic barrier: hom-disequalities for \({\mathcal H}_1\)-clauses
- First-order logic theorem proving and model building via approximation and instantiation
- Normalization of linear Horn clauses
- Verifying Cryptographic Protocols with Subterms Constraints
- Superposition for Fixed Domains
- Challenges in the Automated Verification of Security Protocols
- Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables
- Deciding the Inductive Validity of ∀ ∃ * Queries
- State space reduction in the Maude-NRL protocol analyzer
- Harald Ganzinger's legacy: contributions to logics and programming
- From search to computation: redundancy criteria and simplification at work
- Paths, tree homomorphisms and disequalities for H₁-clauses
- System description: SPASS-FD
- Automatic verification of security protocols in the symbolic model: the verifier ProVerif
- Automated verification of equivalence properties of cryptographic protocols
- Key Substitution in the Symbolic Analysis of Cryptographic Protocols
- Automating security analysis: symbolic equivalence of constraint systems
- Automatic bit- and memory-precise verification of eBPF code
- First-order automatic literal model generation
- A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties
This page was built for publication: Towards an automatic analysis of security protocols in first-order logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4263167)
