Comparative Study of Eight Formal Specifications of the Message Authenticator Algorithm

Hubert Garavel 1 Lina Marsso 1
1 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : The Message Authenticator Algorithm (MAA) is one of the first cryptographic functions for computing a Message Authentication Code. Between 1987 and 2001, the MAA was adopted in international standards (ISO 8730 and ISO 8731-2) to ensure the authenticity and integrity of banking transactions. In 1990 and 1991, three formal, yet non-executable, specifications of the MAA (in VDM, Z, and LOTOS) were developed at NPL. Since then, five formal executable specifications of the MAA (in LOTOS, LNT, and term rewrite systems) have been designed at INRIA Grenoble. This article provides an overview of the MAA and compares its formal specifications with respect to common-sense criteria, such as conciseness, readability, and efficiency of code generation.
Document type :
Conference papers
MARS/VPT 2018 - 3nd Workshop on Models for Formal Analysis of Real Systems and the 6th International Workshop on Verification and Program Transformation, Apr 2018, Thessaloniki, Greece. 268, pp.41 - 87, 2018, 〈10.4204/EPTCS.268.2〉
Liste complète des métadonnées

Cited literature [29 references]  Display  Hide  Download

https://hal.inria.fr/hal-01775332
Contributor : Hubert Garavel <>
Submitted on : Wednesday, April 25, 2018 - 11:42:10 AM
Last modification on : Tuesday, June 5, 2018 - 2:15:59 PM

File

Garavel-Marsso-18.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Hubert Garavel, Lina Marsso. Comparative Study of Eight Formal Specifications of the Message Authenticator Algorithm. MARS/VPT 2018 - 3nd Workshop on Models for Formal Analysis of Real Systems and the 6th International Workshop on Verification and Program Transformation, Apr 2018, Thessaloniki, Greece. 268, pp.41 - 87, 2018, 〈10.4204/EPTCS.268.2〉. 〈hal-01775332〉

Share

Metrics

Record views

71

Files downloads

18