first MAC algorithm to gain widespread acceptance was the Message Authenticator Algorithm (also known as Message Authentication Algorithm, MAA for short) [@Davies-85] [@Davies-Clayden-88] [@Preneel-11] designed in 1983 by Donald Davies and David Clayden at the National Physical Laboratory (NPL) in response to a request of the UK Bankers Automated Clearing Services. The MAA was adopted by ISO in 1987 and became part of the international standards 8730 [@ISO-8730:1990] and 8731-2 [@ISO-8731-2:1992]. Later, cryptanalysis of MAA revealed various weaknesses, including feasible brute-force attacks, existence of collision clusters, and key-recovery techniques [@Preneel-vanOorschot-96] [@Rijmen-Preneel-DeWin-96] [@Preneel-Rumen-vanOorschot-97] [@Preneel-vanOorschot-99] [@Preneel-11]. For this reason, MAA was withdrawn from ISO standards in 2002.

From the point of view of formal methods, the MAA is interesting because of its pioneering nature, because its definition is freely available and stable, and because it is involved enough while remaining of manageable complexity. Over the past decades, various formal specifications of the MAA have been developed using VDM, Z, abstract data types (i.e., algebraic specifications), term rewrite systems, etc. For such formalisms, the usual examples often deal with syntax trees, which are explored using standard traversals (breadth-first, depth-first, etc.); contrary to such commonplace examples, cryptographic functions (and the MAA, in particular) exhibit 