{'fraction_non_alphanumeric': 0.040158987192698364, 'fraction_numerical': 0.01719417046960106, 'mean_word_length': 4.469565217391304, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 2, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 5, 'word_list_counts': {'cursed_substrings.json': 24, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Specifying a Cryptographical Protocol in Lustre and SCADE

We present SCADE and Lustre models of the Message Authenticator Algorithm (MAA), which is one of the first cryptographic functions for computing a message authentication code. The MAA was adopted between 1987 and 2001, in international standards (ISO 8730 and ISO 8731-2), to ensure the authenticity and integrity of banking transactions. This paper discusses the choices and the challenges of our MAA implementations. Our SCADE and Lustre models validate 201 official test vectors for the MAA.


Introduction
One of the first Message Authentication Code (MAC) algorithms to gain widespread acceptance was the Message Authenticator Algorithm (MAA, also known as the Message Authentication Algorithm) [5,6,21] designed in 1983 by Donald Davies and David Clayden. The MAA was adopted by ISO in 1987 and became part of the international standards 8730 [10] and 8731-2 [11]. Later, cryptanalysis of the MAA revealed various weaknesses, including feasible brute-force attacks, existence of collision clusters, and key-recovery techniques [22,26,24,23,21]. For this reason, the MAA was withdrawn from ISO standards in 2002. Even if the MAA was deprecated, as it happens to every cryptographic protocol as time passes, various formal specifications of the MAA have been developed before and after 2002. Most likely because the MAA wqs the first message authentication code algorithm and its definition is stable and will not change anymore. Moreover, it was designed as a standalone algorithm that does not rely on any preexisting hash function or cipher and, hence, has manageable complexity. The existing formal specifications of the MAA are either non-executable, such as the VDM one in 1990 [19,20], the Z one in 1991 [15], the LOTOS one in 1990/1991 [18,17] or executable, such as the LOTOS one ( [8]), the LNT one ( [8]), and those automatically derived from a term rewrite system ( [7]). More details about these earlier formal specifications of the MAA are available in [8]. Thus, the MAA could be viewed as a sort of Rosetta stone 1 for formal methods. However, synchronous models of the MAA have been missing so far, and this is what the present article is about.
This paper brings MAA models in synchronous languages to enrich the collection of formal models for the MAA algorithm. More precisely, in this paper, we present a formal model of the MAA with the synchronous formal language Lustre [9] dedicated to design embedded control systems; and with the industrial formal language SCADE (Safety Critical Application Development Environment) [4]. We discuss implementation choices and challenges, common to both models, partly because the SCADE language is based on Lustre language. Finally, we explain how we test the two formal models with the complete set of test vectors derived from the initial specification [6]. The remainder of the paper is organized as follows. Section 2 presents the technical perspective of the MAA. The modeling of the MAA using the synchronous language SCADE/Lustre is described in Section 3. Section 4 precises how the SCADE and the Lustre models have been validated. Finally, Section 5 gives some concluding remarks and future work directions.

The MAA Algorithm
In data security, a Message Authentication Code (MAC) is a short sequence of bits that is computed from a given message; a MAC ensures both the authenticity and integrity of the message, i.e., that the message sender is the stated one and that the message contents have not been altered. The design of MAC usually involves cryptographic keys shared between the message sender and receiver, which makes it more secure under attacks. In this section, we briefly explain the principles of the MAA while more detailed explanations are provided in [5,6] and [16,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 J and K. The message is seen as a sequence of blocks. If the number of bytes of the message is not a multiple of four, extra null bytes are added at the end of the message to complete the last block. The size of the message should be less than 1,000,000 blocks; otherwise, the MAA result is said to be undefined; we believe that this restriction, which is not inherent to the algorithm itself, was added in the second ISO standard [13] to provide MAA implementations with an upper bound (four megabytes) on the size of memory buffers used to store messages.
The MAA produces as output a block, which is the MAC value computed from the key and the message. The fact that this result has only 32 bits proved to be a major weakness enabling cryptographic attacks; MAC values computed by modern algorithms now have a much larger number of bits. Apart from the aforementioned restriction on the size of messages, the MAA behaves as a totally-defined function; its result is deterministic in the sense that, given a key and a message, there is only a single MAC result, which neither depends on implementation choices nor on hidden inputs, such as randomlygenerated numbers.
The MAA calculations rely upon conventional 32-bit logical and arithmetic operations, among which: AND (conjunction), OR (disjunction), XOR (exclusive disjunction), CYC (circular rotation by one bit to the left), ADD (addition), CAR (carry bit generated by 32-bit addition), MUL (multiplication, sometimes decomposed into HIGH MUL and LOW MUL, which denote the most-and least-significant blocks in the 64-bit product of a 32-bit multiplication). On this basis, more involved operations are defined, among which MUL1 (result of a 32-bit multiplication modulo 2 32 − 1), MUL2 (result of a 32-bit multiplication modulo 2 32 −2), MUL2A (faster version of MUL2), FIX1 and FIX2 (two unary functions 2 respectively defined as x → AND(OR(x,A),C) and x → AND(OR(x,B),D), where A, B, C, and D are the four hexadecimal block constants A = 02040801, B = 00804021, C = BFEF7FDF, and D = 7DFEFBFF). The MAA operates in three successive phases: • The PRELUDE takes the two blocks J and K of the key and converts them into six blocks X 0 , Y 0 , V 0 , W , S, and T . This phase is executed once. After the prelude, J and K are no longer used.
• The MAIN LOOP successively iterates on each block M n of the message (M 1 , ..., M n ). This phase maintains three variables X, Y , and V (initialized to X 0 , Y 0 , and V 0 , respectively), which are modified at each iteration. The main loop also uses the value of W , but does not use S and T . • The CODA adds the blocks S and T at the end of the message and performs two more iterations on these blocks. After the last iteration, the MAA result is XOR(X, Y ), called Z.
In 1987, the second ISO standard [11,Section 5] introduced an additional feature (called mode of operation), which concerns messages longer than 256 blocks, which was not present in the early MAA versions designed at NPL. Figure 1 gives an overview of "the mode of operation". Each message longer than 256 blocks must be split into segments of 256 blocks each, with the last segment possibly containing less than 256 blocks. The above MAA algorithm (prelude, main loop, and coda) is applied to the first segment, resulting in a value noted Z 1 . This block Z 1 is then inserted before the first block of the second segment, leading to a 257-block message to which the MAA algorithm is applied, resulting in a value noted Z 2 . This is done repeatedly for all the n segments, the MAA result Z i computed for the 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.

Modelling MAA in SCADE and Lustre
We consider the MAA models LNT-18 [8] and REC-17 [7] and extend them to model the full MAA algorithm in the synchronous languages Lustre [9] and SCADE [2]. Lustre is a synchronous language based on the dataflow model of computation, which defines a reactive system that receives inputs at each tick of a logical clock and calculates outputs. The relation between inputs and outputs is described using a system of (unordered) equations. At a given cycle, the value of inputs can be memorized to be reused in the next cycles. The outputs at a given instant may thus depend on current and past inputs, but not on future inputs. The relations between inputs and outputs are specified in nodes using constants, operators, functions, auxiliary variables, as well as other nodes, which provide for a compositional description of complex systems. SCADE is an industrial language that merges two different academic languages: Lustre, a declarative dataflow language, and Esterel [3] an imperative, synchronous process calculus; more precisely, SCADE embodies a graphical variant of Esterel known as SyncCharts [1]. Although these languages are quite different, the designers of SCADE managed to integrate both in one coherent language. In the present article, our modelling is based upon the dataflow subset of SCADE, with little or no use of the Esteral/SynchCharts features. Also, following the approach of a previous modelling of the MAA using term rewrite systems ( [7]), we chose not to rely on predefined data types of SCADE (bits, machine words, etc.) but to define all our types from scratch, using the type constructors provided by the language. One advantage of this approach is that it is fully formal, without implicit assumptions about the implementation of machine words or the behaviour of predefined arithmetic operations. This also provides a thorough exercise to assess the correctness and performance of Lustre and SCADE compilers.
A large part of our SCADE/Lustre models contain generic definitions independent of the MAA that could be reused to model other examples. The whole SCADE model of the MAA is presented in both the Appendix A and the MARS repository, while the Lustre model will only appear in the MARS repository, as it is very similar to the SCADE one. As in [7], we choose to represent blocks as words of four bytes, rather than thirty-two bits. Thereby, the logical operations on blocks (AND, OR, XOR, and CYC) are easy to define using bitwise and bytewise manipulations. The bits, bytes and blocks are represented with the three following SCADE data structures: Next, we define a set of functions to implement the corresponding logical operations on bits, bytes, and blocks. The arithmetical operations (ADD, CAR, and MUL) have been implemented using 8-bit, 16-bit, and 32-bit adders and multipliers, more or less inspired from the theory of digital circuits. Thus, the structure Pair shown below, represents the result of the multiplication of two blocks. A message is a list of blocks, each block of the message is an input of the main MAC node in SCADE, as illustrated in Figure 4 (graphically) and in Figure 5 (in code). Note that in the synchronous dataflow SCADE/Lustre, a node describes the relation between its input and output parameters using a system of equations. A node is composed of a set of unordered equations that define each output parameter according to the actual or previous input parameters.
The MAC node takes as input the message to encode, and a key, which corresponds to two words (called K and J). A local variable init defines the beginning of a message, and another variable n stores the number of blocks, in order to ensure the implementation of the "mode of operation" of the MAA, i.e., segmentation of messages larger than 1024 bytes (as explained in Section 2). The MAC provides as outputs the result of the intermediate computations (prelude, mainloop) in the auxiliary blocks (X, Y, V, W, S, T), and the result of its main computation, i.e., the MAC for the given input (one key and a message), which is represented by a variable (Z). At each call of the SCADE node MAC, one new block of the message is processed as follows: • for the 1 st block of the message, the auxiliary variables (X, Y, and V) are computed with an iteration of the mainLoop function with the initial values (X0, Y0, V0) computed by the function prelude shown in Figure 5;  • for the 257 th block of the message, the auxiliary variables are computed with an iteration of the mainLoop2 function, which consists of two iterations of the mainLoop, one on the result of the previous coda (Z), and one on this block message; and, • for the other blocks of the message, the auxiliary variables are computed by taking into account the previous auxiliary variables (pre X, pre Y, and pre V) computed by the previous block. Figure 2 represents the graphical SCADE MAC A node without the implementation of the "mode of operation" (segmentation of the 1024 bytes messages). User defined operators such as functions (prelude, mainLoop, and coda) or nodes are represented by yellow boxes while native SCADE operators are represented in blue boxes. In particular, the two specific flow manipulation operators for nodes (inherited from Lustre) are used in the MAC A node (See Figure 2): • the memory operator pre ("previous") refers to the value of an input or output variable at the previous cycle; • the initialization operator -> ("followed by") initializes a stream.
In order to implement the "mode of operation", we add a graphical node counting the number of blocks (nr) of the segment, represented in Figure 3. The node size contains the graphical choice operator, enabling the design of two branches. The first one resets the number of blocks (nr) for the 257 th block of the message (pre segment), while the second branch increases nr for the other blocks. Note that segment is a constant corresponding to the maximum size of a message segment (256 blocks). The choice operator and the size node are then used to design the two branches of the graphical MAC node implementing the "mode of operation" represented in Figure 2. Note that one of the branches consist of the MAC A node represented in Figure 2. We could use the modular reset feature of SCADE (restart) to reinitialize the MAC node from the outside. It would have simplified the counter definition, and so the model, but since Lustre does not provide this feature, we don't use it for either of the models. Keys could also  be represented using the type Pair, but we prefer introducing the following dedicated structure Key to clearly distinguish between keys and other pairs (e.g., results of the multiplication of two blocks): type Key = struct { K : Block ; J : Block }; We define the "multiplicative" functions used for MAA computations, most of which are presented in [6] or have been later introduced in [16]. The three principal low-level operations are MUL1, MUL2, and MUL2A, with its auxiliary functions. We also define the higher-level functions that implement the MAA algorithm on one segment (maximum 1024-byte), namely prelude, inner loop, coda, as well as the principal function MAC (that computes the 4-byte signature of a message).
It turns out that SCADE/Lustre enables an elegant modeling of the involved data structures, such as enumeration (e.g., the enumeration Bit) and structures (e.g., the type Byte defined as Octet). We briefly discuss below some of our choices for modeling the MAA in SCADE/Lustre. Functions computing several results. There are several such functions in the MAA; let us consider the prelude function which takes two block parameters J and K and returns six block parameters X, Y, V, W, S, and T. By exploiting the fact that SCADE/Lustre functions may return one or several parameters, we can elegantly define the prelude function in SCADE as follows: The definitions of the auxiliary functions preludeJ, preludeK, preludeHJ, and preludeHK are in Appendix M. This function is invoked as follows (as it is done in the MAC node): X , Y , V , W , S , T = prelude (J , K ); Note that in SCADE the underscore symbol (_) is used in place of defining a local variable if the corresponding returned value is not used. In our case, we needed some outputs from the auxiliary functions for the test vectors, but not for the prelude function, which is why we 'assigned them to _' in prelude.
Comparison between SCADE and Lustre implementations: In the semantic context of our MAA formal models the differences between the two languages are negligible. First, SCADE uses comma instead of a semicolon, and defines the type before the equal in the constant/function definitions. Second, using let/tel in a function composed of one statement is not permitted in SCADE, which generally reduces the number of code lines. However, the main difference is on the compilers: the SCADE compiler enabled us to detect some potentially non-initialized variables in the MAC node and variables not used in the prelude function. The Lustre and SCADE models contain 9 types (structures), 442 constants, 100 functions, and 1 nodes each. Our complete Lustre model of the MAA (see the repository) consists of 1908 lines and our complete SCADE model of the MAA (see Appendix A) has 1762 lines and 3 additional graphical nodes.
Comparison between SCADE/Lustre and earlier implementations: Our two synchronous models are executable, in a sense that they can be compiled automatically into some executable program that will be run to generate the expected results. Let us review these two synchronous models with the three earlier executable specifications; REC-17 [7], LOTOS-18 [8], and, LNT-18 [8].
• Rather than importing external fragments of code written in C, as in to implement for instance blocks and arithmetic operations on blocks, REC-17 and Lustre/SCADE models implement the algorithm entirely, they are self-contained and fully-formal. Even if using external fragments would allow a shorter formalization and generation of more efficient code. We prefer to avoid the risks arising when formal and non-formal codes are mixed (e.g., an error was found in the external implementation in C [8]).
• Contrary to REC 17, LNT-18 and LOTOS-18 specifications, the Lustre/SCADE models contains duplicated computations. Effectively, the MAC node is defined as a sequential function; at each instant, the MAC calculates prelude and coda, even if prelude is only needed at the beginning of each message sequence, and the latter is only needed at the end. Such "trick" was necessary, since modelling cryptographical protocol is not the usual application domain of Lustre/SCADE.
• SCADE and LNT-18 models have a more disciplined specification style than the three other executable specifications, because of the numerous static-analysis checks (e.g., unused variables, useless assignments, etc.) performed by their compilers.
• Finally, the SCADE model contains graphical representations, which makes the model readable and easier to use for non-specialists. To the best of our knowledge, this feature is absent in other specification languages.

Testing the MAA Model
To validate our SCADE and Lustre models, we define four sets of test vectors derived from the specification in [6]. The four sets are defined as follows: (T1) implements the 36 checks listed in Tables 1, 2, and 3 of [6]. These test vectors specify, for a few given keys and messages, the expected values of intermediate calculations (e.g., MUL1, MUL2, MUL2A, etc.).
(T2) is based upon Table 4 of [6], checking if the main loop of the MAA (as described on page 10 of [6]) is correctly implemented on six groups of checks (three single-block messages and one three-block message); T2 corresponds to 56 tests.
(T3) is based upon Table 5 of [6], checking if the MAA signature is correctly computed on four groups of checks, with two different keys and two different messages; T3 corresponds to 64 tests.
(T4) checks all intermediary values of the algorithm with a message of 20 blocks containing only zeros directly taken from Table 6 of [6]; T4 corresponds to 45 tests.
We automate the test execution process, for the test vector (T3) presented in [6, Table 6], namely, four groups of checks, with two different keys and two different messages. The test automation process is different for Lustre and SCADE; we explain them in the following section.

Validation of the Lustre model
When automating the test execution process, we use the testing tool Lurette [14] and take advantage of its connection with the Lustre language. Figure 6 gives an overview of Lurette in the context of testing our Figure 6: Overview of the Lurette testing tool MAA model. Lurette takes two inputs: (i) a specification of the environment constraints in Lutin [25] to dynamically constrain the inputs, (ii) an oracle implementing the test decision, in our case the 12 possible pairs (one key K J, and a message of two blocks), and the expected resulting MAC; and some parameters controlling the execution and the coverage of the generated input sequences, e.g., the number of steps (n) in the execution sequence. Lurette interacts with the Lustre implementation of the MAA, logs the generated sequence of inputs and their corresponding outputs in a file, and displays the test decisions. Following [7], we add three supplementary test vectors that operate on messages of 16, 256, and 4100 blocks containing bit patterns not preserved by permutations to detect implementation mistakes arising from byte permutations (e.g., endianness issues) or incorrect segmentation of messages longer than 1024 bytes (i.e., 256 blocks). Originally in [7], it was done by introducing a function acting as a pseudo-random message generator, which is only possible to implement in Lustre with recursive nodes. Thus, we rewrite the node MAC as the recursive Lustre MAC long messages node as below: When defining the recursive node in the code above, we specify the integer depth of recursion in triangular brackets, the depth of the recursion. The MAC long messages has three inputs: the blocks INIT and INCR to generates a message of the given length ( it ), the blocks of which follow an arithmetic progression, and the key KJ.
The Lutin environment constrains the input of the MAA to one out of four messages, each one containing two words. Note that if the input values are not explicitly constrained in the Lutin environment, random numbers will be generated. The environment contains the 12 possible pairs of keys and messages. Although larger and more complex environments could be written, this task is tedious and error-prone, in particular due to the representation of messages and keys by natural numbers. In our example, correct tests consist of a correct MAC value, given one key and a message. A small excerpt of oracle for our Lustre model is given by the following Lustre code, containing the test decisions and the expected output: the auxiliary block values of X, Y and MAC value for each message block given in the first columnn of [6, Table 6].
node oracle ( id : int ; init : bool ; X , Y , Z : Block ; n : int ) returns ( res : bool ); let res = true -> (( id = 1 and init and X = x48B204D6 and Y = x5834A585 ) or ( id = 2 and init and X = x6AEBACF8 and Y = x9DB15CF6 ) or ... and CHECK () = true and ch ec k_ lo ng _me ss ag e () = true ); tel ; The whole Lutin scenario and Lustre oracle for testing the Lustre model with the test vector (T3) will appear in the MARS Workshop repository.
The Lustre and the test scenarios for the sets of test vectors (T1), (T2), (T3), (T4) has 1908 lines and contains 9 types (structures), 442 constants, 100 functions, and 4 nodes. Our Lustre model of the MAA was successfully validated by the 203 tests.

Validation of the SCADE model
We automate the test execution process, by using the SCADE test environment toolset. To achieve this goal, one has to write a test scenario in an SSS file, with the description of the test sequences for testing the main MAC node. The scenario sets the input values and defines the expected output values to be checked. For instance, for our SCADE MAA model, expected output values consist of the correct MAC value (Z) or the three intermediate values (X, Y, and V), given one key and a message as inputs. A small excerpt of the test scenario is given by the following SCADE code, containing the input sequences: a key, a message block and a boolean indicating if it is the first block of the message. The expected outputs are the auxiliary block values of X, Y and MAC value for each block of message given in [6,Table 6]: The SCADE scenario files (.sss) contain the following instructions: • SSM::set: assign a specific value to an input for the next execution cycle; • SSM::check: register a test of an output against a specified value; • SSM::uncheck: unregister the active test for an observable output; • SSM::cycle: set the number of execution cycles in a test sequence (the default number of cycles is set to 1 when no argument is specified); • #: comment the line.
Note that tests are registered by the next calls to SSM::cycle instruction. The whole scenario for testing our SCADE model with the test vector (T3) will appear in the MARS Workshop repository. The test vector with long messages (i.e., containing more than two blocks) and the test vectors for the auxiliary functions are hard coded in functions, as for instance, the twenty-words message in the Appendix Q.
The SCADE model and the test scenarios for the sets of test vectors (T1), (T2), (T3), (T4), which is 201 tests in total, have 1894 lines and contain 9 types (structures), 442 constants, 99 functions, and 2 nodes. Our SCADE model of the MAA was successfully validated by these 201 tests.

Conclusion and Future Work
In this paper we have presented a formal SCADE model of the Message Authenticator Algorithm (MAA). First, we gave an overview of this cryptographic functions for computing a Message Authentication Code, then we discussed the choices and the challenges of this implementation in SCADE and compared it to the Lustre implementation. Finally we validated our model using the test test vectors derived from the specification in [6] The modelling of the MAA and its validation enabled us to find three errors in the Lustre v6 toolbox: (i) lv6 compiler generates invalid C code if a variable identifier uses quotes ('); (ii) another issue with constant structures and the compiler lv6; and (iii) Lurette tool ignoring -2c-exec option; all these errors have been communicated to the Lustre v6 developers and have been quickly fixed by the team. The modelling of the SCADE model enabled us to improve the Lustre model, more precisely by detecting potentially non-initialized variables and unused variables.
Since neither SCADE, nor Lustre implements the list data type, we had to consider only messages with fixed size in our SCADE model. However, in our Lustre model, we could generate pseudo-random messages by adding a recursive node. It is however fair to warn the reader that testing our Lustre/SCADE MAA models was a tedious task, i.e., we had to manually define more than 400 constants.
In this paper we only have written the main node computing the MAC with the graphical language SCADE. As future work, the full MAA algorithm or at least its main functions could be designed with the graphical language SCADE and some test scenarios could also be simulated on the graphical nodes. To improve the code efficiency, one could as well implement blocks and arithmetic operations on blocks in external fragments of code written in C, and import them in the Lustre/SCADE models.

A Formal Model of the MAA in SCADE
This annex presents the specification of the MAA in the SCADE language. This specification is fully self-contained, meaning that it does not depend on any externally-defined library -with the minor disadvantage of somewhat lengthy definitions for byte and blocks constants. For readability, the specification has been split into 16 parts, each part being devoted to a particular type, a group of functions sharing a common purpose, or a collection of test vectors. The first parts contain general definitions that are largely independent from the MAA; starting from Section K, the definitions become increasingly more MAA-specific. All machine words (bytes, blocks, etc.) are represented according to the "big endian" convention, i.e., the first argument of each corresponding constructor denote the most significant bit.

B Definitions for type Bit
We define bits using an enumeration Bit (X0 and X1), together with functions implementing logical operations on bits.

C Definitions for Type Byte
We define bytes (octets) using a structure Octet that contains the eight bits of a byte, together with functions implementing bitwise logical operations, left-shift and right-shift operations on bytes, as well as all byte constants needed to formally describe the MAA and its test vectors.

D Definitions for Type OctetSum
We define type OctetSum that stores the result of the addition of two octets. Values of this type are 9-bit words, made up using the structure OctetSum that gathers one bit for the carry and an octet for the sum. The two principal functions for this type are addOctetSum (which adds two octets and an input carry bit, and returns both an output carry bit and an 8-bit sum), and addOctet (which is derived from the former one by dropping the input and output carry bits); the other functions are auxiliary functions implementing an 8-bit adder. x = orBit ( andBit ( andBit ( x1 , x2 ) , notBit ( x3 )) , andBit ( orBit ( x1 , x2 ) , x3 ));

F Definitions for Type HalfSum
We define type HalfSum that stores the result of the addition of two half words. Values of this type are 17-bit words, made up using the constructor buildHalfSum that gathers one bit for the carry and a half word for the sum. The five principal non-constructors for this type are eqHalfSum (which tests equality), addHalfSum (which adds two half words and returns both a carry bit and a 16-bit sum), addHalf (which is derived from the former one by dropping the carry bit), addHalfOctet and addHalfOctets (which are similar to the former one but take byte arguments that are converted to half words before summation); the other non-constructors are auxiliary functions implementing a 16-bit adder built using two 8-bit adders.

H Definitions for Type BlockSum
We define type BlockSum that stores the result of the addition of two blocks. Values of this type are 33-bit words, made up using the constructor buildBlockSum that gathers one bit for the carry and a block for the sum. The five principal non-constructors for this type are eqBlockSum (which tests equality), addBlockSum (which adds two blocks and returns both a carry bit and a 32-bit sum), addBlock (which is derived from the former one by dropping the carry bit), addBlockHalf and addBlockHalves (which are similar to the former one but take half-word arguments that are converted to blocks before summation); the other non-constructors are auxiliary functions implementing a 32-bit adder built using four 8-bit adders.

J Definitions for Type Key
We define a type Key that is intended to represent the 64-bit keys (J, K) used by the MAA. This type has a constructor buildKey that takes two blocks and returns a key. In [16], keys are represented using the type Pair, but we prefer introducing a dedicated type to clearly distinguish between keys and, e.g., results of the multiplication of two blocks.

M Definitions (3) of MAA-specific Cryptographic Functions
We define a third set of auxilary functions used for MAA computations, and the higher-level functions that implement the MAA algorithm, namely the prelude, the inner loop, and the coda; the two principal functions are MAA (which computes the signature of a nonsegmented message) and MAC (which splits a message into 1024-byte segments and computes the overall signature of this message by iterating on each segment, the 4-byte signature of each segment being prepended to the bytes of the next segment).

N Test Vectors (1) for Checking MAA Computations
We define a first set of test vectors for the MAA. The following expressions implement the checks listed in Tables 1, 2, and 3 of [6] and should all evaluate to true if the MAA functions are correctly implemented.

O Test Vectors (2) for Checking MAA Computations
We define a second set of test vectors for the MAA, based upon Table 4 of [6]. The following expressions implement six groups of checks (three single-block messages and one three-block message). They should all evaluate to true if the main loop of MAA (as described page 10 of [6]) is correctly implemented. ; −− f a k e "A" c o n s t a n t B = x00000001 ; −− f a k e "B" c o n s t a n t C = xFFFFFFFB ; −− f a k e "C" c o n s t a n t D = xFFFFFFFB ; −− f a k e "D" c o n s t a n t V = x00000001 ; W = x00000001 ; −− t r u e "A" c o n s t a n t B = x00804021 ; −− t r u e "B" c o n s t a n t C = xBFEF7FDF ; −− t r u e "C" c o n s t a n t D = x7DFEFBFF ; −− t r u e "D" c o n s t a n t X0 = x21D869BA ; Y0 = x7792F9D4 ; We complete the above tests with additional test vectors taken from [12,Annex E.3.3], which only gives detailed values for the first block of the 84-block test message. −− t r u e "B" c o n s t a n t C = xBFEF7FDF ; −− t r u e "C" c o n s t a n t D = x7DFEFBFF ; −− t r u e "D" c o n s t a n t X0 = x21D869BA ; Y0 = x7792F9D4 ; V0 = xC4EB1AEB ; W = xF6A09667 ; M = x0A202020 ;

P Test vectors (3) for Checking MAA Computations
We define a third set of test vectors for the MAA, based upon Table 5 of [6]. The following expressions implement four groups of checks, with two different keys and two different messages. They should all evaluate to true if the MAA signature is correctly computed.

Q Test Vectors (4) for Checking MAA Computations
We define a last set of test vectors for the MAA. The first one (a message of 20 blocks containing only zeros) was directly taken from Table 6 of [6].