# Automated Cryptographic Analysis of the Pedersen Commitment Scheme

## TL;DR

This paper presents a formal, mechanised verification of the Pedersen commitment scheme, establishing its security properties and extending the EasyCrypt framework to support discrete logarithm and commitment abstractions.

## Contribution

It introduces a novel formal verification of Pedersen commitments and extends EasyCrypt to facilitate reasoning about discrete logarithms and commitment protocols.

## Key findings

- Proved correctness, perfect hiding, and computational binding of Pedersen commitments.
- Extended EasyCrypt framework to support discrete logarithm and commitment abstractions.
- Facilitates future verification of complex cryptographic protocols.

## Abstract

Aiming for strong security assurance, recently there has been an increasing interest in formal verification of cryptographic constructions. This paper presents a mechanised formal verification of the popular Pedersen commitment protocol, proving its security properties of correctness, perfect hiding, and computational binding. To formally verify the protocol, we extended the theory of EasyCrypt, a framework which allows for reasoning in the computational model, to support the discrete logarithm and an abstraction of commitment protocols. Commitments are building blocks of many cryptographic constructions, for example, verifiable secret sharing, zero-knowledge proofs, and e-voting. Our work paves the way for the verification of those more complex constructions.