National Physical Lab (NPL) UK
(and many others)
CADP (Construction and Analysis of Distributed Processes)
1100 lines of LOTOS, 1700 lines of LNT.
The Message Authentication Algorithm (MAA, ISO Standard 8731) is a
cryptographic algorithm intended to secure banking transactions. Given a
file and a key (a character string), the MAA algorithm computes a
digital signature, using one-way hashing functions. The signature is
called Message Authentication Code (MAC).
A formal description in LOTOS of the MAA algorithm was written by Harold B. Munster at the National Physical Laboratory (UK). This description uses only the abstract data types of LOTOS.
Then this description was slighty adapted by Hubert Garavel and Philippe Turlier so that the CAESAR.ADT compiler could be efficiently used, to translate the Abstract Data Types to a C program.
This case study is an application of Abstract Data Types to the formal
description of a cryptographic algorithm.
Using the CAESAR.ADT compiler, we showed that specification can be (with small adaptations) compiled into executable code. The C code we obtained allowed us to compute the MAC signature for large Unix files (up to 30,000 bytes).
655 avenue de l'Europe
38330 Montbonnot Saint Martin
Tel: +33 4 76 61 52 24
Fax: +33 4 76 61 52 52
The LOTOS description as well as explanations on the verification with
CADP are available on-line at :
This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies