4结束语
    Dolev-Yao模型的安全协议形式化方法在高抽象层次建立协议模型，即在 “完善”的密码系统基础上讨论安全协议本身的安全属性，这样无法避免密码原语适应性的攻击。本文分析了对于NSL协议的同态攻击，并提出了一个改进方案，在协议中增加一个哈希函数破坏了同态结构。安全协议形式化方法设计的一个趋势是安全协议设计时同时考虑密码协议算法的性质，必须把形式化分析方法和密码可靠性结合起来。
    参考文献：
    [1] D. Dolev, A. C. Yao. On the Security of Public key protocols, Proceedings of the IEEE 22nd Annual Symposium on Foundations of Computer Science, pages 34-39. IEEE computer Society Press, 1983.
    [2] Burrows M, Abadi M, Needham R. A  Logic of Authentication. ACM Transactions in Computer Systems, 8(1):18-36, 1990
    [3] Lawrence C. Paulson. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 6:85-128, 1998
    [4] Fabrega F J T, Hertzog J, Guttman J. Strand Spaces: Proving Security Protocols Correct. Journal of Computer Security, 7(2/3):191-23,1999
    [5] Schneider S. Verifying Authentication Protocols in CSP.  IEEE Transaction on Software Engineering, 24(9):741-758 ,1998,
    [6] C. Meadows. The NRL protocol analyzer: An overview.   The Journal of Logic Programming, 26(2), 113-131, 1996
    [7] Cortier V, Delaune S, Lafourcade P. A Survey of Algebraic Properties Used in Cryptographic Protocols. Journal of Computer Security, 14(1):1-43, 2006
    [8]  S Delaune, P Lafourcade, D Lugiez, R Treinen – Citeseer.  Symbolic Protocol Analysis in Presence of a Homomorphism Operator and Exclusive Or , Automata, Languages and Programming , Volume 4052,Pages 132-143,2006
 

(责任编辑：)