The Community for Technology Leaders
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
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
233 ms
(Ver 3.3 (11022016))