Security in the Generic Group Model is a standard requirement for new hardness assumptions in (bilinear) groups. Recently, the Generic Group Model has also been increasingly used to prove the security of new cryptographic constructions such as algebraic MACs or structure-preserving signature schemes. Since pen-and-paper proofs in the Generic Group Model are usually tedious and hard to write and verify, they might contain errors that go unnoticed. We address this problem by developing a new method to automatically prove security statements in the Generic Group Model as they occur in actual papers. Existing tools like the one by Barthe et al. (CRYPTO'14) and an extended version by Barthe et al. (PKC'15) have severe limitations that prevent them from achieving this goal: The first tool cannot deal with oracles that take handle variables, as required for example for structure preserving signature schemes. The second tool only performs proofs with respect to a bounded number of oracle queries and standard (unbounded) security definitions are therefore out of scope. To lift these limitations, we develop a completely new approach to prove the security of cryptographic constructions in the Generic Group Model. We start by defining (i) a general language to describe security definitions, (ii) a class of logical formulas that characterize how an adversary can win, and (iii) a translation from security definition to such formulas. Our master theorem relates the security of the construction to the existence of a solution for the associated logical formula. Next, we define a constraint solving algorithm that proves the security of a construction by proving the absence of solutions. Finally, we report on the fully automated gga∞ tool that implements the algorithm. We demonstrate the effectiveness and performance of the gga∞ tool on a significant number of examples from the literature.