Model Checking Security Protocols
From MaRDI portal
Publication:3176380
DOI10.1007/978-3-319-10575-8_22zbMATH Open1392.68228OpenAlexW2803681306MaRDI QIDQ3176380FDOQ3176380
C. J. F. Cremers, David Basin, Catherine 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
Recommendations
Cryptography (94A60) Specification and verification (program logics, model checking, etc.) (68Q60) Network protocols (68M12)
Cites Work
- YAPA: A Generic Tool for Computing Intruder Knowledge
- Computer Aided Verification
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- The NRL Protocol Analyzer: An Overview
- Title not available (Why is that?)
- Mobile values, new names, and secure communication
- Term Rewriting and All That
- Unification in the union of disjoint equational theories: Combining decision procedures
- Using encryption for authentication in large networks of computers
- On the security of ping-pong protocols
- Title not available (Why is that?)
- Title not available (Why is that?)
- Automated verification of selected equivalences for security protocols
- Title not available (Why is that?)
- Deciding knowledge in security protocols under equational theories
- On the security of public key protocols
- Computationally sound implementations of equational theories against passive adversaries
- Protocol insecurity with a finite number of sessions and composed keys is NP-complete.
- Analysing password protocol security against off-line dictionary attacks
- Automated complexity analysis based on ordered resolution
- Computing Knowledge in Security Protocols under Convergent Equational Theories
- Verification: Theory and Practice
- Foundations of Software Science and Computation Structures
- Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
- Variant Narrowing and Equational Unification
- Programming Languages and Systems
- Degrees of Security: Protocol Guarantees in the Face of Compromising Adversaries
- Title not available (Why is that?)
- The CL-Atse Protocol Analyser
- Title not available (Why is that?)
- Algebraic Intruder Deductions
- A survey of symbolic methods in computational analysis of cryptographic systems
- Term Rewriting and Applications
- The reactive simulatability (RSIM) framework for asynchronous systems
- A framework for compositional verification of security protocols
- Automatic analysis of a non-repudiation protocol
- Propositional SAT Solving
- Model Checking Probabilistic Systems
- Unification in permutative equational theories is undecidable
- Provably Repairing the ISO/IEC 9798 Standard for Entity Authentication
- A formal language for cryptographic protocol requirements
- On the freedom of decryption
- Partial-Order Reduction
- Let’s Get Physical: Models and Methods for Real-World Security Protocols
- Limits of the Cryptographic Realization of Dolev-Yao-Style XOR
- Limits of the BRSIM/UC Soundness of Dolev-Yao Models with Hashes
Cited In (10)
- Analyzing Internet Routing Security Using Model Checking
- Verification and modelling of authentication protocols
- Title not available (Why is that?)
- Automated proof of Bell-LaPadula security properties
- Formal Modeling and Verification of High-Availability Protocol for Network Security Appliances
- Formal verification of security model using SPR tool
- Communicating Sequential Processes. The First 25 Years
- Modular verification of security protocol code by typing
- Formalization and analysis of the post-quantum signature scheme FALCON with Maude
- Title not available (Why is that?)
Uses Software
This page was built for publication: Model Checking Security Protocols
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3176380)
