Paper 2024/1819
VCVio: A Formally Verified Forking Lemma and Fiat-Shamir Transform, via a Flexible and Expressive Oracle Representation
Abstract
As cryptographic protocols continue to become more complex and specialized, their security proofs have grown more complex as well, making manual verification of their correctness more difficult. Formal verification via proof assistants has become a popular approach to solving this, by allowing researchers to write security proofs that can be verified correct by a computer. In this paper we present a new framework of this kind for verifying security proofs, taking a foundational approach to representing and reasoning about protocols. We implement our framework in the Lean programming language, and give a number of security proofs to demonstrate that our system is both powerful and usable, with comparable automation to similar systems. Our framework is especially focused on reasoning about and manipulating oracle access, and we demonstrate the usefulness of this approach by implementing both a general forking lemma and a version of the Fiat-Shamir transform for sigma protocols. As a simple case study we then instantiate these to an implementation of a Schnorr-like signature scheme.
Metadata
- Available format(s)
-
PDF
- Category
- Foundations
- Publication info
- Preprint.
- Contact author(s)
-
tumax040 @ umn edu
hoppernj @ umn edu - History
- 2024-11-15: revised
- 2024-11-06: received
- See all versions
- Short URL
- https://ia.cr/2024/1819
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2024/1819,
author = {Devon Tuma and Nicholas Hopper},
title = {{VCVio}: A Formally Verified Forking Lemma and Fiat-Shamir Transform, via a Flexible and Expressive Oracle Representation},
howpublished = {Cryptology {ePrint} Archive, Paper 2024/1819},
year = {2024},
url = {https://eprint.iacr.org/2024/1819}
}
