Abstract
Every communication system requiring security properties is certainly critical. In order to study the security of communication systems, we have developed a methodology for the application of the formal analysis techniques of communication protocols to the analysis of cryptographic ones. We have extended the design and analysis phases with security properties. Our methodology uses a specification technique based on the HMSC/MSC requirement languages, and translates it into a generic schema for the SDL specification language, which is used for the analysis. Thus, the technique allows the specification of security protocols using a standard formal language and uses Object-Orientation for reusability purposes. The final goal is not only the formal specification of a security system, but to examine the possible attacks, and later use the specification in more complex systems.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
R. Alur, T. Henzinger, F. Mang, S. Qadeer, S. Rajamani, and S. Tasiran. Mocha: modularity in model checking. CAV 98: Computer-aided Verification, Lecture Notes in Computer Science 1427, pages 521–525. Springer-Verlag, 1998
M. Burrows, M. Abadi, and R. Needham. A logic of authentication. In Proceedings of the Royal Society, Series A, 426(1871):233–271, 1989
S.M. Bellovin and M. Merrit. Encrypted key exchange: Password-based protocols secure against dictionary attacks. In Proceedings of IEEE Symposium on Reseach in Security and Privacy, pages 72–84, 1992
G. Denker and J. Millen. CAPSL intermediate language. In Formal Methods and Security Protocols,1999. FLOC’ 99 Workshop
D. Dolev and A. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, IT-29:198–208, 1983
D. Hogrefe. Validation of SDL systems. Computer Networks and ISDN Systems, 28(12):1659–1667, June 1996
ITU-T, Geneva, Switzerland. Message Sequence Charts, 1999. ITU-T Recommendation Z.120
ITU-T, Geneva, Switzerland. Specification and Description Language (SDL), 1999. ITU-T Recommendation Z.100
G. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs, 1991
J. Lopez,, J.J. Ortega; J. M. Troya. Verification of authentication protocols using SDLMethod. First International Workshop on Security in Information Systems (SIS 2002), April 2002, pp. 61–71
G. Lowe. Towards a Completeness Result for Model Checking of Security Protocols. 11th IEEE Computer Security Foundations Workshop, pages 96–105. IEEE Computer Society, 1998
W. Marrero, E. Clarke, and S. Jha. Model checking for security protocols. DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997
C. Meadows. Open issues in formal methods for cryptographic protocol analysis. Proceedings of DISCEX 2000, pages 237–250. IEEE Comp. Society Press, 2000.
J. C. Mitchell, M. Mitchell, and U. Stern. Automated analysis of cryptographic protocols using Murphi. In Proceedings of IEEE Symposium on Security and Privacy, pages 141–151. IEEE Computer Society Press, 1997.
M. Rusinowich, M. Turuani. Protocol Insecurity with Finite Number of Sessions is NPcomplete. 14th IEEE Computer Security Foundations Workshop June 11–13, 2001
P. Ryan and Scheneider. The Modelling and Analysis of Security Protocols: the CSP Approach. Addison-Wesley, 2001
A. Sarma J. Ellsberger, D. Hogrefe. SDL-Formal object-oriented language for communication systems. Prentice-Hall, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lopez, J., Ortega, J.J., Troya, J.M. (2002). Protocol Engineering Applied to Formal Analysis of Security Systems. In: Davida, G., Frankel, Y., Rees, O. (eds) Infrastructure Security. InfraSec 2002. Lecture Notes in Computer Science, vol 2437. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45831-X_17
Download citation
DOI: https://doi.org/10.1007/3-540-45831-X_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44309-4
Online ISBN: 978-3-540-45831-9
eBook Packages: Springer Book Archive