| Organisation: |
National Physical Lab (NPL) UK
|
| Method: |
LOTOS
|
| Tools used: |
CADP (Construction and Analysis of Distributed Processes)
|
| Domain: |
Cyptography
|
| Period: |
1991-1993
|
| Size: |
1110 lines of LOTOS.
|
| Description: |
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.
|
| Conclusions: |
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).
|
| Publications: |
- ISO/IEC International Standard 8731-2. International Organization for
Standardization - Banking - Approved Algorithms for Message
Authentication - Part 2: Message Authenticator Algorithm. Geneva, 1992.
- Harold B. Munster, "LOTOS Specification of the MAA Standard, with an
Evaluation of LOTOS", NPL Report DITC 191/91, National Physical
Laboratory (Teddington, Middlesex, UK), September 1991.
- Philippe Turlier. "La compilation des types abstraits algebriques du
langage LOTOS" Mémoire d'ingénieur CNAM, Grenoble, December 1992.
- Hubert Garavel and Philippe Turlier, "CAESAR.ADT: Un compilateur pour
les types algebriques du langage LOTOS", In Rachida Dssouli and
Gregor v. Bochmann, editors, Actes du Colloque Francophone pour
l'Ingénierie des Protocoles CFIP'93 (Montréal, Canada), 1993.
Available on-line from the VASY FTP site in
PDF
or
PostScript 
|
| Contact: |
Hubert Garavel
INRIA Rhone-Alpes
655 avenue de l'Europe
38330 Montbonnot Saint Martin
FRANCE
Tel: +33 4 76 61 52 24
Fax: +33 4 76 61 52 52
E-mail: Hubert.Garavel@inria.fr
|
| Further remarks: |
The LOTOS description as well as explanations on the verification with
CADP are available on-line at :
ftp://ftp.inrialpes.fr/pub/vasy/demos/demo_12.tar.Z
This case-study, amongst others, is described on the CADP Web Page :
http://cadp.inria.fr
|
Back to the CADP case studies page