Message Authenticator Algorithm

Description:rewrite system that formally models 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
Paper(s): A Large Term Rewrite System Modelling a Pioneering Cryptographic Algorithm
Comparative Study of Eight Formal Specifications of the Message Authenticator Algorithm

Abstract

We present a term rewrite system that formally models the Message Authenticator Algorithm (MAA), which was one of the first cryptographic functions for computing a Message Authentication Code and was adopted, between 1987 and 2001, in international standards (ISO 8730 and ISO 8731-2) to ensure the authenticity and integrity of banking transactions. Our term rewrite system is large (13 sorts, 18 constructors, 644 non-constructors, and 684 rewrite rules), confluent, and terminating. Implementations in thirteen different languages have been automatically derived from this model and used to validate 200 official test vectors for the MAA.

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)
Creative Commons License    This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License.