We 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

• Pombrio, Justin Lee

Publisher

• Worcester Polytechnic Institute

Identifier

• E-project-042911-040748

Advisor

• Dougherty, Daniel J.
• Christopher, Peter R.
• Guttman, Joshua D.

Year

• 2011

Date created

• 2011-04-29

Resource type

• Major Qualifying Project

Major

• Interdisciplinary

Rights statement

• In Copyright