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.

Pairing-based cryptography is widely used for its efficiency and functionality. When designing pairing-based schemes, one common task is to devise algorithms for verifying a set of untrusted group elements with respect to a set of trusted group elements. One might be searching for a verification algorithm for a signature scheme or a method for verifying an IBE/ABE private key with respect to the IBE/ABE public parameters. In ACM CCS 2019 Hohenberger Vusirikala, the AutoPPE software tool was introduced for automatically generating a set of pairing product equations (PPEs) that can verify the correctness of a set of pairing group elements with respect to a set of trusted group elements. This task is non-trivial. Some schemes (e.g., those based on dual system encryption) provably do not support any efficient algorithm for verifying the private keys with respect to the public parameters. Other schemes (e.g., the Boyen-Waters anonymous IBE) were left in a gray area by Hohenberger-Vusirikala (CCS 19) -- no conjunction of PPEs was known for testing them, but no proof of untestability either.

Using a set of pairing product equations (PPEs) to verify the correctness of an untrusted set of pairing elements with respect to another set of trusted elements has numerous cryptographic applications. These include the design of basic and structure-preserving signature schemes, building oblivious transfer schemes from "blind" IBE, finding new verifiable random functions and keeping the IBE/ABE authority "accountable" to the user.

While the feasibility of constant-round and actively secure MPC has been known for over two decades, the last few years have witnessed a flurry of designs and implementations that make its deployment a palpable reality. To our knowledge, however, existing concretely efficient MPC constructions are only for up to three parties.