Automated unbounded verification of security protocols

DOI10.1007/3-540-45657-0_24MaRDI QIDQ4804905zbMATH OpenFDO

Authors Yannick Chevalier, Laurent Vigneron

Publication date 1 May 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2404/24040324.htm

Mathematics Subject Classification ID

Data encryption (aspects in computer science) (68P25) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Verifying security protocols modelled by networks of automata
• Automatic verification of security protocols in the symbolic model: the verifier ProVerif
• Models and Proofs of Protocol Security: A Progress Report
• SAT-Based Verification of Security Protocols Via Translation to Networks of Automata
• Model Checking Software

Cited in

(26)

• An attack-finding algorithm for security protocols.
• Secure mechanical verification of mutually recursive procedures
• Automated proof of Bell-LaPadula security properties
• Combining proverif and automated theorem provers for security protocol verification
• On the relationships between models in protocol verification
• Automatic verification of secrecy properties for linear logic specifications of cryptographic protocols
• Verification of security protocols with lists: from length one to unbounded length
• From model-checking to automated testing of security protocols: bridging the gap
• scientific article; zbMATH DE number 2086169 (Why is no real title available?)
• The Open-Source Fixed-Point Model Checker for Symbolic Analysis of Security Protocols
• Automated Verification of Dynamic Root of Trust Protocols
• Proving Group Protocols Secure Against Eavesdroppers
• Challenges in the Automated Verification of Security Protocols
• Models and Proofs of Protocol Security: A Progress Report
• Bounding messages for free in security protocols -- extension to various security properties
• Equal to the task?
• Automatic verification of security protocols in the symbolic model: the verifier ProVerif
• Programming Languages and Systems
• Model Checking Software
• Trustworthy Global Computing
• Verifying security protocols modelled by networks of automata
• SAT-Based Verification of Security Protocols Via Translation to Networks of Automata
• Bounding Messages for Free in Security Protocols
• Distributed temporal logic for the analysis of security protocol models
• An NP decision procedure for protocol insecurity with XOR
• Simulation relations for alternating Büchi automata

Describes a project that uses

Uses Software

• Casper

This page was built for publication: Automated unbounded verification of security protocols

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