Automatic verification of secrecy properties for linear logic specifications of cryptographic protocols
DOI10.1016/J.JSC.2004.04.002zbMATH Open1137.68431OpenAlexW2036707990MaRDI QIDQ2643568FDOQ2643568
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
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
Cryptography (94A60) Specification and verification (program logics, model checking, etc.) (68Q60) Network protocols (68M12)
Cites Work
- Title not available (Why is that?)
- The NRL Protocol Analyzer: An Overview
- Linear logic
- Linear concurrent constraint programming: Operational and phase semantics
- Algorithmic analysis of programs with well quasi-ordered domains.
- Using encryption for authentication in large networks of computers
- A logic of authentication
- Logic Programming with Focusing Proofs in Linear Logic
- Uniform proofs as a foundation for logic programming
- On the security of public key protocols
- Protocol insecurity with a finite number of sessions and composed keys is NP-complete.
- Forum: A multiple-conclusion specification logic
- An attack on the Needham-Schroeder public-key authentication protocol
- Title not available (Why is that?)
- Title not available (Why is that?)
- An effective fixpoint semantics for linear logic programs
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Rewriting semantics of meta-objects and composable distributed services
- Encoding transition systems in sequent calculus
- Typed multiset rewriting specifications of security protocols
- Theory and Applications of Satisfiability Testing
- Asynchronous communication model based on linear logic
- Title not available (Why is that?)
Cited In (5)
- Cryptographic protocol logic: satisfaction for (timed) Dolev-Yao cryptography
- Title not available (Why is that?)
- LACPV'2001. Logical aspects of cryptographic protocol verification. Proceedings of the 1st workshop (a satellite workshop of CAV'01), Paris, France, July 23, 2001.
- Encryption as an abstract data-type (extended abstract)
- Finite Models in FOL-Based Crypto-Protocol Verification
Uses Software
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)
