|
| 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 |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
Formal Specification and Verification of Fully Asynchronous Implementations of the Data Encryption Standard
Wendelin Serwe
Proceedings of the International Workshop on Models for Formal Analysis of Real Systems (MARS 2015), Suva, Fiji
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.
| 87 pages |  |
 PostScript |
| Slides of W. Serwe's lecture at MARS'2015: | |
ERRATUM [Oct 22, 2020]
There was a minor error in Figure 1 on page 63: the link OUTPUT_R goes from CHOOSE_R to IIP, rather than from XOR_32 to IIP. Noticeably, the LNT and LOTOS code in the appendices of the paper was correct. Here is the revised figure:
