Message Authenticator Algorithm

Description:models of the Message Authenticator Algorithm (MAA), which was one of the first cryptographic functions for computing a Message Authentication Code and was adopted ISO 8730 and ISO 8731-2
Author(s):Hubert Garavel, Lina Marsso
Event(s): MARS'17, MARS'18, MARS'20
Paper(s): A Large Term Rewrite System Modelling a Pioneering Cryptographic Algorithm
Comparative Study of Eight Formal Specifications of the Message Authenticator Algorithm
Specifying a cryptographical protocol in Lustre and SCADE

Abstract

The Message Authenticator Algorithm (MAA) is a pioneering algorithm in computer security, namely, one of the first cryptographic functions for computing a Message Authentication Code. Between 1987 and 2001, the MAA, as defined in the international standards ISO 8730 and ISO 8731-2, ensured the authenticity and integrity of banking transactions. The MAA also plays a role in the history of formal methods for it served as a common benchmark for the comparative assessment of specification languages. In 1990 and 1991, three formal models of the MAA (in VDM, Z, and LOTOS) were developed at NPL. This work has been pursued at INRIA Grenoble through a series of three MARS articles published in 2017, 2018, and 2020.
In the article Large Term Rewrite System Modelling a Pioneering Cryptographic Algorithm the MAA is manually specified as a (large, confluent, terminating) term rewrite system, from which implementations in thirteen different languages are automatically derived.
In Comparative Study of Eight Formal Specifications of the Message Authenticator Algorithm, various specifications of the MAA in the LOTOS and LNT languages are presented, and compared to six prior specifications with respect to conciseness, readability, and efficiency of code generation.
Two new models of the MAA are presented in Specifying a cryptographical protocol in Lustre and SCADE. The models are given in the synchronous dataflow languages Lustre and SCADE, and are manually derived from the aforementioned term rewrite system. The correctness of the formal models for the MAA is assessed on the 200 official test vectors found in the MAA standards; the work reveals mistakes in the annexes of the standards ISO 8730 and ISO 8731-2, as well as bugs in a few compilers for formal specification languages.

Model(s)

    1. Download Model
    2. Browse Model
    3. tool(s): REC tool
      1. Download Model
      2. Browse Model
      3. tool(s): AProVE tool
      1. Download Model
      2. Browse Model
      3. tool(s): Clean
      1. Download Model
      2. Browse Model
      3. tool(s): Haskell
      1. Download Model
      2. Browse Model
      3. tool(s): LNT (CADP)
      1. Download Model
      2. Browse Model
      3. tool(s): LOTOS (CADP)
      1. Download Model
      2. Browse Model
      3. tool(s): Maude
      1. Download Model
      2. Browse Model
      3. tool(s): mCRL2
      1. Download Model
      2. Browse Model
      3. tool(s): OCaml
      1. Download Model
      2. Browse Model
      3. tool(s): Opal
      1. Download Model
      2. Browse Model
      3. tool(s): Rascal
      1. Download Model
      2. Browse Model
      3. tool(s): Scala
      1. Download Model
      2. Browse Model
      3. tool(s): Standard ML
      1. Download Model
      2. Browse Model
      3. tool(s): Stratego/XT
      1. Download Model
      2. Browse Model
      3. tool(s): Tom
    1. Download Model
    2. Browse Model
    3. tool(s): LOTOS (CADP)
    1. Download Model
    2. Browse Model
    3. tool(s): LNT (CADP)
    1. Download Model
    2. Browse Model
    3. tool(s): Lustre
    1. Download Model
    2. Browse Model
    3. tool(s): Scade
Creative Commons License    This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License.