Applying Formal Methods to the Analysis of a Key Management Protocol
作者： Catherine Meadows
关键词:
摘要: In this paper we develop methods for analyzing key management and authentication protocols using techniques developed the solutions of equations in a term rewriting system. particular, describe model class possible attacks on those as systems, also software tool based narrowing algorithm that can be used analysis such protocols. We formally protocol results these to analyze security properties. show how flaw was found, verification corrected scheme techniques.
medra.org 参考文章(29)
Catherine A. Meadows, A System for the Specification and Verification of Key Management Protocols. ieee symposium on security and privacy. pp. 182- 197 ,(1991)
Oded Goldreich, Shimon Even, Adi Shamir, On the Security of Ping-Pong Protocols when Implemented using the RSA international cryptology conference. pp. 58- 72 ,(1985)
Pierre Rety, Claude Kirchner, Hélène Kirchner, Pierre Lescanne, NARROWER: a new algorithm for unification and its application to Logic Programming Rewriting Techniques and Applications. pp. 141- 157 ,(1985) , 10.1007/3-540-15976-2_7
Paul F. Syverson, A Logic for the Analysis of Cryptographic Protocols Defense Technical Information Center. ,(1990) , 10.21236/ADA230779
Gérard Huet, Derek C. Oppen, Equations and rewrite rules: a survey Formal Language Theory#R##N#Perspectives and Open Problems. pp. 349- 405 ,(1980) , 10.1016/B978-0-12-115350-2.50017-8
Katherine A. Yelick, Unification in combinations of collapse-free regular theories Journal of Symbolic Computation. ,vol. 3, pp. 153- 181 ,(1987) , 10.1016/S0747-7171(87)80025-1
D. E. Knuth, P. B. Bendix, Simple Word Problems in Universal Algebras Computational Problems in Abstract Algebra#R##N#Proceedings of a Conference Held at Oxford Under the Auspices of the Science Research Council Atlas Computer Laboratory, 29th August to 2nd September 1967. pp. 342- 376 ,(1983) , 10.1007/978-3-642-81955-1_23
R. K. Bauer, T. A. Berson, R. J. Feiertag, A key distribution protocol using event markers ACM Transactions on Computer Systems. ,vol. 1, pp. 249- 255 ,(1983) , 10.1145/357369.357373
Dianne E. Britton, Formal Verification of a Secure Network with End-to-End Encryption ieee symposium on security and privacy. pp. 154- 154 ,(1984) , 10.1109/SP.1984.10009
Collin I'Anson, Chris Mitchell, Security defects in CCITT recommendation X.509 ACM SIGCOMM Computer Communication Review. ,vol. 20, pp. 30- 34 ,(1990) , 10.1145/378570.378623