Journal of University of Chinese Academy of Sciences >
Invariant Generation Techniques in Cryptographic Protocol Analysis
Received date: 2001-09-19
Revised date: 2001-10-19
Online published: 2002-01-10
Formal methods for cryptographic protocol analysis has drawn attention in recent years This leads to a development of the generation and specification techniques of invariant Invariantis defined what messages an intruder can and cannot learn and can be used to prove authentication as well as secrecy results, appear to be central This paper introducls an overview of invariant in different systems, analyzes their relationships to each other, develops a simple taxonomy, and discuses some of the implications for future research.
Key words： cryptographic protocols; formal analysis; invariant
FAN Hong , FENG DengGuo , GUO JinGeng . Invariant Generation Techniques in Cryptographic Protocol Analysis[J]. Journal of University of Chinese Academy of Sciences, 2002 , 19(1) : 91 -96 . DOI: 10.7523/j.issn.2095-6134.2002.1.013
[1] L C P aulson.The Inductive Approach to Verifying Cryptog raphic Pro toco ls.Journal of Computer Secur ity, 1998, 6:85～128.
[2] D Do lev, O Grumberg, D Peled.Model Checking.M TN Press, 1999.
[3] N Heintze, J D Tyg ar.A Model fo r Secure P rot oco ls and their Composition.IEEE Transactio n o n Softwa re Engineering, 1996, 22(16).
[4] Michael Burrows, Mar tin Abadi, Roger Needham.A Logic of Authentication.ACM T ransactions in Compute r Systems, 1990, 8(1):1 8～ 36.
[5] Da rrell Kindred.T heory Generation for Security P roto co ls:〔PhD thesis〕.Carnegie Mello n University, 1999.
[6] F Jav ier T haye r Fabreg a, Jonathan C Herzog, Joshua D Guttman.St rand Space:Why is a Security Pro tocol Correct ? In:Proceedings of the 1998 IEEE Symposium on Security and Pr iv acy.IEEE Computer So ciety Press, 1998.160～ 171.
[7] C Meadows.Analysis of the Internet Key Exchange Protocol Using the NRL ProtocolAnaly zer.In:Proceedings of the 1999 Symposium on Security and Privacy. IEEE Computer Society P ress.1999.
[8] G Lowe.Breaking and Fixing theNeedham-Schrode r Public-key Pro tocol Using FDR.In:Tools and Algori thms for the Construction and Analysis of Systems,volume 1055 o f Lecture No tes in Computer Science.Ber lin:Springer-Verlag, 1996.147～166.
[9] 冯登国.国内外信息安全研究现状及其发展趋势.网络安全技术与应用, 2001, 1(1).
[10] 冯登国.计算机通信网络安全.北京:清华大学出版社, 2001.
[11] 范红, 冯登国.密码协议形式化分析的研究现状与有关问题.网络安全技术与应用, 2001, 8
/
| 〈 |
|
〉 |