TMN协议的形式化分析

• Original Articles • Previous Articles Next Articles

An approach to the formal analysis of the TMN protocol

LIU Xiu-ying1,2;ZHANG Yu-qing2;YANG Bo1;XING Ge2

(1. State Key Lab. of Integrated Service Networks, Xidian Univ., Xi'an 710071, China;
2. National Computer Network Intrusion Protection Center, Chinese Academy of Sciences, Beijing 100039, China)

Received:1900-01-01 Revised:1900-01-01 Online:2004-10-20 Published:2004-10-20

Abstract

Abstract: This paper analyzes the TMN protocol comprehensively using a formal analysis method called the running-mode analysis and uncovers a number of attacks on the TMN protocol. According to the detailed forms of these attacks and the different intentions of the intruder, we classify these attacks. Finally, linking with known attacks, we deduce that the running-mode analysis has analyzed the TMN protocol effectively.

Key words: TMN protocol, model checking, cryptographi protocol, running-mode analysis

CLC Number:

TP309

LIU Xiu-ying1;2;ZHANG Yu-qing2;YANG Bo1;XING Ge2.

An approach to the formal analysis of the TMN protocol

[J].J4, 2004, 31(5): 785-790.

[1]	SHEN Lixiang,MU Dejun,CAO Guo,XIE Guangqian,SHU Fangyong. Constructing formal verification models for hardware Trojans [J]. Journal of Xidian University, 2021, 48(3): 146-153.
[2]	SHU Xinfeng,WANG Changtai,WANG Yan,ZHANG Lili. Propositional projection temporal logic based distributed model checking method [J]. Journal of Xidian University, 2020, 47(4): 39-47.
[3]	DING Ming,ZHANG Shuling,ZHANG Chen,Zhang Jun. Method for the verification of safety requirements of avionics systems [J]. Journal of Xidian University, 2019, 46(3): 66-73.
[4]	DUAN Zhao, LIU Kunlong. Dynamic program verification via a CPAChecker [J]. Journal of Xidian University, 2019, 46(1): 33-38.
[5]	PANG Tao;DUAN Zhenhua;LIU Xiaofang. Symbolic model checking of Verilog programs with the propositional projection temporal logic [J]. J4, 2014, 41(2): 79-84.
[6]	YANG Yuanyuan;MA Wenping;LIU Weibo;YU You;GU Jian. Automatic detection of security protocols with XOR [J]. J4, 2012, 39(4): 120-125+183.
[7]	YANG Chen;DUAN Zhenhua. Stutter-invariant propositional interval temporal logic [J]. J4, 2011, 38(2): 151-156.
[8]	ZHANG Hai-bin;DUAN Zhen-hua. Model checking interval temporal logic [J]. J4, 2009, 36(2): 338-342.
[9]	ZHANG Hai-bin;DUANG Zhen-hua. Model checking multirate hybrid systems [J]. J4, 2008, 35(1): 60-648.
[10]	GUO Jian1;JIN Nai-yong2. Vacuity detection in computation temperal logic [J]. J4, 2007, 34(5): 794-799.
[11]	ZHANG Hai-bin;DUAN Zhen-hua. Decidability of the dense timed interval temporal logic [J]. J4, 2007, 34(3): 463-467.

An approach to the formal analysis of the TMN protocol

Like

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 11

Metrics

Comments

Recommended 10