Specifying a Cryptographical Protocol in Lustre and SCADE

Lina Marsso

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.

In Ansgar Fehnker and Hubert Garavel: Proceedings of the 4th Workshop on Models for Formal Analysis of Real Systems (MARS 2020), Dublin, Ireland, April 26, 2020, Electronic Proceedings in Theoretical Computer Science 316, pp. 149–199.
Published: 26th April 2020.

ArXived at: https://dx.doi.org/10.4204/EPTCS.316.7 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org