A Large Term Rewrite System Modelling a Pioneering Cryptographic Algorithm - Archive ouverte HAL Access content directly
Conference Papers Year : 2017

A Large Term Rewrite System Modelling a Pioneering Cryptographic Algorithm

(1) , (1)
1
Hubert Garavel
Lina Marsso
  • Function : Author
  • PersonId : 1006713

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.
Fichier principal
Vignette du fichier
Garavel-Marsso-17.pdf (234.15 Ko) Télécharger le fichier
Origin : Publisher files allowed on an open archive
Loading...

Dates and versions

hal-01511859 , version 1 (21-04-2017)

Identifiers

Cite

Hubert Garavel, Lina Marsso. A Large Term Rewrite System Modelling a Pioneering Cryptographic Algorithm. 2nd Workshop on Models for Formal Analysis of Real Systems, Apr 2017, Uppsala, Sweden. pp.129 - 183, ⟨10.4204/EPTCS.244.6⟩. ⟨hal-01511859⟩
245 View
200 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More