Student Work

A Formalization of Strand Spaces in Coq

Pubblico

Contenuto scaricabile

open in viewer

In this paper we formally prove the correctness of two theorems about cryptographic protocol analysis using the Coq proof assistant. The theorems are known as the Authentication Tests in the strand space formalism. With such tests, we can determine whether certain values remain secret so we can check whether certain security properties are achieved by a protocol. Coq is a formal proof management system. It provides a formal language to express mathematical assertions, mechanically checks proofs of these assertions. Coq works within the theory of the calculus of inductive constructions. We first formalize strand spaces by giving definitions in Coq of the basic notions. Then we express the two authentication tests and give constructive proofs for them.

  • 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-043015-101530
Advisor
Year
  • 2015
Date created
  • 2015-04-30
Resource type
Major
Rights statement

Relazioni

In Collection:

Articoli

Elementi

Permanent link to this page: https://digital.wpi.edu/show/9z9031571