# HAL: A Library for Homomorphic Authentication

## Overview

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 *s*_{x}; next, anyone can compute an
authentication tag *s*_{f,y} that certifies the value
*y=f(x)* as output of function *f*; *s*_{f,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.

### Homomorphic Authenticators

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*s*_{x1}, ...,*s*_{xn}corresponding to dataset*D*, inputs*x1, ..., xn*and labels*L1, ..., Ln*respectively, yields a tag*s*_{f,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.

#### Homomorphic Authenticators with Efficient Verification

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***)**-->*vk*_{f}, which returns a verification key bound to the function*f*and its input labels.**Verify(***vk*_{f},*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.

## Implemented schemes

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.

## Pairing library

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.

## Build instructions

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

### Using HAL as a library

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.

### Portability

We have tested the library on:

- macOS 10.12.1 (Sierra)
- Linux Mint 18 Cinnamon 3.0.7 64-bit

## Tutorials

The library includes some usage examples.

### Basic usage

`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`

).

### Compiler for homomorphic computations

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_model`

file.Run

`$ test/createFunction test/func_file`

with 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**.

## Directory structure

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.

- fgp/ --- implementation of the
- 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.

## Authors

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 (dario.fiore@imdea.org) Martin Zuber (zubersmartin@gmail.com)

## References

[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