Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif
DOI10.1007/978-3-319-10082-1_3zbMath1448.68185OpenAlexW134285089MaRDI QIDQ5253587
Publication date: 27 May 2015
Published in: Foundations of Security Analysis and Design VII (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-10082-1_3
Cryptography (94A60) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Authentication, digital signatures and secret sharing (94A62) Computer security (68M25)
Related Items (2)
Uses Software
Cites Work
- Reducing protocol analysis with XOR to the XOR-free case in the Horn theory based approach
- An NP decision procedure for protocol insecurity with XOR
- A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties
- Deciding \(\mathcal H_1\) by resolution
- Security protocols: from linear to classical logic by abstract interpretation
- Oriented equational logic programming is complete
- Abstracting cryptographic protocols with tree automata.
- Verification of cryptographic protocols: tagging enforces termination
- Secrecy types for asymmetric communication.
- Protocol insecurity with a finite number of sessions and composed keys is NP-complete.
- Security properties: two agents are sufficient
- Automated verification of selected equivalences for security protocols
- Computer-assisted verification of a protocol for certified email
- Security Protocol Verification: Symbolic and Computational Models
- The NRL Protocol Analyzer: An Overview
- Analyzing security protocols with secrecy types and logic programs
- Just fast keying
- New directions in cryptography
- On the security of public key protocols
- Using encryption for authentication in large networks of computers
- Mobile values, new names, and secure communication
- FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
- FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
- Computer-Aided Security Proofs for the Working Cryptographer
- Programming Languages and Systems
- Bounding Messages for Free in Security Protocols
- Verification, Model Checking, and Abstract Interpretation
- Computer Aided Verification
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif
