Agile Cryptographic Agreement Protocol

Introduction

The goal of the proposed Agile Cryptographic Agreement Protocol (ACAP) is to give all secure communication prerequisites to the communicating parties. ACAP, after a successful exchange, provides the communicating parties with the following prerequisites:

A shared secret established through Diffie Hellman that can be used to provide perfect forward secrecy.
Public keys used for authentication.
List of cryptographic algorithms supported by both communicating parties, that will later be used to ensure the needed security attributes.

Message definition

The role I represents the initiator in the communication and role R represents the responder in the communication.

Formal model verification

The message exchange was modelled and verified by using the Scyther tool.
The final model can be accessed here.
The model consists of three roles:

Initiator role I that intiates the message exchange (a.k.a. client).
Responder role R that responds to the initiator request (a.k.a. server).
Executability role O that is used to describe the needed events to formally verify the Diffie-Hellman exchange used in ACAP.

Each role consits of send (e.g. send_1) and receive (e.g. recv_1) events. Certain events have the exclamation mark sign ! before their respective number. This means that the message should be sent to all roles in the verification. In this way we ensure that the excutability role O gets the message containing the Diffie-Hellman exhange and changes it appropriately and sends to the other side.
For further information on SPDL syntax please refer to the Scyther manual and protocol examples.

Scyther compilation

Even though the Scyther tool has a nice GUI the model was verified by using the scyther command line tool. The tool was downloaded and compiled for 64-bit architecture from the official GitHub repository. The compilation was done on a Debian/Ubuntu system.

$ git clone https://github.com/cascremers/scyther.git
$ cd scyther/
$ sed -i "s/-m32/-m64/" src/BuildUnix.cmake
$ sudo aptitude install cmake build-essential flex bison gcc-multilib
$ make
$ file gui/Scyther/scyther-linux
gui/Scyther/scyther-linux: ELF 64-bit LSB executable, x86-64, ...

The 64-bit binary was needed because the solution space created by scyther during verifications with higher number of runs (number_of_runs>5) or by using unbounded verification resulted in RAM usage higher than 2³² bits (roughly 4GB of RAM). The maximum memory usage when performing unbounded verification of ACAP for certain claims was up to 13GB, so a machine with 16GB RAM should be OK.

Model verification

After compiling scyther we can check whether the defined model acutally works out. This is done by using the characterize option in scyther.

$ cd scyther
$ wget public.tel.fer.hr/acap/acap.spdl
$ src/scyther-linux -c -r 3 acap.spdl
claim	acap,I	Reachable_I8	-   Ok	[at least 1 variant]
claim	acap,R	Reachable_R8	-   Ok	[at least 1 variant]

Scyther can also produce a nice output by using the dot format. The output of this verification (after transforming dot to png) is shown in the following figures:

The final verification step can be done by using the following script. The script takes the number of runs as the first argument and sequentially checks whether all defined claims are satisfied. Sample code for unbounded verification (runs=0), and the verification results are shown below.
NOTE: Unbounded verification can take a really long time (up to 3 days) depending on the resources available. It is advised to use a smaller amount of runs (3, 4 or 5) for testing.

$ cd scyther
$ wget public.tel.fer.hr/acap/scyther_script.sh
$ chmod +x scyther_script.sh
$ runs=0
$ ./scyther_script.sh $runs
claim	acap,I	SKR_I2	KDF(h(Gr,i))	Ok  [no attack within bounds]
claim	acap,R	SKR_R2	KDF(h(Gi,r))	Ok  [no attack within bounds]
claim	acap,I	Weakagree_I3	-   Ok	[no attack within bounds]
claim	acap,R	Weakagree_R3	-   Ok	[no attack within bounds]
claim	acap,I	Commit_I4   (R,g(i),Gr)	Ok  [no attack within bounds]
claim	acap,R	Commit_R4   (I,g(r),Gi)	Ok  [no attack within bounds]
claim	acap,I	Alive_I5    -	Ok  [no attack within bounds]
claim	acap,R	Alive_R5    -	Ok  [no attack within bounds]
claim	acap,I	Niagree_I6  -	Ok  [no attack within bounds]
claim	acap,R	Niagree_R6  -	Ok  [no attack within bounds]
claim	acap,I	Nisynch_I7  -	Ok  [no attack within bounds]
claim	acap,R	Nisynch_R7  -	Ok  [no attack within bounds]

Prototype implementation and evaluation

A prototype of acap has been implemented in Python3. Installation procedure for Debian jessie is as follows:

$ sudo aptitude install gcc python3-dev python3-crypto python3-pip libffi-dev \
python3-cffi python3-setuptools libssl-dev
$ sudo pip3 install --upgrade cffi
$ sudo pip3 install netifaces
$ sudo pip3 install cryptography

The implementation can be accessed here.
Packet captures for different communication protocols and layers: TCP UDP IP Ethernet
Sample output for running server and client on the localhost:

# ./server
Refreshed DH and Nonce...
INFO - Server negotiated: 
{
    "hash": {
        "algorithm": "SHA-256",
        "timestamp": "2015-08-27 14:52"
    },
    "public_key": {
        "algorithm": "ECDSA_192",
        "timestamp": "2015-08-27 14:52"
    },
    "secret_key": {
        "algorithm": "AES-CTR_256",
        "timestamp": "2015-08-27 14:52"
    }
}
INFO - Shared secret key (256 bit): 6f:54:52:cd:05:b1:49:92:d3:ef:df:40:a2:06:20:8c:8a:c5:29:44:c0:b4:32:3b:b1:b0:8f:91:27:01:f6:7f
INFO - TOTAL duration: 10919
...

# ./client
INFO - Client negotiated: 
{
    "hash": {
        "algorithm": "SHA-256",
        "timestamp": "2015-08-27 14:52"
    },
    "public_key": {
        "algorithm": "ECDSA_192",
        "timestamp": "2015-08-27 14:52"
    },
    "secret_key": {
        "algorithm": "AES-CTR_256",
        "timestamp": "2015-08-27 14:52"
    }
}
INFO - Shared secret key (256 bit): 6f:54:52:cd:05:b1:49:92:d3:ef:df:40:a2:06:20:8c:8a:c5:29:44:c0:b4:32:3b:b1:b0:8f:91:27:01:f6:7f
INFO - TOTAL duration: 36012

Message formats are derived from the message definition and are as follows: