Formal Specification and Verification of Fully Asynchronous Implementations of the Data Encryption Standard

Wendelin Serwe 1, *
* Corresponding author
1 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : This paper presents two formal models of the Data Encryption Standard (DES), a first using the international standard LOTOS, and a second using the more recent process calculus LNT. Both models encode the DES in the style of asynchronous circuits, i.e., the data-flow blocks of the DES algorithm are represented by processes communicating via rendezvous. To ensure correctness of the models, several techniques have been applied, including model checking, equivalence checking, and comparing the results produced by a prototype automatically generated from the formal model with those of existing implementations of the DES. The complete code of the models is provided as appendices and also available on the website of the CADP verification toolbox.
Document type :
Conference papers
Rob van Glabbeek; Jan Friso Groote; Peter Höfner. Proceedings of the first Workshop on Models for Formal Analysis of Real Systems (MARS 2015), Nov 2015, Suva, Fiji. 196, 2015, Electronic Proceedings in Theoretical Computer Science, Proceedings of the first Workshop on Models for Formal Analysis of Real Systems (MARS 2015). 〈10.4204/EPTCS.196.6〉
Liste complète des métadonnées

Cited literature [3 references]  Display  Hide  Download

https://hal.inria.fr/hal-01227999
Contributor : Wendelin Serwe <>
Submitted on : Monday, November 23, 2015 - 11:05:04 AM
Last modification on : Friday, November 27, 2015 - 1:02:52 AM
Document(s) archivé(s) le : Friday, April 28, 2017 - 2:53:23 PM

Identifiers

Collections

Citation

Wendelin Serwe. Formal Specification and Verification of Fully Asynchronous Implementations of the Data Encryption Standard. Rob van Glabbeek; Jan Friso Groote; Peter Höfner. Proceedings of the first Workshop on Models for Formal Analysis of Real Systems (MARS 2015), Nov 2015, Suva, Fiji. 196, 2015, Electronic Proceedings in Theoretical Computer Science, Proceedings of the first Workshop on Models for Formal Analysis of Real Systems (MARS 2015). 〈10.4204/EPTCS.196.6〉. 〈hal-01227999〉

Share

Metrics

Record views

201

Files downloads

126