$i$-th segment being inserted before the first block of the $(i+1)$-th segment. Finally, the MAC for the entire message is the MAA result $Z_n$ computed for the last segment.

Prior Formal Specifications of the MAA {#HISTORY}
======================================

The informal description of the MAA can be found both in ISO standard 8731-2 [@ISO-8731-2:1992] or in a 1988 NPL technical report [@Davies-Clayden-88]. On this basis, several formal models of the MAA have been developed:

-   In 1990, G. I. Parkin and G. O’Neill designed a formal specification of the MAA in VDM [@Parkin-ONeill-90] [@Parkin-ONeill-91]. To our knowledge, this was the first attempt at applying formal methods to the MAA. The VDM specification became part of the ISO standard defining the MAA [@ISO-8731-2:1992 Annex B]. Three implementations in C [@Parkin-ONeill-90 Annex C], Miranda [@Parkin-ONeill-90 Annex B], and Modula-2 [@Lampard-91] were written by hand along the lines of the VDM specification.

-   In 1991, M. K. F. Lai formally described the MAA using the set-theoretic Z notation [@Lai-91]. He adopted Knuth’s “literate programming” approach, by inserting formal fragments of Z code in the natural-language description of the MAA.

-   In 1991, Harold B. Munster produced a formal specification of the MAA in LOTOS [@Munster-91-a]. 