scientific article; zbMATH DE number 1341618
From MaRDI portal
Publication:4263167
zbMATH Open1038.94548MaRDI QIDQ4263167FDOQ4263167
Authors: Christoph Weidenbach 
Publication date: 17 February 2000
Title of this publication is not available (Why is that?)
Cited In (28)
- Paths, tree homomorphisms and disequalities for -clauses
- Superposition for Fixed Domains
- SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment
- From Search to Computation: Redundancy Criteria and Simplification at Work
- Key Substitution in the Symbolic Analysis of Cryptographic Protocols
- Deciding \(\mathcal H_1\) by resolution
- On the symbolic reduction of processes with cryptographic functions.
- A domain-specific language for cryptographic protocols based on streams
- Secrecy types for asymmetric communication.
- On the relationships between models in protocol verification
- Extending \(H_1\)-clauses with disequalities
- First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation
- A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties
- Automating security analysis: symbolic equivalence of constraint systems
- Challenges in the Automated Verification of Security Protocols
- System description: SPASS-FD
- State space reduction in the Maude-NRL protocol analyzer
- Normalization of linear Horn clauses
- Deciding the Inductive Validity of ∀ ∃ * Queries
- Security protocols: from linear to classical logic by abstract interpretation
- Finite reasons for safety
- Harald Ganzinger’s Legacy: Contributions to Logics and Programming
- Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif
- Verifying Cryptographic Protocols with Subterms Constraints
- Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables
- Automated Verification of Equivalence Properties of Cryptographic Protocols
- Verification of cryptographic protocols: tagging enforces termination
- Crossing the syntactic barrier: hom-disequalities for \({\mathcal H}_1\)-clauses
Uses Software
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4263167)
