Message Authenticator Algorithm - Revision history

GreenC bot: Move 1 url. Wayback Medic 2.5 per WP:URLREQ#citeftp

2025-05-27T09:25:46Z

Move 1 url. Wayback Medic 2.5 per WP:URLREQ#citeftp

← Previous revision		Revision as of 09:25, 27 May 2025
Line 39:		Line 39:
	{{cite report\|author=M. K. F. Lai \|year=1991 \|title=A Formal Interpretation of the MAA Standard in Z \|type=NPL Report DITC 184/91 \|institution=National Physical Laboratory \|location=Teddington, Middlesex, UK}}		{{cite report\|author=M. K. F. Lai \|year=1991 \|title=A Formal Interpretation of the MAA Standard in Z \|type=NPL Report DITC 184/91 \|institution=National Physical Laboratory \|location=Teddington, Middlesex, UK}}
	</ref> one in [[Language Of Temporal Ordering Specification\|LOTOS]],<ref>		</ref> one in [[Language Of Temporal Ordering Specification\|LOTOS]],<ref>
	{{cite report\|author=Harold B. Munster \|year=1991 \|title=LOTOS Specification of the MAA Standard, with an Evaluation of LOTOS \|type=NPL Report DITC 191/91 \|institution=National Physical Laboratory \|location=Teddington, Middlesex, UK \|url=ftp://ftp.inrialpes.fr/pub/vasy/publications/others/Munster-91-a.pdf}}		{{cite report\|author=Harold B. Munster \|year=1991 \|title=LOTOS Specification of the MAA Standard, with an Evaluation of LOTOS \|type=NPL Report DITC 191/91 \|institution=National Physical Laboratory \|location=Teddington, Middlesex, UK \|archive-url=https://web.archive.org/web/20170706122244/ftp://ftp.inrialpes.fr/pub/vasy/publications/others/Munster-91-a.pdf \|archive-date=2017-07-06 \|url-status=dead \|url=ftp://ftp.inrialpes.fr/pub/vasy/publications/others/Munster-91-a.pdf}}
	</ref> and one in [[Vienna Development Method\|VDM]].<ref>		</ref> and one in [[Vienna Development Method\|VDM]].<ref>
	{{cite report\|author1=Graeme I. Parkin \|author2=G. O’Neill \|year=1990 \|title=Specification of the MAA Standard in VDM \|type=NPL Report DITC 160/90 \|institution=National Physical Laboratory, Teddington, Middlesex, UK}}</ref><ref>		{{cite report\|author1=Graeme I. Parkin \|author2=G. O’Neill \|year=1990 \|title=Specification of the MAA Standard in VDM \|type=NPL Report DITC 160/90 \|institution=National Physical Laboratory, Teddington, Middlesex, UK}}</ref><ref>

Whizz40: section

2023-10-21T14:00:22Z

section

← Previous revision		Revision as of 14:00, 21 October 2023
Line 1:		Line 1:
	The '''Message Authenticator Algorithm''' ('''MAA''') was one of the first [[Cryptography\|cryptographic]] functions for computing a [[message authentication code]] (MAC). It was designed in 1983 by [[Donald Davies]] and David Clayden at the [[National Physical Laboratory (United Kingdom)]] in response to a request of the UK Bankers Automated Clearing Services. The MAA was one of the first Message Authentication Code algorithms to gain widespread acceptance.		The '''Message Authenticator Algorithm''' ('''MAA''') was one of the first [[Cryptography\|cryptographic]] functions for computing a [[message authentication code]] (MAC).

			== History ==
			It was designed in 1983 by [[Donald Davies]] and David Clayden at the [[National Physical Laboratory (United Kingdom)]] in response to a request of the UK Bankers Automated Clearing Services. The MAA was one of the first Message Authentication Code algorithms to gain widespread acceptance.

	== Development and standardization ==		== Development and standardization ==

Citation bot: Alter: template type, title. Add: isbn, pages, doi, chapter, chapter-url, authors 1-1. Removed or converted URL. Formatted dashes. Upgrade ISBN10 to 13. | Use this bot. Report bugs. | Suggested by Abductive | #UCB_webform 1189/3849

2022-08-08T22:29:29Z

Alter: template type, title. Add: isbn, pages, doi, chapter, chapter-url, authors 1-1. Removed or converted URL. Formatted dashes. Upgrade ISBN10 to 13. | Use this bot. Report bugs. | Suggested by Abductive | #UCB_webform 1189/3849

← Previous revision		Revision as of 22:29, 8 August 2022
Line 24:		Line 24:
	{{cite journal\|first1=Bart \|last1=Preneel \|first2= Paul C.\|last2=van Oorschot \|year=1999 \|title=On the Security of Iterated Message Authentication Codes \|journal=IEEE Transactions on Information Theory \|volume=45 \|number=1 \|pages=188–199 \|doi=10.1109/18.746787}}		{{cite journal\|first1=Bart \|last1=Preneel \|first2= Paul C.\|last2=van Oorschot \|year=1999 \|title=On the Security of Iterated Message Authentication Codes \|journal=IEEE Transactions on Information Theory \|volume=45 \|number=1 \|pages=188–199 \|doi=10.1109/18.746787}}
	</ref><ref>		</ref><ref>
	{{cite ~~document~~\|first1=Bart \|last1=Preneel \|first2=Vincent \|last2=Rumen \|first3= Paul C.\|last3=van Oorschot \|year=1997 \|title=Security Analysis of the Message Authenticator Algorithm (MAA) -journal=European Transactions on Telecommunications \|volume=8 \|number=5 \|pages=455–470 \|doi=10.1002/ett.4460080504}}		{{cite journal\|first1=Bart \|last1=Preneel \|first2=Vincent \|last2=Rumen \|first3= Paul C.\|last3=van Oorschot \|year=1997 \|title=Security Analysis of the Message Authenticator Algorithm (MAA) -journal=European Transactions on Telecommunications \|volume=8 \|number=5 \|pages=455–470 \|doi=10.1002/ett.4460080504}}
	</ref><ref>		</ref><ref>
	{{cite conference\|first1=Vincent \|last1=Rijmen \|first2=Bart \|last2=Preneel \|first3=Erik \|last3=De Win \|year=1996 \|title=Key Recovery and Collision Clusters for MAA \|conference=Proceedings of the 1st International Conference on Security in Communication Networks (SCN’96) \|url=https://www.cosic.esat.kuleuven.be/publications/article-437.pdf}}		{{cite conference\|first1=Vincent \|last1=Rijmen \|first2=Bart \|last2=Preneel \|first3=Erik \|last3=De Win \|year=1996 \|title=Key Recovery and Collision Clusters for MAA \|conference=Proceedings of the 1st International Conference on Security in Communication Networks (SCN’96) \|url=https://www.cosic.esat.kuleuven.be/publications/article-437.pdf}}
	</ref> For this reason, MAA was withdrawn from ISO standards in 2002 but continued to be used as a prominent case study for assessing various [[formal methods]].<ref>{{cite ~~web~~\|url=https://link.springer.com/referenceworkentry/10.1007%2F978-1-4419-5906-5_591\|~~title~~=MAA\|publisher=Encyclopedia of Cryptography and Security\|year=2011\|access-date=3 May 2021}}</ref>		</ref> For this reason, MAA was withdrawn from ISO standards in 2002 but continued to be used as a prominent case study for assessing various [[formal methods]].<ref>{{cite book\|chapter-url=https://link.springer.com/referenceworkentry/10.1007%2F978-1-4419-5906-5_591\|chapter=MAA\|publisher=Encyclopedia of Cryptography and Security\|year=2011\|doi=10.1007/978-1-4419-5906-5_591 \|access-date=3 May 2021\|title=Encyclopedia of Cryptography and Security \|last1=Preneel \|first1=Bart \|pages=741–742 \|isbn=978-1-4419-5905-8 }}</ref>

	== Formal specifications of the MAA ==		== Formal specifications of the MAA ==

Dormskirk: /* Attacks */ expand based on text at National Physical Laboratory (United Kingdom)

2021-05-03T10:04:37Z

Attacks: expand based on text at National Physical Laboratory (United Kingdom)

← Previous revision		Revision as of 10:04, 3 May 2021
Line 27:		Line 27:
	</ref><ref>		</ref><ref>
	{{cite conference\|first1=Vincent \|last1=Rijmen \|first2=Bart \|last2=Preneel \|first3=Erik \|last3=De Win \|year=1996 \|title=Key Recovery and Collision Clusters for MAA \|conference=Proceedings of the 1st International Conference on Security in Communication Networks (SCN’96) \|url=https://www.cosic.esat.kuleuven.be/publications/article-437.pdf}}		{{cite conference\|first1=Vincent \|last1=Rijmen \|first2=Bart \|last2=Preneel \|first3=Erik \|last3=De Win \|year=1996 \|title=Key Recovery and Collision Clusters for MAA \|conference=Proceedings of the 1st International Conference on Security in Communication Networks (SCN’96) \|url=https://www.cosic.esat.kuleuven.be/publications/article-437.pdf}}
			</ref> For this reason, MAA was withdrawn from ISO standards in 2002 but continued to be used as a prominent case study for assessing various [[formal methods]].<ref>{{cite web\|url=https://link.springer.com/referenceworkentry/10.1007%2F978-1-4419-5906-5_591\|title=MAA\|publisher=Encyclopedia of Cryptography and Security\|year=2011\|access-date=3 May 2021}}</ref>
	</ref> For this reason, MAA was withdrawn from ISO standards in 2002.

	== Formal specifications of the MAA ==		== Formal specifications of the MAA ==

Dormskirk: /* Formal specifications of the MAA */ tidy referencing

2021-05-03T10:02:33Z

Formal specifications of the MAA: tidy referencing

← Previous revision		Revision as of 10:02, 3 May 2021
Line 40:		Line 40:
	{{cite report\|author1=Graeme I. Parkin \|author2=G. O’Neill \|year=1990 \|title=Specification of the MAA Standard in VDM \|type=NPL Report DITC 160/90 \|institution=National Physical Laboratory, Teddington, Middlesex, UK}}</ref><ref>		{{cite report\|author1=Graeme I. Parkin \|author2=G. O’Neill \|year=1990 \|title=Specification of the MAA Standard in VDM \|type=NPL Report DITC 160/90 \|institution=National Physical Laboratory, Teddington, Middlesex, UK}}</ref><ref>
	{{cite conference\|author1=Graeme I. Parkin \|author2=G. O’Neill \|year=1991 \|title=Specification of the MAA Standard in VDM \|editor1=Søren Prehn \|editor2=W. J. Toetenel \|conference=Formal Software Development – Proceedings (Volume 1) of the 4th International Symposium of VDM Europe (VDM’91), Noordwijkerhout, The Netherlands \|series=Lecture Notes in Computer Science \|volume=551 \|publisher=Springer \|pages=526–544 \|doi=10.1007/3-540-54834-3_31}}		{{cite conference\|author1=Graeme I. Parkin \|author2=G. O’Neill \|year=1991 \|title=Specification of the MAA Standard in VDM \|editor1=Søren Prehn \|editor2=W. J. Toetenel \|conference=Formal Software Development – Proceedings (Volume 1) of the 4th International Symposium of VDM Europe (VDM’91), Noordwijkerhout, The Netherlands \|series=Lecture Notes in Computer Science \|volume=551 \|publisher=Springer \|pages=526–544 \|doi=10.1007/3-540-54834-3_31}}
	</ref> The VDM specification became part of the 1992 revision of the International Standard 8731-2, and three implementations were manually derived from that latter specification: [[C (programming language)\|C]], [[Miranda (programming language)\|Miranda]], and [[Modula-2]]<ref>		</ref> The VDM specification became part of the 1992 revision of the International Standard 8731-2, and three implementations were manually derived from that latter specification: [[C (programming language)\|C]], [[Miranda (programming language)\|Miranda]], and [[Modula-2]].<ref>{{cite report\|author=R. P. Lampard \|year=1991 \|title=An Implementation of MAA from a VDM Specification \|type=NPL Technical Memorandum DITC 50/91 \|institution=National Physical Laboratory \|location=Teddington, Middlesex, UK}}</ref>
	{{cite report\|author=R. P. Lampard \|year=1991 \|title=An Implementation of MAA from a VDM Specification \|type=NPL Technical Memorandum DITC 50/91 \|institution=National Physical Laboratory \|location=Teddington, Middlesex, UK}}
	</ref> .

	Other formal models of the MAA have been developed. In 2017, a complete formal specification of the MAA as a large [[Rewriting\|term rewriting system]] was published;<ref>		Other formal models of the MAA have been developed. In 2017, a complete formal specification of the MAA as a large [[Rewriting\|term rewriting system]] was published;<ref>

Dormskirk: /* Formal specifications of the MAA */ adjust word order to place reference at the end

2021-05-03T10:02:03Z

Formal specifications of the MAA: adjust word order to place reference at the end

← Previous revision		Revision as of 10:02, 3 May 2021
Line 40:		Line 40:
	{{cite report\|author1=Graeme I. Parkin \|author2=G. O’Neill \|year=1990 \|title=Specification of the MAA Standard in VDM \|type=NPL Report DITC 160/90 \|institution=National Physical Laboratory, Teddington, Middlesex, UK}}</ref><ref>		{{cite report\|author1=Graeme I. Parkin \|author2=G. O’Neill \|year=1990 \|title=Specification of the MAA Standard in VDM \|type=NPL Report DITC 160/90 \|institution=National Physical Laboratory, Teddington, Middlesex, UK}}</ref><ref>
	{{cite conference\|author1=Graeme I. Parkin \|author2=G. O’Neill \|year=1991 \|title=Specification of the MAA Standard in VDM \|editor1=Søren Prehn \|editor2=W. J. Toetenel \|conference=Formal Software Development – Proceedings (Volume 1) of the 4th International Symposium of VDM Europe (VDM’91), Noordwijkerhout, The Netherlands \|series=Lecture Notes in Computer Science \|volume=551 \|publisher=Springer \|pages=526–544 \|doi=10.1007/3-540-54834-3_31}}		{{cite conference\|author1=Graeme I. Parkin \|author2=G. O’Neill \|year=1991 \|title=Specification of the MAA Standard in VDM \|editor1=Søren Prehn \|editor2=W. J. Toetenel \|conference=Formal Software Development – Proceedings (Volume 1) of the 4th International Symposium of VDM Europe (VDM’91), Noordwijkerhout, The Netherlands \|series=Lecture Notes in Computer Science \|volume=551 \|publisher=Springer \|pages=526–544 \|doi=10.1007/3-540-54834-3_31}}
	</ref> The VDM specification became part of the 1992 revision of the International Standard 8731-2, and three implementations in [[C (programming language)\|C]], [[Miranda (programming language)\|Miranda]], and [[Modula-2]]<ref>		</ref> The VDM specification became part of the 1992 revision of the International Standard 8731-2, and three implementations were manually derived from that latter specification: [[C (programming language)\|C]], [[Miranda (programming language)\|Miranda]], and [[Modula-2]]<ref>
	{{cite report\|author=R. P. Lampard \|year=1991 \|title=An Implementation of MAA from a VDM Specification \|type=NPL Technical Memorandum DITC 50/91 \|institution=National Physical Laboratory \|location=Teddington, Middlesex, UK}}		{{cite report\|author=R. P. Lampard \|year=1991 \|title=An Implementation of MAA from a VDM Specification \|type=NPL Technical Memorandum DITC 50/91 \|institution=National Physical Laboratory \|location=Teddington, Middlesex, UK}}
			</ref> .
	</ref> were manually derived from that latter specification.

	Other formal models of the MAA have been developed. In 2017, a complete formal specification of the MAA as a large [[Rewriting\|term rewriting system]] was published;<ref>		Other formal models of the MAA have been developed. In 2017, a complete formal specification of the MAA as a large [[Rewriting\|term rewriting system]] was published;<ref>

Whizz40: /* Bibliography */ c/e

2021-05-03T09:25:54Z

Bibliography: c/e

← Previous revision		Revision as of 09:25, 3 May 2021
Line 50:		Line 50:
	</ref>		</ref>

	== ~~Bibliography~~ ==		== References ==
	{{reflist}}		{{reflist}}

Whizz40: c/e

2021-05-03T09:25:23Z

c/e

← Previous revision		Revision as of 09:25, 3 May 2021
Line 1:		Line 1:
	The '''Message Authenticator Algorithm''' ('''MAA''') was one of the first [[Cryptography\|cryptographic]] functions for computing a [[~~Message~~ ~~Authentication~~ ~~Code~~]]. It was designed in 1983 by [[Donald Davies]] and David Clayden at the [[National Physical Laboratory (United Kingdom)]] in response to a request of the UK Bankers Automated Clearing Services. The MAA was one of the first Message Authentication Code algorithms to gain widespread acceptance.		The '''Message Authenticator Algorithm''' ('''MAA''') was one of the first [[Cryptography\|cryptographic]] functions for computing a [[message authentication code]] (MAC). It was designed in 1983 by [[Donald Davies]] and David Clayden at the [[National Physical Laboratory (United Kingdom)]] in response to a request of the UK Bankers Automated Clearing Services. The MAA was one of the first Message Authentication Code algorithms to gain widespread acceptance.

	== Development and standardization ==		== Development and standardization ==

Whizz40: /* Formal specifications of the MAA */ c/e

2021-05-03T09:20:51Z

Formal specifications of the MAA: c/e

← Previous revision		Revision as of 09:20, 3 May 2021
Line 33:		Line 33:
	The MAA has been used as a prominent case study for assessing various [[formal methods]].		The MAA has been used as a prominent case study for assessing various [[formal methods]].

	In the early ~~90s~~, the [[National Physical Laboratory (United Kingdom)\|NPL]] developed three formal specifications of the MAA: one in [[Z notation\|Z]],<ref>		In the early 1990s, the [[National Physical Laboratory (United Kingdom)\|NPL]] developed three formal specifications of the MAA: one in [[Z notation\|Z]],<ref>
	{{cite report\|author=M. K. F. Lai \|year=1991 \|title=A Formal Interpretation of the MAA Standard in Z \|type=NPL Report DITC 184/91 \|institution=National Physical Laboratory \|location=Teddington, Middlesex, UK}}		{{cite report\|author=M. K. F. Lai \|year=1991 \|title=A Formal Interpretation of the MAA Standard in Z \|type=NPL Report DITC 184/91 \|institution=National Physical Laboratory \|location=Teddington, Middlesex, UK}}
	</ref> one in [[Language Of Temporal Ordering Specification\|LOTOS]],<ref>		</ref> one in [[Language Of Temporal Ordering Specification\|LOTOS]],<ref>
Line 46:		Line 46:
	Other formal models of the MAA have been developed. In 2017, a complete formal specification of the MAA as a large [[Rewriting\|term rewriting system]] was published;<ref>		Other formal models of the MAA have been developed. In 2017, a complete formal specification of the MAA as a large [[Rewriting\|term rewriting system]] was published;<ref>
	{{cite conference\|first1=Hubert \|last1=Garavel \|first2=Lina \|last2=Marsso \|title=A Large Term Rewrite System Modelling a Pioneering Cryptographic Algorithm \|conference=Proceedings of the 2nd Workshop on Models for Formal Analysis of Real Systems (MARS'17), Uppsala, Sweden \|year=2017 \|series=Electronic Proceedings in Theoretical Computer Science \|volume=244 \| pages=129–183\|url=http://cadp.inria.fr/publications/Garavel-Marsso-17.html \|doi=10.4204/EPTCS.244.6\|arxiv=1703.06573 }}		{{cite conference\|first1=Hubert \|last1=Garavel \|first2=Lina \|last2=Marsso \|title=A Large Term Rewrite System Modelling a Pioneering Cryptographic Algorithm \|conference=Proceedings of the 2nd Workshop on Models for Formal Analysis of Real Systems (MARS'17), Uppsala, Sweden \|year=2017 \|series=Electronic Proceedings in Theoretical Computer Science \|volume=244 \| pages=129–183\|url=http://cadp.inria.fr/publications/Garavel-Marsso-17.html \|doi=10.4204/EPTCS.244.6\|arxiv=1703.06573 }}
	</ref> From this specification, [http://www.mars-workshop.org/repository/012-MAA.html implementations of the MAA in fifteen different languages] have been generated automatically.		</ref> From this specification, [http://www.mars-workshop.org/repository/012-MAA.html implementations of the MAA in fifteen different languages] have been generated automatically. In 2018, two new formal specifications of the MAA, in [[Language Of Temporal Ordering Specification\|LOTOS]] and LNT, have been published.<ref>
	In 2018, two new formal specifications of the MAA, in [[Language Of Temporal Ordering Specification\|LOTOS]] and LNT, have been published. <ref>
	{{cite conference\|first1=Hubert \|last1=Garavel \|first2=Lina \|last2=Marsso \|title=Comparative Study of Eight Formal Specifications of the Message Authenticator Algorithm \|conference=Proceedings of the 3nd Workshop on Models for Formal Analysis of Real Systems (MARS'18) and 6th International Workshop on Verification and Program Transformation (MARS/VPT 2018), Thessaloniki, Greece \|year=2018 \|series=Electronic Proceedings in Theoretical Computer Science \|volume=268 \|pages=41–87\|url=http://cadp.inria.fr/publications/Garavel-Marsso-18.html \|doi=10.4204/EPTCS.268.2\|arxiv=1803.10322 }}		{{cite conference\|first1=Hubert \|last1=Garavel \|first2=Lina \|last2=Marsso \|title=Comparative Study of Eight Formal Specifications of the Message Authenticator Algorithm \|conference=Proceedings of the 3nd Workshop on Models for Formal Analysis of Real Systems (MARS'18) and 6th International Workshop on Verification and Program Transformation (MARS/VPT 2018), Thessaloniki, Greece \|year=2018 \|series=Electronic Proceedings in Theoretical Computer Science \|volume=268 \|pages=41–87\|url=http://cadp.inria.fr/publications/Garavel-Marsso-18.html \|doi=10.4204/EPTCS.268.2\|arxiv=1803.10322 }}
	</ref>		</ref>

Monkbot: Task 18 (cosmetic): eval 17 templates: hyphenate params (1×);

2021-01-14T02:34:43Z

Task 18 (cosmetic): eval 17 templates: hyphenate params (1×);

← Previous revision		Revision as of 02:34, 14 January 2021
Line 4:		Line 4:

	The original specification<ref>		The original specification<ref>
	{{cite conference\|last=Davies \|first=Donald W. \|year=1985 \|title=A Message Authenticator Algorithm Suitable for a Mainframe Computer \|~~booktitle~~=Advances in Cryptology – Proceedings of the Workshop on the Theory and Application of Cryptographic Techniques (CRYPTO’84), Santa Barbara, CA, USA \|series=Lecture Notes in Computer Science \|volume=196 \|publisher=Springer \|pages=393–400 \|doi=10.1007/3-540-39568-7_30\|doi-access=free }}		{{cite conference\|last=Davies \|first=Donald W. \|year=1985 \|title=A Message Authenticator Algorithm Suitable for a Mainframe Computer \|book-title=Advances in Cryptology – Proceedings of the Workshop on the Theory and Application of Cryptographic Techniques (CRYPTO’84), Santa Barbara, CA, USA \|series=Lecture Notes in Computer Science \|volume=196 \|publisher=Springer \|pages=393–400 \|doi=10.1007/3-540-39568-7_30\|doi-access=free }}
	</ref><ref>		</ref><ref>
	{{cite report\|first1=Donald W. \|last1=Davies \|first2= David O. \|last2=Clayden \|year=1988 \|title=The Message Authenticator Algorithm (MAA) and its Implementation \|type=NPL Report DITC 109/88 \|institution=National Physical Laboratory \|location=Teddington, Middlesex, UK \|url=http://www.cix.co.uk/~klockstone/maa.pdf}}		{{cite report\|first1=Donald W. \|last1=Davies \|first2= David O. \|last2=Clayden \|year=1988 \|title=The Message Authenticator Algorithm (MAA) and its Implementation \|type=NPL Report DITC 109/88 \|institution=National Physical Laboratory \|location=Teddington, Middlesex, UK \|url=http://www.cix.co.uk/~klockstone/maa.pdf}}

← Previous revision		Revision as of 09:25, 27 May 2025
Line 39:		Line 39:
	{{cite report\|author=M. K. F. Lai \|year=1991 \|title=A Formal Interpretation of the MAA Standard in Z \|type=NPL Report DITC 184/91 \|institution=National Physical Laboratory \|location=Teddington, Middlesex, UK}}		{{cite report\|author=M. K. F. Lai \|year=1991 \|title=A Formal Interpretation of the MAA Standard in Z \|type=NPL Report DITC 184/91 \|institution=National Physical Laboratory \|location=Teddington, Middlesex, UK}}
	</ref> one in [[Language Of Temporal Ordering Specification\|LOTOS]],<ref>		</ref> one in [[Language Of Temporal Ordering Specification\|LOTOS]],<ref>
	{{cite report\|author=Harold B. Munster \|year=1991 \|title=LOTOS Specification of the MAA Standard, with an Evaluation of LOTOS \|type=NPL Report DITC 191/91 \|institution=National Physical Laboratory \|location=Teddington, Middlesex, UK \|url=ftp://ftp.inrialpes.fr/pub/vasy/publications/others/Munster-91-a.pdf}}		{{cite report\|author=Harold B. Munster \|year=1991 \|title=LOTOS Specification of the MAA Standard, with an Evaluation of LOTOS \|type=NPL Report DITC 191/91 \|institution=National Physical Laboratory \|location=Teddington, Middlesex, UK \|archive-url=https://web.archive.org/web/20170706122244/ftp://ftp.inrialpes.fr/pub/vasy/publications/others/Munster-91-a.pdf \|archive-date=2017-07-06 \|url-status=dead \|url=ftp://ftp.inrialpes.fr/pub/vasy/publications/others/Munster-91-a.pdf}}
	</ref> and one in [[Vienna Development Method\|VDM]].<ref>		</ref> and one in [[Vienna Development Method\|VDM]].<ref>
	{{cite report\|author1=Graeme I. Parkin \|author2=G. O’Neill \|year=1990 \|title=Specification of the MAA Standard in VDM \|type=NPL Report DITC 160/90 \|institution=National Physical Laboratory, Teddington, Middlesex, UK}}</ref><ref>		{{cite report\|author1=Graeme I. Parkin \|author2=G. O’Neill \|year=1990 \|title=Specification of the MAA Standard in VDM \|type=NPL Report DITC 160/90 \|institution=National Physical Laboratory, Teddington, Middlesex, UK}}</ref><ref>

← Previous revision		Revision as of 10:02, 3 May 2021
Line 40:		Line 40:
	{{cite report\|author1=Graeme I. Parkin \|author2=G. O’Neill \|year=1990 \|title=Specification of the MAA Standard in VDM \|type=NPL Report DITC 160/90 \|institution=National Physical Laboratory, Teddington, Middlesex, UK}}</ref><ref>		{{cite report\|author1=Graeme I. Parkin \|author2=G. O’Neill \|year=1990 \|title=Specification of the MAA Standard in VDM \|type=NPL Report DITC 160/90 \|institution=National Physical Laboratory, Teddington, Middlesex, UK}}</ref><ref>
	{{cite conference\|author1=Graeme I. Parkin \|author2=G. O’Neill \|year=1991 \|title=Specification of the MAA Standard in VDM \|editor1=Søren Prehn \|editor2=W. J. Toetenel \|conference=Formal Software Development – Proceedings (Volume 1) of the 4th International Symposium of VDM Europe (VDM’91), Noordwijkerhout, The Netherlands \|series=Lecture Notes in Computer Science \|volume=551 \|publisher=Springer \|pages=526–544 \|doi=10.1007/3-540-54834-3_31}}		{{cite conference\|author1=Graeme I. Parkin \|author2=G. O’Neill \|year=1991 \|title=Specification of the MAA Standard in VDM \|editor1=Søren Prehn \|editor2=W. J. Toetenel \|conference=Formal Software Development – Proceedings (Volume 1) of the 4th International Symposium of VDM Europe (VDM’91), Noordwijkerhout, The Netherlands \|series=Lecture Notes in Computer Science \|volume=551 \|publisher=Springer \|pages=526–544 \|doi=10.1007/3-540-54834-3_31}}
	</ref> The VDM specification became part of the 1992 revision of the International Standard 8731-2, and three implementations were manually derived from that latter specification: [[C (programming language)\|C]], [[Miranda (programming language)\|Miranda]], and [[Modula-2]]<ref>		</ref> The VDM specification became part of the 1992 revision of the International Standard 8731-2, and three implementations were manually derived from that latter specification: [[C (programming language)\|C]], [[Miranda (programming language)\|Miranda]], and [[Modula-2]].<ref>{{cite report\|author=R. P. Lampard \|year=1991 \|title=An Implementation of MAA from a VDM Specification \|type=NPL Technical Memorandum DITC 50/91 \|institution=National Physical Laboratory \|location=Teddington, Middlesex, UK}}</ref>
	{{cite report\|author=R. P. Lampard \|year=1991 \|title=An Implementation of MAA from a VDM Specification \|type=NPL Technical Memorandum DITC 50/91 \|institution=National Physical Laboratory \|location=Teddington, Middlesex, UK}}
	</ref> .

	Other formal models of the MAA have been developed. In 2017, a complete formal specification of the MAA as a large [[Rewriting\|term rewriting system]] was published;<ref>		Other formal models of the MAA have been developed. In 2017, a complete formal specification of the MAA as a large [[Rewriting\|term rewriting system]] was published;<ref>

← Previous revision		Revision as of 10:02, 3 May 2021
Line 40:		Line 40:
	{{cite report\|author1=Graeme I. Parkin \|author2=G. O’Neill \|year=1990 \|title=Specification of the MAA Standard in VDM \|type=NPL Report DITC 160/90 \|institution=National Physical Laboratory, Teddington, Middlesex, UK}}</ref><ref>		{{cite report\|author1=Graeme I. Parkin \|author2=G. O’Neill \|year=1990 \|title=Specification of the MAA Standard in VDM \|type=NPL Report DITC 160/90 \|institution=National Physical Laboratory, Teddington, Middlesex, UK}}</ref><ref>
	{{cite conference\|author1=Graeme I. Parkin \|author2=G. O’Neill \|year=1991 \|title=Specification of the MAA Standard in VDM \|editor1=Søren Prehn \|editor2=W. J. Toetenel \|conference=Formal Software Development – Proceedings (Volume 1) of the 4th International Symposium of VDM Europe (VDM’91), Noordwijkerhout, The Netherlands \|series=Lecture Notes in Computer Science \|volume=551 \|publisher=Springer \|pages=526–544 \|doi=10.1007/3-540-54834-3_31}}		{{cite conference\|author1=Graeme I. Parkin \|author2=G. O’Neill \|year=1991 \|title=Specification of the MAA Standard in VDM \|editor1=Søren Prehn \|editor2=W. J. Toetenel \|conference=Formal Software Development – Proceedings (Volume 1) of the 4th International Symposium of VDM Europe (VDM’91), Noordwijkerhout, The Netherlands \|series=Lecture Notes in Computer Science \|volume=551 \|publisher=Springer \|pages=526–544 \|doi=10.1007/3-540-54834-3_31}}
	</ref> The VDM specification became part of the 1992 revision of the International Standard 8731-2, and three implementations in [[C (programming language)\|C]], [[Miranda (programming language)\|Miranda]], and [[Modula-2]]<ref>		</ref> The VDM specification became part of the 1992 revision of the International Standard 8731-2, and three implementations were manually derived from that latter specification: [[C (programming language)\|C]], [[Miranda (programming language)\|Miranda]], and [[Modula-2]]<ref>
	{{cite report\|author=R. P. Lampard \|year=1991 \|title=An Implementation of MAA from a VDM Specification \|type=NPL Technical Memorandum DITC 50/91 \|institution=National Physical Laboratory \|location=Teddington, Middlesex, UK}}		{{cite report\|author=R. P. Lampard \|year=1991 \|title=An Implementation of MAA from a VDM Specification \|type=NPL Technical Memorandum DITC 50/91 \|institution=National Physical Laboratory \|location=Teddington, Middlesex, UK}}
			</ref> .
	</ref> were manually derived from that latter specification.

	Other formal models of the MAA have been developed. In 2017, a complete formal specification of the MAA as a large [[Rewriting\|term rewriting system]] was published;<ref>		Other formal models of the MAA have been developed. In 2017, a complete formal specification of the MAA as a large [[Rewriting\|term rewriting system]] was published;<ref>

← Previous revision		Revision as of 09:20, 3 May 2021
Line 33:		Line 33:
	The MAA has been used as a prominent case study for assessing various [[formal methods]].		The MAA has been used as a prominent case study for assessing various [[formal methods]].

	In the early ~~90s~~, the [[National Physical Laboratory (United Kingdom)\|NPL]] developed three formal specifications of the MAA: one in [[Z notation\|Z]],<ref>		In the early 1990s, the [[National Physical Laboratory (United Kingdom)\|NPL]] developed three formal specifications of the MAA: one in [[Z notation\|Z]],<ref>
	{{cite report\|author=M. K. F. Lai \|year=1991 \|title=A Formal Interpretation of the MAA Standard in Z \|type=NPL Report DITC 184/91 \|institution=National Physical Laboratory \|location=Teddington, Middlesex, UK}}		{{cite report\|author=M. K. F. Lai \|year=1991 \|title=A Formal Interpretation of the MAA Standard in Z \|type=NPL Report DITC 184/91 \|institution=National Physical Laboratory \|location=Teddington, Middlesex, UK}}
	</ref> one in [[Language Of Temporal Ordering Specification\|LOTOS]],<ref>		</ref> one in [[Language Of Temporal Ordering Specification\|LOTOS]],<ref>
Line 46:		Line 46:
	Other formal models of the MAA have been developed. In 2017, a complete formal specification of the MAA as a large [[Rewriting\|term rewriting system]] was published;<ref>		Other formal models of the MAA have been developed. In 2017, a complete formal specification of the MAA as a large [[Rewriting\|term rewriting system]] was published;<ref>
	{{cite conference\|first1=Hubert \|last1=Garavel \|first2=Lina \|last2=Marsso \|title=A Large Term Rewrite System Modelling a Pioneering Cryptographic Algorithm \|conference=Proceedings of the 2nd Workshop on Models for Formal Analysis of Real Systems (MARS'17), Uppsala, Sweden \|year=2017 \|series=Electronic Proceedings in Theoretical Computer Science \|volume=244 \| pages=129–183\|url=http://cadp.inria.fr/publications/Garavel-Marsso-17.html \|doi=10.4204/EPTCS.244.6\|arxiv=1703.06573 }}		{{cite conference\|first1=Hubert \|last1=Garavel \|first2=Lina \|last2=Marsso \|title=A Large Term Rewrite System Modelling a Pioneering Cryptographic Algorithm \|conference=Proceedings of the 2nd Workshop on Models for Formal Analysis of Real Systems (MARS'17), Uppsala, Sweden \|year=2017 \|series=Electronic Proceedings in Theoretical Computer Science \|volume=244 \| pages=129–183\|url=http://cadp.inria.fr/publications/Garavel-Marsso-17.html \|doi=10.4204/EPTCS.244.6\|arxiv=1703.06573 }}
	</ref> From this specification, [http://www.mars-workshop.org/repository/012-MAA.html implementations of the MAA in fifteen different languages] have been generated automatically.		</ref> From this specification, [http://www.mars-workshop.org/repository/012-MAA.html implementations of the MAA in fifteen different languages] have been generated automatically. In 2018, two new formal specifications of the MAA, in [[Language Of Temporal Ordering Specification\|LOTOS]] and LNT, have been published.<ref>
	In 2018, two new formal specifications of the MAA, in [[Language Of Temporal Ordering Specification\|LOTOS]] and LNT, have been published. <ref>
	{{cite conference\|first1=Hubert \|last1=Garavel \|first2=Lina \|last2=Marsso \|title=Comparative Study of Eight Formal Specifications of the Message Authenticator Algorithm \|conference=Proceedings of the 3nd Workshop on Models for Formal Analysis of Real Systems (MARS'18) and 6th International Workshop on Verification and Program Transformation (MARS/VPT 2018), Thessaloniki, Greece \|year=2018 \|series=Electronic Proceedings in Theoretical Computer Science \|volume=268 \|pages=41–87\|url=http://cadp.inria.fr/publications/Garavel-Marsso-18.html \|doi=10.4204/EPTCS.268.2\|arxiv=1803.10322 }}		{{cite conference\|first1=Hubert \|last1=Garavel \|first2=Lina \|last2=Marsso \|title=Comparative Study of Eight Formal Specifications of the Message Authenticator Algorithm \|conference=Proceedings of the 3nd Workshop on Models for Formal Analysis of Real Systems (MARS'18) and 6th International Workshop on Verification and Program Transformation (MARS/VPT 2018), Thessaloniki, Greece \|year=2018 \|series=Electronic Proceedings in Theoretical Computer Science \|volume=268 \|pages=41–87\|url=http://cadp.inria.fr/publications/Garavel-Marsso-18.html \|doi=10.4204/EPTCS.268.2\|arxiv=1803.10322 }}
	</ref>		</ref>