HAL is a software library that implements homomorphic authenticator (HA) schemes. An HA is a cryptographic primitive that allows for proving and verifying the integrity of computations on authenticated data. Informally speaking, this means that a party can use a secret key to authenticate a value x obtaining an authentication tag sx; next, anyone can compute an authentication tag sf,y that certifies the value y=f(x) as output of function f; sf,y can be eventually verified by anyone with knowledge of an appropriate (public or secret) verification key. This verification will ensure that y is indeed f(x), for an x correctly authenticated using the corresponding secret key.
Going a bit more in detail, an HA scheme includes the following algorithms:
- KeyGen, which generates a public evaluation key ek, a secret authentication key sk, and a verification key vk. If vk can be publicly released the HA is called a homomorphic signature, otherwise the scheme is called a homomorphic MAC.
- Auth( sk, D, L, x ) -->s, which on input the secret authentication key sk, a dataset name D, an input label L (a string), and a message x, returns an authentication tag s.
- Eval( f, s1,...,sn )-->s, which on input the description of an n-to-1 function f, and n authentication tags s1,...,sn, returns a new authentication tag s for the result.
- Verify( vk, f, _L1, ..., Ln, D, x, s ), which on input the verification key vk, the description of function f with input labels L1, ..., Ln, a dataset name D, a message x and an authentication tag s, returns accept or reject.
A tuple of algorithms such the ones described above is an homomorphic authenticator if it offers the following properties.
- Correctness: applying Eval on valid tags sx1, ..., sxn corresponding to dataset D, inputs x1, ..., xn and labels L1, ..., Ln respectively, yields a tag sf,y that verifies against function f, labels L1, ..., Ln, dataset D, and message f(x1, ..., xn).
- Succinctness: the size of authentication tags is short and independent of the input size.
- Security: without the scheme's secrets it is computationally infeasible to create valida tags for false computations results.
For formal definitions and theoretical discussions about these, see [GW13], [CF13], [BFR13], and references therein.
An interesting class of HA schemes (considered in the library) are those that offer efficient verification. The difference is that the Verify algorithm can be "split" in two algorithms:
- VerifyPrep( vk, f, L1, ..., Ln )--> vkf, which returns a verification key bound to the function f and its input labels.
- Verify( vkf, D, x, s ), which on input the verification key generated as above, a dataset name D, a message x and an authentication tag s, returns accept or reject.
Essentially, VerifyPrep creates a verification key that is independent of the dataset name D and thus can be reused to verify computations of the same function f on different datasets D1, D2, etc. Notably, this way the running of Verify becomes independent of f and, in most constructions, constant in the input size.
The HAL library currently provides an implementation of:
-
fgp. An homomorphic MAC with efficient verification for degree-2 arithmetic circuits over polynomials (see below for more details). This is the scheme implicitly described in [FGP14].
The message space of this scheme is the polynomial ring Z[X,Y]/qZ, where q is a prime number that is the order of the bilinear groups used by the scheme. "Fresh messages" (i.e., those taken by Auth) have degree at most 1 in Y and degree at most d in X. The messages taken by Verify are expected to have degree at most 2 in Y and 2*d in X. The class of functions f supported by this scheme are arithmetic circuits of multiplicative depth 1 (degree 2) where additions and multiplications are over the ring Z[X,Y]/qZ. In the special case in which the message values are constant polynomials (i.e., of degree 0 in both X and Y), the scheme almost matches the homomorphic MAC described in [BFR13].
-
cf13. The homomorphic MAC for arithmetic circuits described in [CF13].
The message space of this scheme is the ring Z/qZ, where q is an arbitrary prime number whose bitsize determines the security of the scheme.
-
A collection of utilities that can be common to several schemes, such as the implementation of a PRF mapping binary strings into integers in a finite ring, and a tool that allows to write a (degree-2) algorithm and compiles into C code that corresponds to the homomorphic computation over tha authentication tags, the verification keys, and the messages.
For those HA schemes that use pairings (e.g., fgp) the HAL library uses the [RELIC] library, and in particular its instantiation of a Barreto-Naehrig curve, providing 128 bits of security. RELIC is also used to handle most of Zq arithmetic operations.
HAL is written in C and relies on the following:
- GMP for multi-precision arithmetic
- RELIC for elliptic-curve- and pairing-based schemes
- FLINT for polynomial operations
After GMP, RELIC and FLINT are installed (they are supposed to be in /usr/local, this can be changed in the Makefile), you can build the library by running:
$ bash configure
$ make hal-crypto
If you wish to use HAL as a library, so that you can write your code in any directory and link it against HAL, run:
$ make lib
This creates a file libhal-crypto.a into ./lib
To install the library, run:
$ make install PREFIX=/installation-path
This will install hal-crypto.a into /installation-path/lib, and the
required headers into /installation-path/include/hal-crypto/. So your
application should be linked using -L/installation-path/lib -lhal-crypto,
and compiled using -I/installation-path/include/hal-crypto.
By default (if the PREFIX is not set) the library will be installed
in /usr/local. Note that in that case, as well as in any case where
the path you give requires super-user privileges, you should run the
command preceded by sudo.
We have tested the library on:
- macOS 10.12.1 (Sierra)
- Linux Mint 18 Cinnamon 3.0.7 64-bit
The library includes some usage examples.
test/sample_test.c contains a usage example of the library with the
fgp scheme. The code essentially generates random messages and
applies a degree 2 computation on them. The result is then checked.
An executable can be built from that source file by running
$ make test
This will create the test/sampleTest executable which should, when
run, print Verification SUCCESSFUL to standard output.
A similar file test/cf_test.c contains a usage example with the
cf13 homomorphic MAC (to be compiled with make cftest).
The library makes available a tool for writing the code of a function in a generic way, and for compiling this code into C code for executing this function over the message space, the authentication tags, and the verification keys (for verification preparation). To use this utility do the following:
-
Write a generic function in a file using the instruction and model given in the
test/func_modelfile. -
Run
$ test/createFunction test/func_filewith the file you just wrote (e.g.,test/func_file) as parameter. -
Run $ make test2
-
Run the test/sampleTest2 executable that was created to test the computation.
If you wish to use the compiled functions in your own code, you can
stop at step 2 and use the code in test/sample_test2.c as reference.
At the moment this compiler utility works only for fgp.
The directory structure of the library is as follows:
- src/ --- main C source code, which contains the following modules:
- fgp/ --- implementation of the fgp homomorphic MAC
- cf13/ --- implementation of the cf13 homomorphic MAC
- utils/ --- implementation of some utility functions such as a pseudorandom function, conversions between various (big) integer types, random numbers generaton, and error handling.
- include/ --- headers files, following the same structure of src
- test/ --- a test source file as described above
- func --- a directory with source files and headers associated with the function creation options
- lib/ --- will store the libhal-crypto.a static library
- obj/ --- will contain object files after compilation
- doxygen/ --- doxygen configuration file for the library and a script for generating a documentation pdf file.
The HAL library is developed by Martin Zuber and Dario Fiore, and is released under the MIT License (see the LICENSE file).
Copyright (c) 2016-2017 Dario Fiore ([email protected]) Martin Zuber ([email protected])
[BFR13] Verifiable Delegation of Computation on Outsourced Data , Michael Backes, Dario Fiore, Raphael M. Reischuk, ACM Conference on Computer and Communications Security (ACM CCS) 2013
[CF13] Practical Homomorphic MACs for Arithmetic Circuits , Dario Catalano and Dario Fiore, EUROCRYPT 2013
[FGP14] Efficiently Verifiable Computation on Encrypted Data , Dario Fiore, Rosario Gennaro, and Valerio Pastro, ACM Conference on Computer and Communications Security (ACM CCS) 2014
[GW13] Fully Homomorphic Message Authenticators , Rosario Gennaro and Daniel Wichs, ASIACRYPT 2013
[RELIC] RELIC is an Efficient LIbrary for Cryptography , D. F. Aranha and C. P. L. Gouvea