Automatic verification of temporal-epistemic properties of cryptographic protocols

DOI10.3166/JANCL.19.463-487zbMath1186.68105OpenAlexW2081927093MaRDI QIDQ5188176

Alessio Lomuscio, Ioana Boureanu, Mika Cohen

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.463-487

zbMATH Keywords

model-checkingepistemic logicsecurity protocols

Mathematics Subject Classification ID

Cryptography (94A60) Theory of compilers and interpreters (68N20) Data encryption (aspects in computer science) (68P25) Specification and verification (program logics, model checking, etc.) (68Q60) Authentication, digital signatures and secret sharing (94A62)

Related Items (5)

To know or not to know: Epistemic approaches to security protocol verification ⋮ Unnamed Item ⋮ Unnamed Item ⋮ An omniscience-free temporal logic of knowledge for verifying authentication protocols ⋮ A communication algorithm for teamwork in multi-agent environments

Uses Software

• LDYIS
• VerICS
• TAPS
• MCMAS-X
• AVISPA
• Casper
• MCMAS

Cites Work

• The dining cryptographers problem: Unconditional sender and recipient untraceability
• The NRL Protocol Analyzer: An Overview
• On the security of public key protocols
• Using encryption for authentication in large networks of computers

This page was built for publication: Automatic verification of temporal-epistemic properties of cryptographic protocols