| 基于TLA的Kerberos协议符号化与检测 |
| |
| 引用本文： | 万良,李样.基于TLA的Kerberos协议符号化与检测[J].贵州大学学报(自然科学版),2007,24(6):605-609. |
| |
| 作者姓名： | 万良 李样 |
| |
| 作者单位： | 贵州大学,计算机理论研究所,贵州,贵阳,550025 |
| |
| 摘 要： | Leslie Lamport提出的一种新逻辑:行为时序逻辑TLA(Temporal Logic of Actions),它能在一种语言中同时表达模型程序与逻辑规则。AVISPA是基于行为时序逻辑的用HLPSL语言编程的协议安全检测工具。文中提出对Kerberos协议角色化,然后用AVISPA工具对HLPSL编码进行检测,结果表明用基于TLA的检测工具是宜于使用且有效的。
|
| 关 键 词： | 行为时序逻辑 角色 模型检测 |
| 文章编号： | 1000-5269（2007）06-0605-05 |
| 修稿时间： | 2007-10-05 |
TLA Based Kerberos Specification and Verification |
| |
| WAN Liang,LI Xing.TLA Based Kerberos Specification and Verification[J].Journal of Guizhou University(Natural Science),2007,24(6):605-609. |
| |
| Authors: | WAN Liang LI Xing |
| |
| Institution: | Institute of Computer Software and Theory, Guizhou University, Guiyang 550025, China |
| |
| Abstract: | Leslie Lamport put forward a new logic: TLA.A program logic expresses both programs and properties with a single language.The AVISPA Tool provides a suite of applications for building and analyzing formal models of security protocols.Protocol models are written in the High Level Protocol Specification Language,or HLPSL.Then some roles are designed about Kerberos protocol,after that it is expressed by HLPSL and checked by AVISPA tool.The results indicate that the tool based on TLA is very effectual. |
| |
| Keywords: | TLA role model-checking |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
