Formaler Entwurf effizienter Autentisierungsprotokolle mit Schlüsselabsprache
Gunnar Jacobson
The author presents a new, original method for the formal requirements definition and the design of authentication and key-agreement protocols and demonstrates its usage as a design-tool for such protocols. The exemplary formal design of Kerberos demonstrates the applicability and reliability of the method. The author then classifies cryptosystems and protocol runs and provides a generic design approach, which is on an idealised layer independent from the cryptosystem to be used. Generic design schemes for two- and three-party protocols are being worked out and it is shown, how concrete specifications of new protocols may be derived easily. Doing this, specifications of new protocol are generated, for example a three-party private-key protocol.
The design is done by applying logical rules, starting from the protocol goals and prerequisites, which have been previously defined in a requirements definition. The author introduces a new representation technique for this. The author's approach is the inverse application of the popular logic of Burrows, Abadi and Needham, which has up to now been used for the verification of authentication and key-agreement protocols. The new method is called the inverse BAN logic. The representation of the protocol behaviour is done using the specification and description language SDL. This new representation is called "SDL combined with inverse BAN logic", SDL/iBAN. Furthermore, the author presents a development model, which enables a layered, general development of such protocols. [written in German]
Key words: Security protocols, authentication, key agreement, key distribution, formal methods, formal design, BAN logic, Kerberos, SDL.
ISBN 9783895869532. LINCOM Studies in Computer Science 02. 2000.
