Organisation: 
INRIA Grenoble RhôneAlpes / 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 symmetrickey encryption
algorithm, that has been for almost 30 years Federal Information
Processing Standard FIPS46. 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 8byte block ciphers, e.g., for secure payment systems.
An interesting aspect of the DES is that it is specified by a dataflow 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/casestudies/03ides.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: 
[Serwe15]
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 online at: http://cadp.inria.fr/publications/Serwe15.html 
Contact:  Wendelin Serwe INRIA Grenoble RhôneAlpes / CONVECS 655, avenue de l'Europe 38330 Montbonnot SaintMartin 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 casestudy, amongst others, is described on the CADP Web site: http://cadp.inria.fr/casestudies 