LTL model checking for security protocols

DOI10.3166/JANCL.19.403-429zbMath1186.68276OpenAlexW2022738481MaRDI QIDQ5188173

Alessandro Armando, Luca Compagna, Roberto Carbone

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)

Related Items (7)

The Open-Source Fixed-Point Model Checker for Symbolic Analysis of Security Protocols ⋮ \textsc{NeVer}: a tool for artificial neural networks verification ⋮ Multi-attacker protocol validation ⋮ LTL model checking for security protocols ⋮ A communication algorithm for teamwork in multi-agent environments ⋮ Assume-guarantee synthesis for digital contract signing ⋮ TAGED Approximations for Temporal Properties Model-Checking

Uses Software

• AVISPA

Cites Work

• Finite-state analysis of two contract signing protocols
• The NRL Protocol Analyzer: An Overview
• On the security of public key protocols
• LTL model checking for security protocols
• Unnamed Item

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