Student Work
Protocol Analysis via The Chase
PubblicoContenuto scaricabile
open in viewerWe expound a method of analyzing cryptographic protocols using geometric logic and the Chase. Geometric logic is a formal system of logic comparable to first order logic, and the Chase is an algorithm which finds models for a given geometric logic theory. We use the Strand Space formalism as a model of protocol execution. Our work includes a rigorous translation of the Strand Space formalism, developed at MITRE, into geometric logic, a compiler that translates cryptographic protocols into geometric logic theories, and an algorithm for checking isomorphism between protocol executions in a special case in linear time.
- This report represents the work of one or more WPI undergraduate students submitted to the faculty as evidence of completion of a degree requirement. WPI routinely publishes these reports on its website without editorial or peer review.
- Creator
- Publisher
- Identifier
- E-project-042911-040748
- Advisor
- Year
- 2011
- Date created
- 2011-04-29
- Resource type
- Major
- Rights statement
Relazioni
- In Collection:
Articoli
Elementi
Thumbnail | Titolo | Visibilità | Embargo Release Date | Azioni |
---|---|---|---|---|
paper.pdf | Pubblico | Scaricare | ||
ns.scm | Pubblico | Scaricare | ||
strandSpace.txt | Pubblico | Scaricare | ||
cremers.txt | Pubblico | Scaricare | ||
ns.thy | Pubblico | Scaricare | ||
compiler.hs | Pubblico | Scaricare |
Permanent link to this page: https://digital.wpi.edu/show/n296x0804