C. André, Computing SyncCharts Reactions. Electron. Notes Theor. Comput. Sci, vol.88, pp.3-19, 2004.

G. Berry, SCADE: Synchronous design and validation of embedded control software. In: Next Generation Design and Verification Methodologies for Distributed Embedded Control Systems, pp.19-33, 2007.

G. Berry and &. Gonthier, The Esterel Synchronous Programming Language: Design, Semantics, Implementation. Sci. Comput. Program, vol.19, pp.87-152, 1992.
URL : https://hal.archives-ouvertes.fr/inria-00075711

J. Colaço, B. Pagano-&-marc, and . Pouzet, SCADE 6: A formal language for embedded critical software development, Proceedings of the 11th International Symposium on Theoretical Aspects of Software Engineering (TASE'17), pp.1-11, 2017.

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), vol.196, pp.393-400, 1985.

W. Donald, O. Davies-&-david, and . Clayden, The Message Authenticator Algorithm (MAA) and its Implementation, 1988.

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), vol.244, pp.129-183, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01511859

H. Garavel and &. Marsso, Comparative Study of Eight Formal Specifications of the Message Authenticator Algorithm, Proceedings of the 3nd Workshop on Models for Formal Analysis of Real Systems (MARS'18), vol.268, pp.41-87, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01775332

N. Halbwachs, P. Caspi, and P. Raymond-&-daniel-pilaud, The synchronous dataflow programming language LUSTRE, Proceedings of the IEEE, vol.79, issue.9, pp.1305-1320, 1991.

, International Standard 8730, International Organization for Standardization -Banking, ISO, 1986.

, Approved Algorithms for Message Authentication -Part 1: Data Encryption Algorithm (DEA), ISO, 1987.

, International Standard 8730, International Organization for Standardization -Banking, ISO, 1990.

, Approved Algorithms for Message Authentication -Part 2: Message Authenticator Algorithm. International Standard 8731-2, International Organization for Standardization -Banking, ISO, 1992.

E. Jahier and P. Raymond-&-philippe-baufreton, Case studies with Lurette V2, International Journal on Software Tools for Technology Transfer, vol.8, issue.6, pp.517-530, 2006.
URL : https://hal.archives-ouvertes.fr/hal-00389838

M. K. Lai, A Formal Interpretation of the MAA Standard in Z, 1991.

A. Menezes, P. C. Van-oorschot, &. Scott, and A. Vanstone, Handbook of Applied Cryptography, 1996.

H. B. Munster, Comments on the LOTOS Standard. NPL Technical Memorandum DITC 52/91, 1991.

H. B. Munster, LOTOS Specification of the MAA Standard, with an Evaluation of LOTOS, 1991.

G. I. Parkin and &. O'neill, Specification of the MAA Standard in VDM, 1990.

G. I. Parkin and &. O'neill, Specification of the MAA Standard in VDM, the 4th International Symposium of VDM Europe (VDM'91), vol.1, pp.526-544, 1991.

B. Preneel, Encyclopedia of Cryptography and Security, pp.741-742, 2011.

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 of Cryptographic Techniques (EUROCRYPT'96), vol.1070, pp.19-32, 1996.

B. Preneel, &. Paul, and C. Van-oorschot, On the Security of Iterated Message Authentication Codes, IEEE Transactions on Information Theory, vol.45, issue.1, pp.188-199, 1999.

B. Preneel, V. Rumen, &. Paul, and C. Van-oorschot, Security Analysis of the Message Authenticator Algorithm (MAA), European Transactions on Telecommunications, vol.8, issue.5, pp.455-470, 1997.

P. Raymond, Y. Roux-&-erwan, and . Jahier, Lutin: a language for specifying and executing reactive scenarios, EURASIP Journal on Embedded Systems, 2008.

, Key Recovery and Collision Clusters for MAA, Proceedings of the 1st International Conference on Security in Communication Networks (SCN'96), 1996.

Y. Xppp,

. Z-=-xorblock,

, ) = x00 ) and ( X0 = x34ACF886 ) and ( Y0 = x7397C9AE ) and ( V0 = x7201F4DC ) and ( W = x2829040B ) and ( S = x9E2E7B36 ) and ( T = x13647149 ) and ( X = x2FD76FFB ) and ( Y = x550D91CE ) and ( Xp = xA70FC148 ) and ( Yp = x1D10D8D3 ) and ( Xpp = xB1CC1CC5 ) and ( Ypp = x29C1485F ) and ( Xppp = x288FC786 ) and ( Yppp = x9115A558 ) and

