Symbolic protocol composition logic : proving network protocols to be secure
Abstract/Contents
- Abstract
- While computational methods for the verification of network protocols view cryptographic operations as the manipulation of bitstrings, symbolic approaches view the application of cryptography as manipulation of symbols according to a term grammar, equations, and term manipulation rules. Computational cryptography is very hard given the immense complexity of network protocols. Symbolic cryptography takes security of cryptographic primitives as a given and thereby enables a researcher to focus on protocol-level notions of security, such as authentication of protocol participants and secrecy of nonces and keys. Protocol Composition Logic (PCL) can be characterized in the following ways: it is a direct logic; it is a logic producing before-after assertions; symbolic and computational versions of PCL are maintained and proven sound independently; it is compatible with different logics for reasoning between the preconditions and postconditions. My work extends symbolic PCL. On the theory-building side, I first invent an expressive imperative protocol description language with execution rules and then on top provide a logic for stating security properties of protocols described in my protocol description language. The protocol description language comes with a message algebra with a syntax, a detailed type system, equations, 2 different normal forms, and 3 different types of term containment. My logic consists of a language for formulating assertions about protocols and a semantics for that language. Among other things, I have refined PCL's notion of honesty, clarified the dependence of assertions on setup assumptions, and made explicit the dependence of secrecy proofs on role parameters. I provide an updated proof system (axioms and rules) for my updated logic. On the problem solving side, I extend the existing treatment of secrecy, culminating in a proof of secrecy for the IEEE 802.11-2012 4-Way Handshake. My approach lets us prove secrecy also for keys and tags (macs, signatures, and hashes), not only nonces. Previous treatment relied on honest protocol participants not revealing the protecting keys, and this assumption has now been made explicit. Proving secrecy no longer relies on induction over the artificial notion of a 'basic sequence'. On the development side, my thesis provides novel, clear notation (usable in all of symbolic cryptography) and a rigorous exposition (suitable for direct proof automation).
Description
| Type of resource | text |
|---|---|
| Form | electronic; electronic resource; remote |
| Extent | 1 online resource. |
| Publication date | 2014 |
| Issuance | monographic |
| Language | English |
Creators/Contributors
| Associated with | Stiller, Stephan Hyeonjun |
|---|---|
| Associated with | Stanford University, Department of Computer Science. |
| Primary advisor | Mitchell, John |
| Thesis advisor | Mitchell, John |
| Thesis advisor | Dill, David L |
| Thesis advisor | Pratt, Vaughan R |
| Advisor | Dill, David L |
| Advisor | Pratt, Vaughan R |
Subjects
| Genre | Theses |
|---|
Bibliographic information
| Statement of responsibility | Stephan Hyeonjun Stiller. |
|---|---|
| Note | Submitted to the Department of Computer Science. |
| Thesis | Thesis (Ph.D.)--Stanford University, 2014. |
| Location | electronic resource |
Access conditions
- Copyright
- © 2014 by Stephan Hyeonjun Stiller
- License
- This work is licensed under a Creative Commons Attribution Non Commercial Share Alike 3.0 Unported license (CC BY-NC-SA).
Also listed in
Loading usage metrics...