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)
- Superposition for Fixed Domains
- SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment
- Automatic verification of security protocols in the symbolic model: the verifier ProVerif
- Harald Ganzinger's legacy: contributions to logics and programming
- First-order logic theorem proving and model building via approximation and instantiation
- 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
- Paths, tree homomorphisms and disequalities for \(\mathcal H_1\)-clauses
- Extending \(H_1\)-clauses with disequalities
- 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
- Automated verification of equivalence properties of cryptographic protocols
- Finite reasons for safety. Parameterized verification by finite model finding
- State space reduction in the Maude-NRL protocol analyzer
- Normalization of linear Horn clauses
- Deciding the Inductive Validity of ∀ ∃ * Queries
- From search to computation: redundancy criteria and simplification at work
- Security protocols: from linear to classical logic by abstract interpretation
- Verifying Cryptographic Protocols with Subterms Constraints
- Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables
- 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)
