, Computing SyncCharts Reactions. Electron. Notes Theor. Comput. Sci, vol.88, pp.3-19, 2004.
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. ,
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
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. ,
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. ,
The Message Authenticator Algorithm (MAA) and its Implementation, 1988. ,
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
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
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.
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
A Formal Interpretation of the MAA Standard in Z, 1991. ,
, Handbook of Applied Cryptography, 1996.
, Comments on the LOTOS Standard. NPL Technical Memorandum DITC 52/91, 1991.
LOTOS Specification of the MAA Standard, with an Evaluation of LOTOS, 1991. ,
Specification of the MAA Standard in VDM, 1990. ,
Specification of the MAA Standard in VDM, the 4th International Symposium of VDM Europe (VDM'91), vol.1, pp.526-544, 1991. ,
, Encyclopedia of Cryptography and Security, pp.741-742, 2011.
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. ,
On the Security of Iterated Message Authentication Codes, IEEE Transactions on Information Theory, vol.45, issue.1, pp.188-199, 1999. ,
Security Analysis of the Message Authenticator Algorithm (MAA), European Transactions on Telecommunications, vol.8, issue.5, pp.455-470, 1997. ,
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.
,
,
, ) = 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
,
,
,
,
,
,
,
, Vp = mainLoop
,
,
,
,
], 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 ,
,
,
= x21D869BA ) and ( Y = x7792F9D4 ) and ( V = xC4EB1AEB ) and ( W = xF6A09667 ) and ( S = x6D67E884 ) and ( T = xA511987A ) ,
,
,
,
,
,
,
,
,
,
,
,
, = 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
,