LTL model checking for security protocols

DOI10.3166/JANCL.19.403-429MaRDI QIDQ5188173zbMATH OpenOpenAlexFDO

Authors Alessandro Armando, Roberto Carbone, Luca Compagna

Publication date 10 March 2010

Published in Journal of Applied Non-Classical Logics (Search for Journal in Brave)

Full work available at URL https://doi.org/10.3166/jancl.19.403-429

zbMATH Keywords

bounded model checkingLTLsecurity protocolsSAT-based model checkingabstract communication channelsASWmulti-set rewriting

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 1390339
• LDYIS: a framework for model checking security protocols
• scientific article; zbMATH DE number 1538052
• The ASW protocol revisited: a unified view
• Analysis of security protocols as open systems

Cites work

• Finite-state analysis of two contract signing protocols
• LTL model checking for security protocols
• On the security of public key protocols
• The ASW protocol revisited: a unified view
• The NRL Protocol Analyzer: An Overview

Cited in

(11)

• Multi-attacker protocol validation
• LTL model checking for security protocols
• TAGED Approximations for Temporal Properties Model-Checking
• scientific article; zbMATH DE number 6300104 (Why is no real title available?)
• A communication algorithm for teamwork in multi-agent environments
• Assume-guarantee synthesis for digital contract signing
• \textsc{NeVer}: a tool for artificial neural networks verification
• Model Checking Security Protocols
• The Open-Source Fixed-Point Model Checker for Symbolic Analysis of Security Protocols
• Logic Programming
• Abstraction-based optimal controller synthesis using dynamic quantization and RRT*

Describes a project that uses

Uses Software

• AVISPA

This page was built for publication: LTL model checking for security protocols

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