Formal Methods and the Public Key Directory

This repository contains ProVerif models of the Public Key Directory specification and uses Duvet to ensure the specification requiremments are satisfied by the known implementations.

To understand the motivation for this repository, please refer to: Software Assurance & That Warm and Fuzzy Feeling.

Running Proofs

Prerequisites

Install ProVerif to verify the proofs.

Install Duvet to trace the requirements from the implementations to the proofs.

Run the Proofs

cd proofs
for f in *.pv; do
    echo "Verifying $f..."
    proverif "$f" || exit 1
done

Duvet Requirements Traceability

All proofs include duvet annotations linking to specification requirements. Run duvet report from the repository root to generate a traceability report.

duvet report