Model Checking Security Protocols
From MaRDI portal
Publication:3176380
DOI10.1007/978-3-319-10575-8_22zbMath1392.68228OpenAlexW2803681306MaRDI QIDQ3176380
C. J. F. Cremers, David A. Basin, Catherine A. Meadows
Publication date: 20 July 2018
Published in: Handbook of Model Checking (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-10575-8_22
Cryptography (94A60) Specification and verification (program logics, model checking, etc.) (68Q60) Network protocols (68M12)
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A survey of symbolic methods in computational analysis of cryptographic systems
- Deciding knowledge in security protocols under equational theories
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- On the freedom of decryption
- Computationally sound implementations of equational theories against passive adversaries
- Unification in permutative equational theories is undecidable
- Protocol insecurity with a finite number of sessions and composed keys is NP-complete.
- A formal language for cryptographic protocol requirements
- Unification in the union of disjoint equational theories: Combining decision procedures
- The reactive simulatability (RSIM) framework for asynchronous systems
- Automated verification of selected equivalences for security protocols
- A framework for compositional verification of security protocols
- Provably Repairing the ISO/IEC 9798 Standard for Entity Authentication
- Automated complexity analysis based on ordered resolution
- The NRL Protocol Analyzer: An Overview
- Partial-Order Reduction
- Propositional SAT Solving
- Model Checking Probabilistic Systems
- Let’s Get Physical: Models and Methods for Real-World Security Protocols
- Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
- On the security of ping-pong protocols
- The CL-Atse Protocol Analyser
- Degrees of Security: Protocol Guarantees in the Face of Compromising Adversaries
- YAPA: A Generic Tool for Computing Intruder Knowledge
- On the security of public key protocols
- Using encryption for authentication in large networks of computers
- Term Rewriting and All That
- Mobile values, new names, and secure communication
- Variant Narrowing and Equational Unification
- Computing Knowledge in Security Protocols under Convergent Equational Theories
- Verification: Theory and Practice
- Programming Languages and Systems
- Algebraic Intruder Deductions
- Term Rewriting and Applications
- Computer Aided Verification
- Limits of the BRSIM/UC Soundness of Dolev-Yao Models with Hashes
- Limits of the Cryptographic Realization of Dolev-Yao-Style XOR
- Foundations of Software Science and Computation Structures
This page was built for publication: Model Checking Security Protocols
