基于TLA的NS安全协议分析及检测

doi:10.3969/j.issn.1007130X.2010.

J4 ›› 2010, Vol. 32 ›› Issue (7): 38-41.doi: 10.3969/j.issn.1007130X.2010.

基于TLA的NS安全协议分析及检测

黄贻望1,2,万良1,李祥1

(1.贵州大学计算机软件与理论研究所，贵州贵阳 550025;2.铜仁学院数学与计算机科学系，贵州铜仁 554300)

收稿日期:2009-06-05 修回日期:2009-08-26 出版日期:2010-06-25 发布日期:2010-06-25
通讯作者: 黄贻望 E-mail:hywcxq1@163.com
作者简介:黄贻望（1978），男，湖南怀化人，硕士生，研究方向为模型检测与协议分析；万良，博士生，研究方向为模型检测与协议分析；李祥，教授，博士生导师，研究方向为计算机理论与密码学。

Analysis and Checking of the NS Security Protocol Based on the Temporal Logic of Action

HUANG Yiwang1,2，WAN Liang1，LI Xiang1

(1.Institute of Computer Software and Theory,Guizhou University,Guiyang 550025;
2.Department of Mathematics and Computer Science,Tongren College,Tongren 554300,China)

Received:2009-06-05 Revised:2009-08-26 Online:2010-06-25 Published:2010-06-25
Contact: HUANG Yiwang E-mail:hywcxq1@163.com

摘要/Abstract

摘要：

行为时序逻辑是一种组合了时序逻辑与行为逻辑来对并发系统进行描述与验证的逻辑，在描述并发转移系统中，行为时序逻辑通过引入行动和行为的概念，使得系统和属性可用同一种行为时序逻辑来表示。本文首先介绍行为时序逻辑的语法、语义及简单推理规则；然后以典型的NS公开密钥协议为例，对其进行形式化分析，建立了入侵者参加的简化模型。通过对模型进行FSM建模，转化为TLA+描述的规约系统，然后对其进行TLC检测，发现其存在中间人的重放攻击。

关键词: 安全协议, 模型检测, TLA, TLA+, TLC

Abstract:

TLA is a logic which combines the temporal logic and the logic of action,describing and validating the concurrent systems with TLA. TLA can express the system and the corresponding properties by adding actions and behaviors.First,this paper introduces the grammer,semantics and simple reasoning rules, and then formally analyzes the NS protocol, and sets up the FSM model, and specifies the model with TLA+, and then checks the corresponding properties with the tool of TLC. The results of checking shows there exists middleman’s replay attack.

Key words: security protocol；model checking；TLA；TLA+；TLC

黄贻望1,2,万良1,李祥1. 基于TLA的NS安全协议分析及检测[J]. J4, 2010, 32(7): 38-41.

HUANG Yiwang1,2，WAN Liang1，LI Xiang1. Analysis and Checking of the NS Security Protocol Based on the Temporal Logic of Action[J]. J4, 2010, 32(7): 38-41.

[1]	刘子源, 马占有, 李霞, 高滢囡, 何娜娜, 黄瑞祺. 基于模糊测度的模糊分支时态逻辑模型检测[J]. 计算机工程与科学, 2024, 46(04): 676-683.
[2]	李召恺, 马占有, 李健祥, 郭昊. 基于模糊决策过程的模糊计算树逻辑模型检测[J]. 计算机工程与科学, 2022, 44(02): 266-275.
[3]	黄文杰, 向凤红, 毛剑琳. 基于LM_RBF-PID的板球系统轨迹控制[J]. 计算机工程与科学, 2020, 42(08): 1423-1429.
[4]	郑小宇, 刘冬梅, 杜益宁, 周子健, 邱玫媚, 朱鸿. 模式驱动的系统安全性设计的验证[J]. 计算机工程与科学, 2020, 42(07): 1197-1207.
[5]	袁申,魏杰林,李永明. 具有多值决策过程的广义可能性计算树逻辑模型检测[J]. 计算机工程与科学, 2019, 41(01): 88-97.
[6]	钟小妹，肖美华，李伟，谌佳，李娅楠. RFID超轻量级认证协议RCIA形式化分析与改进[J]. 计算机工程与科学, 2018, 40(12): 2183-2192.
[7]	王亚鹏，雷丽晖. 基于CTL模型检测的胃腺癌核心路径形式化验证[J]. 计算机工程与科学, 2018, 40(12): 2280-2286.
[8]	雷丽晖，郭越，张延波. 可能性测度下的CTL符号化模型检测[J]. 计算机工程与科学, 2018, 40(11): 2008-2014.
[9]	陈昱，王淼，任海燕，曾立. 星载感应式磁力仪地面检测系统及数据预处理软件设计[J]. 计算机工程与科学, 2018, 40(09): 1606-1610.
[10]	肖美华1，梅映天1,2，李伟1，李娅楠1，钟小妹1，宋子繁1. 基于时间戳私钥签名技术的Nayak-T协议安全性分析[J]. 计算机工程与科学, 2017, 39(12): 2252-2259.
[11]	袁红娟1,2,马艳芳3,潘海玉1,2. 模糊交互时态逻辑的模型检测[J]. 计算机工程与科学, 2017, 39(12): 2290-2296.
[12]	吴格格，庄雷，张坤丽，王国卿. 移动支付协议PCMS的形式化分析和验证[J]. 计算机工程与科学, 2017, 39(01): 67-73.
[13]	秦济龙1，李庆华2，王恩东1，公维锋1，张峰1，牛赟3，乌力吉3，张向民3. 一种路由交换阵列节点芯片及其系统的设计与实现[J]. 计算机工程与科学, 2016, 38(12): 2392-2401.
[14]	文延东1,2，文双春1，刘昱2，卫宝跃2，张以涛2，曹检飞1,2. 基于软件无线电的通信信号测试平台设计与实现[J]. 计算机工程与科学, 2016, 38(09): 1769-1774.
[15]	阮志毅，沈有建，刘凤玲. 基于数学形态学的模糊集理论在车牌字符识别中的运用[J]. J4, 2016, 38(03): 562-568.

基于TLA的NS安全协议分析及检测

Analysis and Checking of the NS Security Protocol Based on the Temporal Logic of Action

PDF

可视化

摘要/Abstract

引用本文

使用本文

相关文章 15

编辑推荐

Metrics

本文评价