rule defining a non-constructor $f$ must have the form “$f (P_1, ..., P_n) \rightarrow ...$”, where each $P_i$ contains only constructors and free variables; (iii) some LOTOS sorts and operations were implemented as C types and functions, by importing manually-written C code — for instance, addition, multiplication, and bit shifts on 32-bit words were implemented directly in C. From this specification, the [C[Æ]{}SAR.ADT]{} compiler could automatically generate C code that, combined with a small handwritten main program, computed the MAC value corresponding to a message and a key.

Specification of the MAA as a Term Rewrite System {#MODEL}
=================================================

Taking Garavel & Turlier’s LOTOS specification as a starting point, our central contribution is a formal model of the MAA specified as a term rewrite system. This model is expressed using the notations of the simple rewriting language REC proposed in [@Duran-Roldan-Balland-et-al-09 Sect. 3] and [@Duran-Roldan-Bach-10 Sect. 3.1], which was lightly enhanced to distinguish between free constructors (declared in the “” part) and non-constructors (declared in the “” part and defined by rewrite rules given in the “” part).

The model is given in Annex \[ANNEX-REC\] of the present article. Notice that the model has a few (only six) conditional rules 