D. W. Davies, A Message Authenticator Algorithm Suitable for a Mainframe Computer, Advances in Cryptology ? Proceedings of the Workshop on the Theory and Application of Cryptographic Techniques (CRYPTO'84), pp.393-400, 1985.
DOI : 10.1007/3-540-39568-7_30

W. Donald, &. Davies, O. David, and . Clayden, A Message Authenticator Algorithm Suitable for a Mainframe Computer, NPL Report DITC, vol.1783, 1983.

W. Donald, &. Davies, O. David, and . Clayden, The Message Authenticator Algorithm (MAA) and its Implementation, NPL Report DITC, vol.10988, 1988.

F. Durán, M. Roldán, J. Bach, E. Balland, M. Van-den-brand et al., The Third Rewrite Engines Competition, Proceedings of the 8th International Workshop on Rewriting Logic and Its Applications (WRLA'10), pp.243-26110, 2010.
DOI : 10.1007/3-540-45127-7_27

F. Durán, M. Roldán, E. Balland, M. Van-den-brand, S. Eker et al., The Second Rewrite Engines Competition, Electronic Notes in Theoretical Computer Science, vol.238, issue.3, pp.281-291, 2009.
DOI : 10.1016/j.entcs.2009.05.025

H. Ehrig and &. Mahr, Fundamentals of Algebraic Specification 1 ? Equations and Initial Semantics, EATCS Monographs on Theoretical Computer Science, vol.6, pp.10-1007, 1985.

H. Garavel, Compilation of LOTOS Abstract Data Types, Proceedings of the 2nd International Conference on Formal Description Techniques FORTE'89, pp.147-162, 1989.

H. Garavel, Revisiting sequential composition in process calculi, Journal of Logical and Algebraic Methods in Programming, vol.84, issue.6, pp.742-762, 2015.
DOI : 10.1016/j.jlamp.2015.08.001
URL : https://hal.archives-ouvertes.fr/hal-01247770

H. Garavel and F. Lang, CADP 2011: a toolbox for the construction and analysis of distributed processes, inria.fr/publications/Garavel-Lang-Mateescu-Serwe-13.html, pp.89-107, 2013.
DOI : 10.1007/s100090050009
URL : https://hal.archives-ouvertes.fr/hal-00715056

H. Garavel, F. Lang-&-wendelin, and . Serwe, From LOTOS to LNT, Lecture Notes in Computer Science, vol.118, issue.1, pp.3-2610, 2017.
DOI : 10.1016/j.scico.2016.01.002
URL : https://hal.archives-ouvertes.fr/hal-01621670

H. Garavel and &. Marsso, A Large Term Rewrite System Modelling a Pioneering Cryptographic Algorithm, Proceedings of the 2nd Workshop on Models for Formal Analysis of Real Systems (MARS'17) Electronic Proceedings in Theoretical Computer Science 244, pp.129-183, 2017.
DOI : 10.1002/ett.4460080504
URL : https://hal.archives-ouvertes.fr/hal-01511859

H. Garavel and &. Turlier, ADT : un compilateur pour les types abstraits algébriques du langage LOTOS, Actes du Colloque Francophone pour l'Ingénierie des Protocoles (CFIP'93), pp.325-339, 1993.

I. Iec, LOTOS ? A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour, International Organization for Standardization ? Information Processing Systems ? Open Systems Interconnection, 1989.

M. K. Lai, A Formal Interpretation of the MAA Standard in Z, NPL Report DITC, vol.18491, 1991.

R. P. Lampard, An Implementation of MAA from a VDM Specification, 1991.

J. De-meer, R. Roth, and &. Vuong, Introduction to algebraic specifications based on the language ACT ONE, Computer Networks and ISDN Systems, vol.23, issue.5, pp.363-39210, 1992.
DOI : 10.1016/0169-7552(92)90013-G

A. Menezes, P. C. Van-oorschot, &. Scott, and A. Vanstone, Handbook of Applied Cryptography, 1996.
DOI : 10.1201/9781439821916

B. Harold and . Munster, LOTOS Specification of the MAA Standard, with an Evaluation of LOTOS, NPL Report DITC, vol.19191, 1991.

G. I. Parkin and &. Neill, Specification of the MAA standard in VDM, NPL Report DITC, vol.16090, 1990.
DOI : 10.1007/3-540-54834-3_31

G. I. Parkin and &. Neill, Specification of the MAA standard in VDM, Formal Software Development ? Proceedings 4th International Symposium of VDM Europe (VDM'91), pp.526-54410, 1991.
DOI : 10.1007/3-540-54834-3_31

B. Preneel, Cryptanalysis of message authentication codes, Proceedings of the 1st International Workshop on Information Security Tatsunokuchi, Japan, Lecture Notes in Computer Science 1396, pp.55-65, 1997.
DOI : 10.1007/BFb0030408

B. Preneel, &. Paul, and C. Van-oorschot, MDx-MAC and Building Fast MACs from Hash Functions, Advances in Cryptology ? Proceedings of 15th Annual International Cryptology Conference (CRYPTO'95), pp.1-14, 1995.
DOI : 10.1007/3-540-44750-4_1
URL : http://www.cosic.esat.kuleuven.be/publications/article-53.pdf

B. Preneel, &. Paul, and C. Van-oorschot, On the Security of Two MAC Algorithms, Advances in Cryptology ? Proceedings of the International Conference on the Theory and Application Bit1, pp.6-7, 1996.
DOI : 10.1007/3-540-68339-9_3

. Octet, Bit3 (x) and Bit3, Bit2 (x) and Bit2 (y) Bit4 (x) and Bit4 (y), Bit5 (x) and Bit5 (y), Bit6 (x) and Bit6 (y), Bit7 (x) and Bit7 (y), pp.8-8

. Octet, Bit3 (x) or Bit3, Bit2 (x) or Bit2 (y) Bit4 (x) or Bit4 (y), Bit5 (x) or Bit5 (y), Bit6 (x) or Bit6 (y), Bit7 (x) or Bit7 (y), pp.8-8

=. Xor-y and . Octet, Bit3 (x) xor Bit3, Bit2 (x) xor Bit2 (y) Bit4 (x) xor Bit4 (y), Bit5 (x) xor Bit5 (y), Bit6 (x) xor Bit6 (y), pp.7-7

H. Block and O. Prelude, Block, Block -> ThreePairs AuxPrelude : Pair, Octet -> ThreePairs eqns ofsort Block forall P, pp.0-00

*. ?????????????????????????????????????????????????????-*-)-type, . Maa, and . Prelude, * ! implementedby N255 external * ) : -> Nat MAC ( * ! implementedby MAC * ) : Block, Block, Message -> Block MAAstart : ThreePairs, Message -> Block MAA : Message, pp.2-2

V. , W. , B. , X. ==, !. ?. et al., assert X == xD8804CA5; assert Y == xFDC1A8BA); assert X == x3F6F7248; assert Y == x11AC46B8; ?? 14th MainLoop iteration MainLoop assert X == xACBC13DD; assert Y == x33D5A466; ?? 15th MainLoop iteration MainLoop assert X == x4CE933E1; assert Y == xC21A1846); assert X == xC1ED90DD; assert Y == xCD959B46; ?? 17th MainLoop iteration MainLoop assert X == x3CD54DEB; assert Y == x613F8E2A); assert X == xBBA57835; assert Y == x07C72EAA; ?? 19th MainLoop iteration MainLoop); assert X == xD7843FDC; assert Y == x6AD6E8A4, ?? 11th MainLoop iteration MainLoop assert X == x5EBA06C2; assert Y == x91896CFA; ?? Coda: MainLoop iteration with S MainLoop S); assert X == x1D9C9655; assert Y == x98D1CC75; ?? Coda: MainLoop iteration with T MainLoop