Automatically detecting most vulnerabilities in cryptographic protocols
作者： S.H. Brackin
DOI: 10.1109/DISCEX.2000.824981
关键词:
摘要: The Automatic Authentication Protocol Analyzer, 2nd Version (AAPA2) is a fast, completely automatic tool for formally analyzing cryptographic protocols. It correctly identifies vulnerabilities or their absence in 43 of 51 protocols studied the literature, and it finds errors previously asserted authentication properties two large commercial This paper describes how AAPA2 13 16 vulnerable protocols, which earlier Analyzer (AAPA) only 6 these
sci-hub.se 参考文章(14)
Stephen H. Brackin, Deciding cryptographic protocol adequacy with HOL: The implementation Lecture Notes in Computer Science. pp. 61- 76 ,(1996) , 10.1007/BFB0105397
Makoto Tatebayashi, Natsume Matsuzaki, David B. Newman, Key Distribution Protocol for Digital Mobile Communication Systems international cryptology conference. pp. 324- 334 ,(1989) , 10.1007/0-387-34805-0_30
S.H. Brackin, Evaluating and improving protocol analysis by automatic proof ieee computer security foundations symposium. pp. 138- 152 ,(1998) , 10.1109/CSFW.1998.683164
S Gritzalis, D Spinellis, P Georgiadis, Security protocols over open networks and distributed systems: formal methods for their analysis, design, and verification Computer Communications. ,vol. 22, pp. 697- 709 ,(1999) , 10.1016/S0140-3664(99)00030-4
Catherine Meadows, The NRL Protocol Analyzer: An Overview☆ Journal of Logic Programming. ,vol. 26, pp. 113- 131 ,(1996) , 10.1016/0743-1066(95)00095-X
S.H. Brackin, An interface specification language for automatically analyzing cryptographic protocols network and distributed system security symposium. pp. 40- 51 ,(1997) , 10.1109/NDSS.1997.579219
L. Gong, R. Needham, R. Yahalom, Reasoning about belief in cryptographic protocols ieee symposium on security and privacy. pp. 234- 248 ,(1990) , 10.1109/RISP.1990.63854
G. Lowe, B. Roscoe, Using CSP to detect errors in the TMN protocol IEEE Transactions on Software Engineering. ,vol. 23, pp. 659- 669 ,(1997) , 10.1109/32.637148
J.K. Millen, S.C. Clark, S.B. Freedman, The Interrogator: Protocol Secuity Analysis IEEE Transactions on Software Engineering. ,vol. 13, pp. 274- 288 ,(1987) , 10.1109/TSE.1987.233151
S.H. Brackin, A HOL extension of GNY for automatically analyzing cryptographic protocols Proceedings 9th IEEE Computer Security Foundations Workshop. pp. 62- 76 ,(1996) , 10.1109/CSFW.1996.503691