2014 IEEE 27th Computer Security Foundations Symposium (CSF) (2014)

Vienna, Austria

July 19, 2014 to July 22, 2014

ISSN: 1063-6900

ISBN: 978-1-4799-4290-9

pp: 153-165

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/CSF.2014.19

Joseph A. Akinyele , Johns Hopkins Univ. & Zeutro LLC, Baltimore, MD, USA

Gilles Barthe , IMDEA Software Inst., Madrid, Spain

Benjamin Gregoire , INRIA Sophia-Antipolis Mediterranee, Sophia-Antipolis, France

Benedikt Schmidt , IMDEA Software Inst., Madrid, Spain

Pierre-Yves Strub , IMDEA Software Inst., Madrid, Spain

ABSTRACT

Many algorithms admit very efficient batch versions that compute simultaneously the output of the algorithms on a set of inputs. Batch algorithms are widely used in cryptography, especially in the setting of pairing-based computations, where they deliver significant speed-ups. AutoBatch is an automated tool that computes highly optimized batch verification algorithms for pairing-based signature schemes. Thanks to finely tuned heuristics, AutoBatch is able to rediscover efficient batch verifiers for several signature schemes of interest, and in some cases to output batch verifiers that outperform the best known verifiers from the literature. However, AutoBatch only provides weak guarantees (in the form of a LaTeX proof) of the correctness of the batch algorithms it outputs. In this paper, we verify the correctness and security of these algorithms using the EasyCrypt framework. To achieve this goal, we define a domain-specific language to describe verification algorithms based on pairings and provide an efficient algorithm for checking (approximate) observational equivalence between expressions of this language. By translating the output of AutoBatch to this language and applying our verification procedure, we obtain machine-checked correctness proofs of the batch verifiers. Moreover, we formalize notions of security for batch verifiers and we provide a generic proof in EasyCrypt that batch verifiers satisfy a security property called screening, provided they are correct and the original signature is unforgeable against chosen-message attacks. We apply our techniques to several well-known pairing-based signature schemes from the literature, and to Groth-Sahai zero-knowledge proofs.

INDEX TERMS

Equations, Public key, Probabilistic logic, Optimization, Approximation algorithms

CITATION

J. A. Akinyele, G. Barthe, B. Gregoire, B. Schmidt and P. Strub, "Certified Synthesis of Efficient Batch Verifiers,"

*2014 IEEE 27th Computer Security Foundations Symposium (CSF)*, Vienna, Austria, 2014, pp. 153-165.

doi:10.1109/CSF.2014.19