Database of Case Studies Achieved Using CADP

Fully Asynchronous Model of the Data Encryption Standard

Organisation: INRIA Grenoble Rhône-Alpes / CONVECS

Method: LOTOS
LNT

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Cryptography.

Period: 2004 to 2016

Size: 588,785,433 states and 5,512,418,012 transitions,

Description: The Data Encryption Standard (DES) is a symmetric-key encryption algorithm, that has been for almost 30 years Federal Information Processing Standard FIPS-46. At present, the main weakness of the algorithm is its use of keys of 56 bits, which are too short to withstand brute force attacks. To address this issue, the Triple Data Encryption Algorithm (TDEA or Triple DES) variant applies the DES algorithm three times (encryption, decryption, encryption), using three different keys, and is still an approved symmetric cryptographic algorithm for 8-byte block ciphers, e.g., for secure payment systems.

An interesting aspect of the DES is that it is specified by a data-flow diagram, i.e., as a set of blocks communicating by message passing. Such an architecture is naturally asynchronous because there is no need for a global clock synchronizing these various blocks. Due to different interleavings of the block executions, the exists a risk that the DES execution produces a nondeterministic result, although this is not expected. This problem naturally lends itself to analysis with process calculi.

Extending a previous case study (see http://cadp.inria.fr/case-studies/03-i-des.html),">http://cadp.inria.fr/case-studies/03-i-des.html">http://cadp.inria.fr/case-studies/03-i-des.html), the fully asynchronous DES is considered, describing formal models of the DES in two different process calculi, namely the international standard LOTOS and the more recent LNT language, both supported by CADP. The LOTOS model of the DES was directly derived from the DES standard to experiment with the application of LOTOS for the analysis of asynchronous circuits. In August 2015, the LOTOS model was rewritten into an equivalent LNT model to fulfill the expectations of the MARS workshop. Both models have been analyzed using different techniques, namely data abstraction, model checking, equivalence checking, and the automatic generation of a prototype software implementation. All these verification steps have been automated by an SVL (Script Verification Language) script.



Conclusions: The Data Encryption Standard is an interesting benchmark example, because it is both complex and tractable (with current hardware and/or compositional techniques). Both of the two formal models illustrate an interesting feature of LOTOS and LNT, namely the possibility to easily change the implementation of a data type to transform a prototype implementation into an abstract model adapted to formal verification.

Publications: [cle] Wendelin Serwe. "Formal Specification and Verification of Fully Asynchronous Implementations of the Data Encryption Standard". Proceedings of the International Workshop on Models for Formal Analysis of Real Systems (MARS 2015), Suva, Fiji, November 2015.
Available on-line at: http://cadp.inria.fr/publications/Serwe-15.html
Contact:
Wendelin Serwe
INRIA Grenoble Rhône-Alpes / CONVECS
655, avenue de l'Europe
38330 Montbonnot Saint-Martin
FRANCE
Tel: +33 (0)4 76 61 53 52
Fax: +33 (0)4 76 61 52 52
Email: Wendelin.Serwe@inria.fr



Further remarks: This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies


Last modified: Wed Sep 28 10:55:58 2016.


Back to the CADP case studies page