|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools Forum |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
A Large Term Rewrite System Modelling a Pioneering Cryptographic Algorithm
Hubert Garavel and Lina Marsso
Proceedings of the 2nd Workshop on Models for Formal Analysis of Real Systems (MARS 2017), Uppsala, Sweden, April 2017
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.
| 55 pages |  |
 PostScript |
| Slides of H. Garavel's lecture at the MARS'17 workshop | |
(slides prepared together with L. Marsso) |
ERRATUM [May 2, 2017]
There is a minor error in a comment line of Annex B.20: the last line of page 178 should read:
% key (J = x00FF00FF, K = x00000000), message (M1 = xAAAAAAAA, M2 = x55555555)rather than:
% key (J = x00FF00FF, K = x00000000), message (M1 = x55555555, M2 = xAAAAAAAA)