Cryptographic protocols are in general difficult to analyze, and complicated attacks exposing security flaws have remained hidden years after a protocol is developed. Recently developed tools such as strand spaces and inductive logical proofs provide mechanical procedures for analyzing protocols. The key to these methods is that a generous upper bound on the activity of a malicious penetrator is often much easier to work with than a tighter bound. However, these formalizations make strong assumptions about the algebraic structure of the cryptosystem that are never met in a real application. In this work, we show that an extended form of the strand space machinery can be used to analyze protocols which contain nontrivial algebraic structure, specifically that which arises from the XOR operation. This work also serves as one of the first steps in reconciling computational and formal methods of analyzing cryptographic security.
| Identifer | oai:union.ndltd.org:CLAREMONT/oai:scholarship.claremont.edu:hmc_theses-1133 |
| Date | 01 May 2001 |
| Creators | Mahlburg, Karl |
| Publisher | Scholarship @ Claremont |
| Source Sets | Claremont Colleges |
| Detected Language | English |
| Type | text |
| Format | application/pdf |
| Source | HMC Senior Theses |
Page generated in 0.0017 seconds