A Large Term Rewrite System Modelling a Pioneering Cryptographic Algorithm

Hubert Garavel 1 Lina Marsso 1
1 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
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.
Type de document :
Communication dans un congrès
2nd Workshop on Models for Formal Analysis of Real Systems, Apr 2017, Uppsala, Sweden. 244, pp.129 - 183, 2017, 〈http://mars-workshop.org/mars2017/〉. 〈10.4204/EPTCS.244.6〉
Liste complète des métadonnées

Littérature citée [34 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01511859
Contributeur : Hubert Garavel <>
Soumis le : vendredi 21 avril 2017 - 16:45:46
Dernière modification le : jeudi 11 janvier 2018 - 06:23:43
Document(s) archivé(s) le : samedi 22 juillet 2017 - 13:55:42

Fichier

Garavel-Marsso-17.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

Collections

Citation

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. 244, pp.129 - 183, 2017, 〈http://mars-workshop.org/mars2017/〉. 〈10.4204/EPTCS.244.6〉. 〈hal-01511859〉

Partager

Métriques

Consultations de la notice

254

Téléchargements de fichiers

53