Database of Case Studies Achieved Using CADP

Message Authentication Algorithm (MAA, ISO Standard 8731)

Organisation: National Physical Lab (NPL) UK

Method: LOTOS
LNT
(and many others)

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

Domain: Cryptography.

Period: 1991-1993, 2016-2018

Size: 1100 lines of LOTOS, 1700 lines of LNT.

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

  9. Hubert Garavel and Lina Marsso. Comparative Study of Eight Formal Specifications of the Message Authenticator Algorithm. In Proceedings of the 3rd Workshop on Models for Formal Analysis of Real Systems and the 6th International Workshop on Verification and Program Transformation (MARS/VPT'18), Thessaloniki, Greece, April 2018 Available on-line from http://cadp.inria.fr/publications/Garavel-Marsso-18.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: [email protected]
Further remarks: The LOTOS description as well as explanations on the verification with CADP are available on-line at : http://cadp.inria.fr/ftp/demos/demo_12

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

Last modified: Mon Jul 4 11:03:34 2022.

Back to the CADP case studies page