作者:冯珺珺; 李光耀; 江耘安全协议形式化方法迹语义模型检测
摘要:形式化方法是提高软件系统,特别是safety-critical系统的安全性与可靠性的重要手段。本文提出了一种新的简单的迹语义,用于刻画协议部分安全性质,即只针对协议规约的单个主体,此技术支持协议设计者对安全性质进行形式化规约。运用此技术和模型检测器SPIN找到了两种针对TMN协议的攻击,证明了此方法的实用性,可方便地用于其它网络安全协议验证。
注:因版权方要求,不能公开全文,如需全文,请咨询杂志社
《计算机与现代化》(CN:36-1137/TP)是一本有较高学术价值的大型月刊,自创刊以来,选题新奇而不失报道广度,服务大众而不失理论高度。颇受业界和广大读者的关注和好评。 《计算机与现代化》自创刊以来,以理论联系实际、促进应用开发为宗旨,主要刊登计算机专业方面的新理论、新技术及其在各个领域中应用成果的论文,设有系统分析与设计、软件工程、网络与通讯、过程控制、辅助设计、中文信息技术、人工智能、综合述评、应用与实践等栏目,既有相当的学术水平,又有现实的指导作用。
部级期刊
人气 850789 评论 75
人气 230144 评论 65
人气 214524 评论 35
省级期刊
人气 212897 评论 71