Hubert Garavel

Hubert Garavel

Contact Details

Hubert Garavel

Pubs By Year

Pub Categories

Computer Science - Software Engineering (1)
Computer Science - Logic in Computer Science (1)
Computer Science - Cryptography and Security (1)
Computer Science - Distributed; Parallel; and Cluster Computing (1)
Computer Science - Programming Languages (1)

Publications Authored By Hubert Garavel

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. Read More

The multiway rendezvous introduced in Theoretical CSP is a powerful paradigm to achieve synchronization and communication among a group of (possibly more than two) processes. We illustrate the advantages of this paradigm on the production cell benchmark, a model of a real metal processing plant, for which we propose a compositional software controller, which is written in LNT and LOTOS, and makes intensive use of the multiway rendezvous. Read More