收稿日期: 2001-09-19
修回日期: 2001-10-19
网络出版日期: 2002-01-10
基金资助
973资助项目(G1999035802);国家杰出青年科学基金资助项目(60025205)
Invariant Generation Techniques in Cryptographic Protocol Analysis
Received date: 2001-09-19
Revised date: 2001-10-19
Online published: 2002-01-10
范红 , 冯登国 , 郭金庚 . 安全协议形式化分析的不变式生成技术[J]. 中国科学院大学学报, 2002 , 19(1) : 91 -96 . DOI: 10.7523/j.issn.2095-6134.2002.1.013
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
[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
/
| 〈 |
|
〉 |
