This is the first post in a series on how to prove that Jasmin programs are correct with respect to a high-level specification written in EasyCrypt. The examples used in this posts are taken from the correctness proof of the XMSS signature scheme, which is available here.

This will be split into four parts:

  • Part 1 (this blog post): provides an overview on how to prove correctness of Jasmin programs with respect to an EasyCrypt specification.

  • Part 2: WOTS+: provides a step-by-step proof of WOTS+, a one-time signature scheme.

Overview

proof diagram

Probabilistic Relational Hoare Logic (pRHL) allows us to relate the execution of two probabilistic programs \(c_1\) and \(c_2\):

$$\models c_1 \sim c_2 \ \colon \ P \implies Q, $$ where \(P\) and \(Q\) are relations over memories.

In correctness proofs, it will usually be the case that \(c_1\) is an implementation and \(c_2\) is a high-level specification, or that \(c_1\) is an optimized implementation while \(c_2\) is a reference implementation.

In addition, we can also reason about different executions of the same program. For example, proving noninterference requires proving that two executions of the same program whose initial values for the secret variables may differ results in two final states where the values of the public variables are equal.