Abstract
We present a new method for the formal requirements specification and the design of Authentication and Key-Agreement protocols. The method “SDL combined with inverse BAN logic”, SDL/iBAN is based on the inverse application of the BAN logic of Burrows, Abadi and Needham and the integration with the Specification and Description Language SDL. The exemplary formal design of Kerberos demonstrates the applicability and reliability of the method. We classify cryptosystems and protocol runs and provide a generic design approach, which is on an idealised layer independent from the cryptosystem to be used. We show, how concrete specifications of new protocols may be derived and propose the integration of our method with existing specification methods and software development tools.
Chapter PDF
Similar content being viewed by others
Keywords
- Initial Assumption
- Protocol Message
- Level Belief
- IEEE Computer Security Foundation Workshop
- Generic Design Scheme
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
M. Abadi and R. Needham. Prudent Engineering Practice for Cryptographic Protocols. Digital Systems Research Center Research Report 125, 1994.
R. Anderson and R. Needham. Robustness Principles for Public Key Protocols. In Advances in Cryptology CRYPTO ‘85 Proceedings, Springer Verlag, 1995, pp. 236–247.
M. Bellare and P. Rogaway. Entity Authentication and Key Distribution. In Advances in Cryptology CRYPTO ‘83 Proceedings, Springer Verlag, 1993, pp. 232–249.
M. Burrows, M. Abadi, and R. Needham. A Logic of Authentication. Digital Systems Research Center Research Report 39, 1989.
L. Buttyân, S. Staamann, and U. Wilhelm. A Simple Logic for Authentication Protocol Design. In 11 th IEEE Computer Security Foundations Workshop, 1998, pp. 153–162.
D. Denning and G. Sacco. Timestamps in Key Distribution Protocols. Communications of the ACM, 24 (2), 1981, pp. 58–68.
W. Diffie and M.E. Hellman. New Directions in Cryptography. IEEE Transactions on InformationTheory Vol. IT-22 No.6, 1976, pp. 644–654.
L. Gong, R. Needham, and R. Yahalom. Reasoning about Belief in Cryptographic Protocols. Proc. of the 1990 IEEE Computer Society Symposium on Research in Security and Privacy, 1990, pp. 234–248.
S. Gritzalis, D. Spinellis, and P. Georgiadis. Security Protocols over open networks and distributed systems: Formal Methods for their Analysis, Design, and Verification. Computer Communications Journal, Elsevier, 22 (8), 1999, pp. 695–707.
International Telecommunications Union ITU.”SDL Combined with ASN.1 (SDL/ASN.1)”. ITU Recommendation Z.105,1995.
R. Kemmerer, C. Meadows, and J. Millen. Three Systems for Cryptographic Protocol Analysis. Journal of Cryptology, 7(4); 1994, pp. 79–130.
J. Kohl. The Evolution of the Kerberos Network Authentication Service. In EurOpen Conference Proceedings, 1991, pp. 295–313.
G. Lowe. Breaking and Fixing the Needham-Schroeder Public-Key Protocol using FDR. Tools and Algorithms for the Construction and Analysis of Systems. In Lecture Notes in Computer Science, Springer Verlag,1996,pp. 147–166.
C.A. Meadows. Applying formal methods to the analysis of a key management protocol. Journal of Computer Security, 1 (1), 1992, pp. 5–35.
C.A. Meadows. Formal Verification of Cryptographic Protocols: A Survey. In Advances in Cryptology—ASIACRYPT’94 Proceedings, Springer Verlag, 1994, pp. 133–150.
R.M. Needham and M.D. Schroeder. Using Encryption for Authentication in large Networks of Computers. Communications of the ACM, 21 (12), 1978, pp. 993–999.
S. Pohlig and M. Hellman. An improved Algorithm for computing Logarithms in GF(p) and its cryptographic significance. IEEE Transactions on Information Theory, 24(1), 1978, pp. 106–111.
R. Rivest, A. Shamir, and L. Adleman. A Method for obtaining Digital Signatures and Public Key Cryptosystems. Communications of the ACM, 21(2), 1978, pp. 120–126.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Jacobson, G. (1999). Formal Design of Efficient Authentication and Key Agreement Protocols. In: Preneel, B. (eds) Secure Information Networks. IFIP — The International Federation for Information Processing, vol 23. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35568-9_7
Download citation
DOI: https://doi.org/10.1007/978-0-387-35568-9_7
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-6487-1
Online ISBN: 978-0-387-35568-9
eBook Packages: Springer Book Archive