PhD student Roberto Metere and his supervisor Dr. Changyu Dong, recently received the Best Paper Award for their paper “Automated Cryptographic Analysis of the Pedersen Commitment Scheme” at the 7th International Conference on Mathematical Methods, Models and Architectures for Computer Networks Security (MMM-ACNS 2017)
The conference was held 28 - 30 August in Warsaw, Poland. The paper was selected, after careful consideration by the technical program committee chairs, from 25 papers presented in the conference. Roberto and Dr Dong are in the Secure and Resilient Systems group (SRS), School of Computing.
"We are using cryptography every day. You do not see it, but it in your browser, in the Apps you use, in nearly everything networked to thwart attacks from the insecure cyber space. However, the increasing complexity in the design of cryptographic algorithms and protocols leads to a problem:
Can we trust them?
Are they really that secure as claimed?
Traditionally, we relied on mathematical proofs that are written on paper and checked by experts. But the increasing complexity of the design means that the proofs are getting longer and more complex. It is no long that easy to generate and check a proof. People make mistakes and when a tiny mistake is embedded somewhere in tens or even hundreds pages of proofs, it is almost impossible to find. In fact, it happened, many times, that protocols believed to be secure, even for years, were found to be vulnerable to attacks after further investigation. As a result, it is highly desirable to have tools that can formally and automatically verify cryptographic protocols, proving or disproving its security."
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, the paper 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.
The paper paves the way for the verification of those more complex constructions.
published on: 11 September 2017