Often, pairing-based cryptographic schemes are described using symmetric groups. While these groups simplify the description of new cryptographic schemes, they are rarely the most efficient setting for implementation. Asymmetric groups represent the state-of-the-art in terms of efficiency and converting schemes from symmetric to an asymmetric solution currently requires manual analysis. We demonstrate with AutoGroup how to automate such conversions using SMT solvers as a core building block.
AutoGroup: ACM CCS 2013
AutoGroup+ requires Python 3 or greater and you will need the Charm-Crypto framework (v0.43) to execute the automatically generated asymmetric scheme in Python and/or C++.
AutoGroup+ also requires the Z3 Theorem prover (with Python 3 bindings).
Here are the install steps for Z3:
git clone https://github.com/Z3Prover/z3.git python3 scripts/mk_make.py cd build make
Running The Tool
For the help menu, execute the following:
#: python3 runAutoGroup.py -h usage: runAutoGroup.py [-h] -o OUTFILE -s SDL [-v] -c CONFIG [-l LIBRARY] [-b] [-e] [--short SHORT] [--path PATH] [--print] [-a] sym.-to-asym. conversion for cryptographic schemes in SDL. optional arguments: -h, --help show this help message and exit -o OUTFILE, --outfile OUTFILE generate code of new scheme in C++/Python for Charm -s SDL, --sdl SDL input SDL file description of scheme -v, --verbose enable verbose mode -c CONFIG, --config CONFIG configuration parameters needed for AutoGroup -l LIBRARY, --library LIBRARY which library to benchmark against: miracl or relic -b, --benchmark benchmark AutoGroup execution time -e, --estimate estimate bandwidth for keys and ciphertext/signatures --short SHORT what to minimize: public-keys, secret-keys, assumption, ciphertext, signatures --path PATH destination for AutoGroup+ output files. Default: current dir --print print the selected options -a, --autogroup run AutoGroup only (and not AutoGroup+)
An example for how to execute AutoGroup on the Camenisch-Lysyanskaya (CL) signature scheme with basic options:
python3 runAutoGroup.py --sdl schemes/cl04.sdl --config schemes/configCL.py -o TestCL -v
Note that AutoGroup+ was designed to handle both encryption and signature schemes.
AutoGroup provides several configuration parameters to tune conversion to an asymmetric solution. The configuration file is specified in Python with the following options:
schemeType : for describing the type of input scheme. For public-key encryption,
"PKENC" and for signature types,
operation : to find a solution that reduces the computation time based on cost of
dropFirst : in the event that there are multiple solutions that satisfy the
"both" option of the
short representation requirement, users must specify what option to relax to constrain the options further. The options are
"signatures" for signatures and
"ciphertext" for encryption.
The next set of variables describe basic aspects of the signature or encryption scheme:
keygenPubVar: denotes the user's public-key
keygenSecVar: denotes the user's secret-key
signatureVar: denotes the signature if scheme type is
ciphertextVar: denotes the ciphertext if scheme type is
masterPubVars: denotes the public parameters available to all users of the system (if applicable)
masterSecVars: denotes the master secret-key (if applicable)
We require function names of algorithms described in the SDL specified as
keygenFuncName. Also, for signature schemes, must specify the
verifyFuncName. For encryption, must specify the
We provide a complete configuration file example for the CL signature:
schemeType = "PKSIG" operation = "exp" setupFuncName = "setup" keygenFuncName = "keygen" signFuncName = "sign" verifyFuncName = "verify" masterPubVars = None masterSecVars = None keygenPubVar = "pk" keygenSecVar = "sk" signatureVar = "sig"
See more examples in the
New SDL Structures
AutoGroup+ requires two new SDL inputs for a given scheme: (1) Reduction(s) and (2) Assumption(s).
For (1), we mean an analysis where there is an efficient algorithm called a reduction that is successful in solving the hard problem (underlying the complexity assumption (2)) given black-box access to an adversary that is able to successfully attack the scheme.
Note that AutoGroup+ assumes that the security reduction is correct, the complexity assumptions are true, and that the SDL was typed correctly. If any of these do not hold, then the output of AutoGroup+ cannot be relied upon.
For encryption schemes, the security reduction SDL input typically consists of three algorithms: setup, queries, and challenge. For signature schemes, it simply consists of two algorithms: setup and queries.
The assumption SDL input structure is self explanatory and we include several complexity assumptions from the literature. See the