Automatic verification of secrecy properties for linear logic specifications of cryptographic protocols

DOI10.1016/J.JSC.2004.04.002MaRDI QIDQ2643568zbMATH OpenOpenAlexFDO

Authors Marco Bozzano, Giorgio Delzanno

Publication date 24 August 2007

Published in Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jsc.2004.04.002

zbMATH Keywords

authentication protocolsbottom-up evaluationlinear logicmodel checking

Mathematics Subject Classification ID

Network protocols (68M12) Specification and verification (program logics, model checking, etc.) (68Q60) Cryptography (94A60)

Recommendations

• Automated verification of equivalence properties of cryptographic protocols
• Automated verification of equivalence properties of cryptographic protocols
• scientific article; zbMATH DE number 2086169
• Automatic verification of cryptographic protocols with SETHEO
• Cryptographically sound and machine-assisted verification of security protocols
• Logic for verifying public-key cryptographic protocols
• Abstract interpretation for proving secrecy properties in security protocols
• Formal verification of cryptographic protocols: A survey
• Automatic verification of security protocols in the symbolic model: the verifier ProVerif

Cites work

• A logic of authentication
• Algorithmic analysis of programs with well quasi-ordered domains.
• An attack on the Needham-Schroeder public-key authentication protocol
• An effective fixpoint semantics for linear logic programs
• Asynchronous communication model based on linear logic
• Automated unbounded verification of security protocols
• Compiling and verifying security protocols
• Encoding transition systems in sequent calculus
• Forum: A multiple-conclusion specification logic
• scientific article; zbMATH DE number 4209572 (Why is no real title available?)
• Linear concurrent constraint programming: Operational and phase semantics
• Linear logic
• Logic Programming with Focusing Proofs in Linear Logic
• On the reachability problem in cryptographic protocols
• On the security of public key protocols
• Protocol insecurity with a finite number of sessions and composed keys is NP-complete.
• Rewriting for cryptographic protocol verification
• Rewriting semantics of meta-objects and composable distributed services
• Specifying and debugging security protocols via hereditary Harrop formulas and Prolog -- a case-study
• Symbolic trace analysis of cryptographic protocols
• TAPS: A first-order verifier for cryptographic protocols
• The NRL Protocol Analyzer: An Overview
• Theory and Applications of Satisfiability Testing
• Typed multiset rewriting specifications of security protocols
• Uniform proofs as a foundation for logic programming
• Using encryption for authentication in large networks of computers

Cited in

(5)

• LACPV'2001. Logical aspects of cryptographic protocol verification. Proceedings of the 1st workshop (a satellite workshop of CAV'01), Paris, France, July 23, 2001.
• Finite Models in FOL-Based Crypto-Protocol Verification
• A logical verification method for security protocols based on linear logic and BAN logic
• Encryption as an abstract data-type (extended abstract)
• Cryptographic protocol logic: satisfaction for (timed) Dolev-Yao cryptography

Describes a project that uses

Uses Software

• TAPS
• Casper
• NRL

This page was built for publication: Automatic verification of secrecy properties for linear logic specifications of cryptographic protocols

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2643568)