| 基于迹语义的网络安全协议形式化分析 |
| |
| 引用本文： | 冯珺珺,李光耀,江耘.基于迹语义的网络安全协议形式化分析[J].计算机与现代化,2007(2):107-109. |
| |
| 作者姓名： | 冯珺珺 李光耀 江耘 |
| |
| 作者单位： | 1. 同济大学CAD研究中心,上海,200092
2. 南昌大学信息工程学院,江西,南昌,330029 |
| |
| 摘 要： | 形式化方法是提高软件系统,特别是safety-critical系统的安全性与可靠性的重要手段.本文提出了一种新的简单的迹语义,用于刻画协议部分安全性质,即只针对协议规约的单个主体,此技术支持协议设计者对安全性质进行形式化规约.运用此技术和模型检测器SPIN找到了两种针对TMN协议的攻击,证明了此方法的实用性,可方便地用于其它网络安全协议验证.
|
| 关 键 词： | 安全协议 形式化方法 迹语义 模型检测 SPIN/Promela 语义 网络安全 协议形式化分析 Semantics Trace Based Security Protocols Network Analysis 协议验证 形式化方法 SPIN 检测器 模型 运用 形式化规约 协议设计 支持 主体 安全性质 |
| 文章编号： | 1006-2475（2007）02-0107-03 |
| 收稿时间： | 2006-10-26 |
| 修稿时间： | 2006年10月26 |
Formal Analysis for Network Security Protocols Based on Trace Semantics |
| |
| FENG Jun-jun,LI Guang-yao,JIANG Yun.Formal Analysis for Network Security Protocols Based on Trace Semantics[J].Computer and Modernization,2007(2):107-109. |
| |
| Authors: | FENG Jun-jun LI Guang-yao JIANG Yun |
| |
| Affiliation: | 1. CAD Research Center of Tongji University, Shanghai 200092, China; 2. College of Information Engineering, Nanchang University, Nanchang 330029, China |
| |
| Abstract: | Formal method has been advocated as an important means of improving the safety and reliability of software systems,especial those which are safety-critical.This paper proposes a new simple trace semantics that can be used to specify security properties,this technique supports a protocol designer to provide formal analysis of the security properties.It illustrates the utility of this technique by exposing two attacks on the well studied protocol TMN. |
| |
| Keywords: | security protocols formal method trace semantics model checking SPIN/Promela |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
