Abstract
A detailed example is given of how a formal specification language has been used to specify an international banking standard on message authentication. It illustrates how a specification language can be used to specify and validate a standard.
The work described in this report demonstrates the application of formal methods to the standards area and it is recommended that formal methods should be used in the formulation and description of appropriate standards.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
BS 7102 (2):1989, 8731-02:1987. Banking — Approved algorithm for message authentication — Part 2: Message authenticator algorithms. Obtainable from: Sales Department, BSI, Linford Wood, Milton Keynes, MK14 6LE.
G.I. Parkin and G. O'Neill. Specification of the MAA Standard in VDM. NPL Report DITC 160/90. February 1990.
BS 7101:1989, ISO 8730:1986. Protecting authentic wholesale messages between financial institutions. Obtainable from: Sales Department, BSI, Linford Wood, Milton Keynes, MK14 6LE.
D.W. Davies and D.O. Clayden. The Message Authenticator Algorithm (MAA) and its Implementation. NPL Report DITC 109/88. February 1988.
C.B. Jones. Systematic Software Development Using VDM. Prentice-Hall International, 1986.
M.K.F. Lai. A formal interpretation of the MAA standard in Z. NPL Report DITC 184/91. June 1991.
H.B. Munster. LOTOS specification of the MAA standard. NPL Report to be published.
C.L.N. Ruggles (Ed.). Formal Methods in Standards, A Report from the BCS Working Group. Springer-Verlag, 1990.
M. Wolczko. Typesetting VDM in LAT E X. Dept. of Computer Science, The University, Manchester, M13 9PL. March 1988.
BSI IST/5/19. VDM Specification Language Proto-Standard. British Standards Institution, 29 March 1990.
I.P. Dickinson. Typesetting VDM-SL with V DM S L macros. National Physical Laboratory, Teddington, Middlesex, TW11 0LW. 20 February 1991.
IEC/ISO. Rules for the drafting and presentation of International Standards. 1986.
ISO/DIS 8730, Banking — Requirements for message authentication (wholesale). 1987.
D.W. Davies and W.L. Price. Security for Computer Networks, An Introduction to Data Security in Teleprocessing and Electronic Funds Transfer. John Wiley & Sons, 1984.
B.W. Kernighan and D.M. Ritchie. The C Programming Language. Prentice-Hall, 1978.
D.A. Turner. An Overview of Miranda. SIGPLAN Notices, December 1986.
ISO/IEC JTC1 SC22/WG13/D106. Modula-2 Standard, Third Working Draft. British Standards Institution, 29 October 1989.
R.P. Lampard. An implementation of MAA from a VDM specification. NPL Technical Memorandum DITC 50/91. January 1991.
D.J.Andrews, A. Garg, S.P.A. Lau, J.R. Pitchers. The Formal Definition of Modula-2 and Its Associated Interpreter. Lecture Notes in Computer Science, Vol 328, Springer-Verlag 1988.
D.J. Andrews. Report from the BSI Panel for the Standardisation of VDM (IST/5/50). Lecture Notes in Computer Science, Vol 328, Springer-Verlag 1988.
ISO/DIS 8731-2, Banking — Approved algorithm for message authentication — Part 2: Message authenticator algorithms, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Parkin, G.I., O'Neill, G. (1991). Specification of the MAA standard in VDM. In: Prehn, S., Toetenel, W.J. (eds) VDM'91 Formal Software Development Methods. VDM 1991. Lecture Notes in Computer Science, vol 551. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54834-3_31
Download citation
DOI: https://doi.org/10.1007/3-540-54834-3_31
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54834-8
Online ISBN: 978-3-540-46449-5
eBook Packages: Springer Book Archive