| 基于行为时序逻辑TLA的安全协议形式化分析与检测 |
| |
| 引用本文： | 白圣广,龙士工.基于行为时序逻辑TLA的安全协议形式化分析与检测[J].贵州大学学报(自然科学版),2012,29(2):99-101. |
| |
| 作者姓名： | 白圣广 龙士工 |
| |
| 作者单位： | 贵州大学 计算机科学与信息学院,贵州 贵阳,550025 |
| |
| 基金项目： | 国家自然科学基金资助项目 |
| |
| 摘 要： | 随着近年来网络协议的不安全性,对安全协议进行形式化分析与检测则显的非常重要。而基于行为时序逻辑TLA的模型检测是形式化分析检测方法中重要的一种。本文主要采用基于TLA的HLPSL语言形式化分析与检测H.530协议。
|
| 关 键 词： | 行为时序逻辑 安全协议 HLPSL |
Formal Analysis and Check of Security Protocol Based on Temporal Logic of Actions TLA |
| |
| BAI Sheng-guang
,
LONG Shi-gong.Formal Analysis and Check of Security Protocol Based on Temporal Logic of Actions TLA[J].Journal of Guizhou University(Natural Science),2012,29(2):99-101. |
| |
| Authors: | BAI Sheng-guang LONG Shi-gong |
| |
| Institution: | (College of Computer Science and information,Guizhou University,Guiyang 550025,China) |
| |
| Abstract: | with the insecurity of network protocol,formal analysis and check of the security protocol is very important.And model checking based on Temporal Logic of Actions TLA is one of important form validation method.This paper mainly analyses and checks H.530 protocol with HLPSL based on TLA language. |
| |
| Keywords: | temporal logic of actions security protocol HLPSL |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
