-- CADP (CONSTRUCTION AND ANALYSIS OF DISTRIBUTED PROCESSES)
-- http://cadp.inria.fr

[Last updated: Thu Oct  6 11:19:49 CEST 2022]

This directory contains an example for LNT.OPEN and CAESAR.ADT. It is based
upon formal descriptions, both in LNT and LOTOS, of the Message Authentication
Algorithm (MAA), a cryptographic algorithm intended to secure banking
transactions.

When given a file and a key (a character string with up to 8 characters),
the MAA algorithm computes a digital signature for the file, using one-way
hashing functions. The signature is called Message Authentication Code (MAC).

The LOTOS description used was taken and adapted from:

   Harold B. Munster, "LOTOS Specification of the MAA Standard, with an 
   Evaluation of LOTOS", NPL Report DITC 191/91, National Physical Laboratory
   (Teddington, Middlesex, UK), September 1991.

It was adapted to CADP in 1995 by Hubert Garavel, and entirely rewritten
to LNT in 2016 by Wendelin Serwe and Hubert Garavel. The LOTOS and LNT
descriptions were then deeply revised by Hubert Garavel and Lina Marsso,
who fixed issues, made simplifications, and added unit tests. An account
of these efforts can be found in [Garavel-Marsso-18] (see below).

The MAA is described using the following files:

   BLOCK.lnt                 LNT definitions for the Block type
   BLOCKVALUES.lnt           LNT definitions for the Block constants
   maa.lnt                   LNT specification of the MAA
   maa.fnt                   C code to implement certain LNT types/functions
   main.c                    driver program to run the MAA
   Makefile                  makefile to compile the LNT version of the MAA
   LOTOS/maa_original.lotos  original LOTOS specification by H. Munster
   LOTOS/maa.lotos           LOTOS specification adapted to CADP
   LOTOS/maa.t               C code to implement certain LOTOS types
   LOTOS/maa.f               C code to implement certain LOTOS functions
   LOTOS/main.c              driver program to run the MAA
   LOTOS/Makefile            makefile to compile the LOTOS version of the MAA
   Tests/*                   MAA test files given in ISO standards
   doc/Davies-Clayden-88.pdf   Informal MAA specification
   doc/Garavel-Marsso-17.pdf   Formal MAA specification (term rewrite system)
   doc/Garavel-Marsso-18.pdf   Formal MAA specification (LNT and LOTOS)

Typing the command 

$	make

will invoke the LNT.OPEN tool to translate the LNT specification to LOTOS.
Then, CAESAR.ADT will be invoked to translate the abstract data types defined
in the generated LOTOS specification into equivalent C types and functions. 
CAESAR.ADT generates a ".h" file which can be mixed with handwritten C code.
In particular, file main.c contains a user-written C program which serves as
a "driver" program to execute the implementation in C of the MAA generated
by CAESAR.ADT. The "make" command will compile everything and produce an
executable program named "maa", and will run this program to compute the MAC
of some file (namely, the original LOTOS description). 

More generally, the "maa" program can be used to compute the MAC of a given
file with a given key.  The command-line syntax is:
	maa [-m] <file> <key>
where option "-m" prints the contents of the file in hexadecimal form.

Typing the command

$	(cd LOTOS; make)

will produce "maa" using the LOTOS specification rather than the LNT one.

Note: In order to save memory, the Reverse function (which allocates most of
the memory that is not freed later) has been written directly in C by Wendelin
Serwe (see files "maa.fnt" and "LOTOS/maa.f"). This leads to a significant
reduction of memory usage. For instance, when applying the "maa" program 
(generated from the LOTOS specification) to the "maa.lotos" file itself, the
memory leaks passes from 13 Mbytes (when the C code for the Reverse function
is generated by CAESAR.ADT) down to 670 kbytes (when the Reverse function is
implemented manually).

Note: When using "maa" to compute the checksum of large files (i.e., larger
than 100 kbytes), a segmentation fault may occur due to stack overflow.