Database of Case Studies Achieved Using CADP

Message Authentication Algorithm (MAA, ISO Standard 8731)

Organisation: National Physical Lab (NPL) UK

Method: LOTOS

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Cryptography.

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:
  1. Donald W. Davies and David O. Clayden. A Message Authenticator Algorithm Suitable for a Mainframe Computer. NPL Report DITC 17/83, National Physical Laboratory (Teddington, Middlesex, UK), February 1983.

  2. Donald Watt Davies. A Message Authenticator Algorithm Suitable for a Mainframe Computer. Proceedings of the Workshop on the Theory and Application of Cryptographic Techniques (CRYPTO'84), Santa Barbara, CA, USA, Lecture Notes in Computer Science (LNCS), vol. 196, pp. 393-400, Springer, August 1984.

  3. Donald W. Davies and David O. Clayden. The Message Authenticator Algorithm (MAA) and its Implementation. NPL Report DITC 109/88, National Physical Laboratory (Teddington, Middlesex, UK), February 1988. Available from http://www.cix.co.uk/~klockstone/maa.htm

  4. ISO/IEC International Standard 8731-2. International Organization for Standardization - Banking - Approved Algorithms for Message Authentication - Part 2: Message Authenticator Algorithm. Geneva, 1992.

  5. 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.

  6. Philippe Turlier. "La compilation des types abstraits algebriques du langage LOTOS". Mémoire d'ingénieur CNAM, Grenoble, December 1992.

  7. 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 http://cadp.inria.fr/publications/Garavel-Turlier-13.html

  8. Hubert Garavel and Lina Marsso. A Large Term Rewrite System Modelling a Pioneering Cryptographic Algorithm. Proceedings of the 2nd International Workshop on Models for Formal Analysis of Real Systems (MARS 2017), Uppsala, Sweden, April 2017. Available on-line from http://cadp.inria.fr/publications/Garavel-Marsso-17.html

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

This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies


Last modified: Fri Apr 21 16:19:49 2017.


Back to the CADP case studies page