scientific article; zbMATH DE number 2043527
From MaRDI portal
zbMath1038.03012MaRDI QIDQ4447230
Véronique Cortier, Hubert Comon-Lundh
Publication date: 16 February 2004
Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2706/27060148.htm
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
first-order logicdecidabilityresolutionexclusive orextension of Skolem classverification of cryptographic protocol
Cryptography (94A60) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Subsystems of classical logic (including intuitionistic logic) (03B20)
Related Items
From Security Protocols to Pushdown Automata, Challenges in the Automated Verification of Security Protocols, Bounding messages for free in security protocols -- extension to various security properties, Towards a unified model of search in theorem-proving: subgoal-reduction strategies, A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols, Canonical Ground Horn Theories, Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically, Reducing protocol analysis with XOR to the XOR-free case in the Horn theory based approach, Verification of cryptographic protocols: tagging enforces termination, A method for symbolic analysis of security protocols, A decidable class of security protocols for both reachability and equivalence properties, Flat and One-Variable Clauses for Single Blind Copying Protocols: The XOR Case, Safely composing security protocols, A symbolic decision procedure for cryptographic protocols with time stamps, Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif
Uses Software