J. Var, K. X0, X. Xp, . Xpp, . Xppp et al.,

V. V0, . Vp, W. Vpp, S. , T. et al.,

. K-=-x5a35d667,

. M1-=-xffffffff,

. M2-=-x00000000,

Y. X0, W. V0, and S. ,

X. , Y. V0, and W. ,

Y. Xp, Vp = mainLoop

. ??-coda,

Y. Xpp, =. Vpp, . Xp, . Yp, W. Vp et al.,

Y. Xppp,

. Z-=-xorblock,

C. H-e-c-k-_-p-r-e-l-u-d-e-_-a-;-var, J. , K. , X. , Y. et al., ], which gives prelude results computed for another key, ) = x00 ) and ( X0 = x34ACF886 ) and ( Y0 = x7397C9AE ) and ( V0 = x7201F4DC ) and ( W = x2829040B ) and ( S = x9E2E7B36 ) and ( T = x13647149 ) and ( X = x8DC8BBDE ) and ( Y = xFE4E5BDD ) and ( Xp = xCBC865BA ) and ( Yp = x0297AF6F ) and ( Xpp = x3CF3A7D2 ) and ( Ypp = x160EE9B5 ) and ( Xppp = xD0482465 ) and ( Yppp = x7050EC5E ) and ( Z = xA018C83B

. K-=-x9d15c437,

X. , Y. , V. , W. , and S. ,

. ??-res, = x21D869BA ) and ( Y = x7792F9D4 ) and ( V = xC4EB1AEB ) and ( W = xF6A09667 ) and ( S = x6D67E884 ) and ( T = xA511987A )

Y. X13, W. V12, and B. ). ,

?. Y14, W. V13, and B. ). ,

?. Y15, W. V14, and B. ). ,

?. Y16, W. V15, and B. ). ,

?. Y17, W. V16, and B. ). ,

?. Y18, W. V17, and B. ). ,

?. Y19, W. V18, and B. ). ,

. ??-coda,

Y. X20, W. V19, and S. ). ,

. ??-coda,

Y. X21, W. V20, and T. ). ,

. ??-tp, = x303FF4AA ) and ( Y = x1277A6D4 ) and ( X1 = x55DD063F ) and ( Y1 = x4C49AAE0 ) and ( X2 = x51AF3C1D ) and ( Y2 = x5BC02502 ) and ( X3 = xA44AAAC0 ) and ( Y3 = x63C70DBA ) and ( X4 = x4D53901A ) and ( Y4 = x2E80AC30 ) and ( X5 = x5F38EEF1 ) and ( Y5 = x2A6091AE ) and ( X6 = xF0239DD5 ) and ( Y6 = x3DD81AC6 ) and ( X7 = xEB35B97F ) and ( Y7 = x9372CDC6 ) and ( X8 = x4DA124A1 ) and ( Y8 = xC6B1317E ) and ( X9 = x7F839576 ) and ( Y9 = x74B39176 ) and ( X10 = x11A9D254 ) and ( Y10 = xD78634BC ) and ( X11 = xD8804CA5 ) and ( Y11 = xFDC1A8BA ) and ( X12 = x3F6F7248 ) and ( Y12 = x11AC46B8 ) and ( X13 = xACBC13DD ) and ( Y13 = x33D5A466 ) and ( X14 = x4CE933E1 ) and ( Y14 = xC21A1846 ) and ( X15 = xC1ED90DD ) and ( Y15 = xCD959B46 ) and ( X16 = x3CD54DEB ) and ( Y16 = x613F8E2A ) and ( X17 = xBBA57835 ) and ( Y17 = x07C72EAA ) and ( X18 = xD7843FDC ) and ( Y18 = x6AD6E8A4 ) and ( X19 = x5EBA06C2 ) and ( Y19 = x91896CFA ) and ( X20 = x1D9C9655 ) and

W. V19, S. , and T. )-=-xdb79fbdc,