Automated Proofs of Signatures using Bilinear Pairings
Guruprasad Eswaraiah, Roopa Vishwanathan, Douglas Nedza · 2018
In this paper, we extend an automated proof-generation tool, AutoG& P with new axioms and formalizations to support composite data types and q-type assumptions, which in turn can be used to automate pairing-based signature schemes. AutoG& P due to Barthe et at. was designed as a tool to automate proofs of cryptographic primitives based on bilinear pairings in the standard model, but the initial version only supported a limited set of data types, limited pairing-based assumptions, and only provided automated proofs for encryption schemes, notably the Boneh-Boyen identity-based encryption scheme. As examples of our extensions, we provide automated proofs for the Boneh-Boyen pairing-based signature schemes under the well-known and widely-used notion of signature security: existential unforgeability under chosen message attacks in the standard model, and the Boneh-Boyen-Shacham group signature scheme, under standard notions of group signature security: anonymity and traceability.