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

DOI10.1016/j.jsc.2004.04.002zbMath1137.68431OpenAlexW2036707990MaRDI QIDQ2643568

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

linear logicmodel checkingauthentication protocolsbottom-up evaluation

Mathematics Subject Classification ID

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

Related Items

Cryptographic protocol logic: satisfaction for (timed) Dolev-Yao cryptography

Uses Software

• TAPS
• Casper
• NRL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Forum: A multiple-conclusion specification logic
• An attack on the Needham-Schroeder public-key authentication protocol
• Encoding transition systems in sequent calculus
• Algorithmic analysis of programs with well quasi-ordered domains.
• Linear concurrent constraint programming: Operational and phase semantics
• Protocol insecurity with a finite number of sessions and composed keys is NP-complete.
• Asynchronous communication model based on linear logic
• Uniform proofs as a foundation for logic programming
• The NRL Protocol Analyzer: An Overview
• On the security of public key protocols
• Logic Programming with Focusing Proofs in Linear Logic
• Using encryption for authentication in large networks of computers
• A logic of authentication
• An effective fixpoint semantics for linear logic programs
• Typed Multiset Rewriting Specifications of Security Protocols
• Theory and Applications of Satisfiability Testing