The Open-Source Fixed-Point Model Checker for Symbolic Analysis of Security Protocols

DOI10.1007/978-3-642-03829-7_6zbMath1252.68193OpenAlexW1598111807MaRDI QIDQ3184787

Sebastian Mödersheim, Luca Viganò

Publication date: 22 October 2009

Published in: Foundations of Security Analysis and Design V (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-03829-7_6

Mathematics Subject Classification ID

Data encryption (aspects in computer science) (68P25) Specification and verification (program logics, model checking, etc.) (68Q60) Network protocols (68M12) Authentication, digital signatures and secret sharing (94A62)

Related Items

Security protocols as choreographies ⋮ \textsf{CaPiTo}: Protocol stacks for services ⋮ Computing knowledge in equational extensions of subterm convergent theories ⋮ Distributed temporal logic for the analysis of security protocol models

Uses Software

• AVISPA
• Casper
• Graphplan
• OFMC
• scyther
• NRL

Cites Work

• Secure protocol composition
• Safely composing security protocols
• Fast planning through planning graph analysis
• Composition of password-based protocols
• On the relationships between models in protocol verification
• A framework for compositional verification of security protocols
• The NRL Protocol Analyzer: An Overview
• The CL-Atse Protocol Analyser
• Cryptographic Protocol Composition via the Authentication Tests
• On the security of public key protocols
• Term Rewriting and All That
• Tree Automata for Detecting Attacks on Protocols with Algebraic Cryptographic Primitives
• LTL model checking for security protocols
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• Algebraic Intruder Deductions
• From One Session to Many: Dynamic Tags for Security Protocols
• Computer Aided Verification
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item