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
• scientific article; zbMATH DE number 1962854
• Logic for verifying public-key cryptographic protocols
• Abstract interpretation for proving secrecy properties in security protocols
• scientific article; zbMATH DE number 1024091
• 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
• Encoding transition systems in sequent calculus
• Forum: A multiple-conclusion specification logic
• scientific article; zbMATH DE number 1614701 (Why is no real title available?)
• scientific article; zbMATH DE number 1670808 (Why is no real title available?)
• scientific article; zbMATH DE number 1692895 (Why is no real title available?)
• scientific article; zbMATH DE number 1696763 (Why is no real title available?)
• scientific article; zbMATH DE number 4209572 (Why is no real title available?)
• scientific article; zbMATH DE number 1754628 (Why is no real title available?)
• scientific article; zbMATH DE number 1759624 (Why is no real title available?)
• scientific article; zbMATH DE number 1903362 (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 security of public key protocols
• Protocol insecurity with a finite number of sessions and composed keys is NP-complete.
• Rewriting semantics of meta-objects and composable distributed services
• 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
• scientific article; zbMATH DE number 1962760 (Why is no real title available?)
• 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)