Skip to main content
University of Oxford Department of Computer Science
  Contact Us     Search  
  1. Home
  2. Our Students
  3. Online Resources & Handbooks
  4. Student projects - A Casper Front End for ProVerif

A Casper Front End for ProVerif

Supervisor

Personal photo - Gavin Lowe Gavin Lowe

Suitable for

Abstract

Casper [1] is a tool that builds CSP models of security protocols, suitable for analysis using the model checker FDR. ProVerif is a different tool for security protocol analysis: protocols are described as Horn clauses, and a resolution-based solver is used to verify the protocol. The goal of this project would be to build a Casper-based front end for ProVerif, allowing the user to model protocols using a more user-friendly syntax. Prerequisites for this course would be the Computer Security course, familiarity with process algebra (e.g. via the Concurrency course), and strong functional programming skills (e.g. via the Functional Programming course).

References:

  • [1] Casper: A Compiler for the Analysis of Security Protocols, Gavin Lowe, Journal of Computer Security, 1998.
  • [2] ProVerif, Bruno Blanchet, http://www.proverif.ens.fr/.

Our Students

Back to Top