more diverse behaviour, as they rather seek to perform irregular computations than linear ones.

The present article is organized as follows. Section \[MAA\] provides an algorithmic overview of the MAA. Section \[HISTORY\] lists the preexisting formal specifications of the MAA. Section \[MODEL\] presents the modelling of the MAA using term rewrite systems. Section \[VALIDATION\] discusses validation steps applied to this model. Finally, Section \[CONCLUSION\] gives concluding remarks.

Overview of the MAA {#MAA}
===================

Nowadays, Message Authentication Codes are computed using different families of algorithms based on either cryptographic hash functions (HMAC), universal hash functions (UMAC), or block ciphers (CMAC, OMAC, PMAC, etc.). Contrary to these modern approaches, the MAA was designed as a standalone algorithm that does not rely on any preexisting hash function or cipher.

In this section, we briefly explain the principles of the MAA. More detailed explanations can be found in [@Davies-85], [@Davies-Clayden-88] and [@Menezes-vanOorschot-Vanstone-96 Algorithm 9.68].

The MAA was intended to be implemented in software and to run on 32-bit computers. Hence, its design intensively relies on 32-bit words (called [*blocks*]{}) and 32-bit machine operations.

The MAA takes as inputs a key and a message. The key has 64 bits and is split into two blocks 