|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools Forum |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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 ), 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: |
[Serwe-15]
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 |
Back to the CADP case studies page