Comparative Study of Eight Formal Specifications of the Message Authenticator Algorithm

TL;DR

This paper compares eight formal specifications of the Message Authenticator Algorithm, evaluating their clarity, conciseness, and suitability for code generation to improve understanding and implementation of cryptographic standards.

Contribution

It provides a comprehensive comparison of multiple formal specifications of the MAA, highlighting their strengths and weaknesses across various criteria.

Findings

Specifications vary in conciseness and readability

Some specifications are more efficient for code generation

The study offers insights into formal methods for cryptographic algorithms

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.