Back to Search
Start Over
A Tutorial-Style Introduction to $$\textsf {DY}^\star $$
- Source :
- Protocols, Strands, and Logic ISBN: 9783030916305, Protocols, Strands, and Logic, Daniel Dougherty; José Meseguer; Sebastian Alexander Mödersheim; Paul Rowe. Protocols, Strands, and Logic, 13066, Springer International Publishing, pp.77-97, 2021, Lecture Notes in Computer Science, ⟨10.1007/978-3-030-91631-2_4⟩
- Publication Year :
- 2021
- Publisher :
- Springer International Publishing, 2021.
-
Abstract
- \(\textsf {DY}^\star \) is a recently proposed formal verification framework for the symbolic security analysis of cryptographic protocol code written in the \(\textsf {F}^\star \) programming language. Unlike automated symbolic provers, \(\textsf {DY}^\star \) accounts for advanced protocol features like unbounded loops and mutable recursive data structures as well as low-level implementation details like protocol state machines and message formats, which are often at the root of real-world attacks. Protocols modeled in \(\textsf {DY}^\star \) can be executed, and hence, tested, and they can even interoperate with real-world counterparts. \(\textsf {DY}^\star \) extends a long line of research on using dependent type systems but takes a fundamentally new approach by explicitly modeling the global trace-based semantics within the framework, hence bridging the gap between trace-based and type-based protocol analyses. With this, one can uniformly, precisely, and soundly model, for the first time using dependent types, long-lived mutable protocol state, equational theories, fine-grained dynamic corruption, and trace-based security properties like forward secrecy and post-compromise security.
- Subjects :
- Discrete mathematics
[INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR]
Finite-state machine
Trace (linear algebra)
Computer science
Star (game theory)
State (functional analysis)
Cryptographic protocol
Data structure
Formal verification
Dependent type
ComputingMilieux_MISCELLANEOUS
[INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL]
Subjects
Details
- ISBN :
- 978-3-030-91630-5
- ISBNs :
- 9783030916305
- Database :
- OpenAIRE
- Journal :
- Protocols, Strands, and Logic ISBN: 9783030916305, Protocols, Strands, and Logic, Daniel Dougherty; José Meseguer; Sebastian Alexander Mödersheim; Paul Rowe. Protocols, Strands, and Logic, 13066, Springer International Publishing, pp.77-97, 2021, Lecture Notes in Computer Science, ⟨10.1007/978-3-030-91631-2_4⟩
- Accession number :
- edsair.doi.dedup.....c9a3ee19294d8e02a7f29ad4f772cb0e