PPE Circuits for Rational Polynomials

Pairings are a powerful algebraic setting for realizing cryptographic functionalities. One challenge for cryptographers who design pairing systems is that the complexity of many systems in terms of the number of group elements and equations to verify has been steadily increasing over the past decade and is approaching the point of being unwieldy. To combat this challenge, multiple independent works have utilized computers to help with the system design. One common design task that researchers seek to automate is summarized as follows: given a description of a set of trusted elements T (e.g., a public key) and a set of untrusted elements U (e.g., a signature), automatically generate an algorithm that verifies U with respect to T using the pairing and group operations. To date, none of the prior automation works for this task have support for solutions with rational polynomials in the exponents despite many pairing constructions employing them (e.g., Boneh-Boyen signatures, Gentry's IBE, Dodis-Yampolskiy VRF). We demonstrate how to support this essential class of pairing systems for automated exploration. Specifically, we present a solution for automatically generating a verification algorithm with novel support for rational polynomials. The class of verification algorithms we consider in this work is called PPE Circuits (introduced in [HVW20]). Intuitively, a PPE Circuit is a circuit supporting pairing and group operations, which can test whether a set of elements U verifies with respect to a set of elements T. We provide a formalization of the problem, an algorithm for searching for a PPE Circuit supporting rational polynomials, a software implementation, and a detailed performance evaluation. Our implementation was tested on over three dozen schemes, including over ten test cases that our tool can handle, but prior tools could not. For all test cases where a PPE Circuit exists, the tool produced a solution in three minutes or less.