Automatic inference of cryptographic key length based on analysis of proof tightness

Abstract

Currently, reasoning about key lengths within a security scheme involves utilizing generalized recommendations or conducting lengthy manual analyses of how security parameters relate to the security of the scheme. In this paper, we provide the tools necessary for automating reasoning about key lengths and effective security within a security scheme. We first formalize the reasoning about cryptographic proofs within an attack tree structure, then expand attack tree methodology to include cryptographic reductions. We then provide the algorithms for maintaining and automatically reasoning about these expanded attack trees. We provide a software tool that utilizes machine-readable proof and attack metadata and the attack tree methodology to provide rapid and precise answers regarding security parameters and effective security. This eliminates the need to rely on generalized recommendations and provides timely reanalysis when newfound attacks or proofs surface. We validate our software tool within the Schnorr public-key signature scheme as a case study.