作者：罗敏 方琳 施炜利小系统理论set协议模型检测spin认证性
摘要：基于Lu＆Smolka的SET协议支付过程简化模型，在小系统理论的基础上，运用Promela语言对协议进行形式化建模，采用线性时态逻辑LTL公式对协议的认证性进行形式化描述。在网络环境被入侵者控制的假设下，运用SPIN发现攻击；采用atomic和Bit-state hashing等优化策略，降低模型检测的复杂性，提高验证效率；最后针对协议存在的漏洞提出协议改进方案。
注：因版权方要求，不能公开全文，如需全文，请咨询杂志社
《计算机与现代化》（CN：36-1137/TP）是一本有较高学术价值的大型月刊，自创刊以来，选题新奇而不失报道广度，服务大众而不失理论高度。颇受业界和广大读者的关注和好评。 《计算机与现代化》自创刊以来，以理论联系实际、促进应用开发为宗旨，主要刊登计算机专业方面的新理论、新技术及其在各个领域中应用成果的论文，设有系统分析与设计、软件工程、网络与通讯、过程控制、辅助设计、中文信息技术、人工智能、综合述评、应用与实践等栏目，既有相当的学术水平，又有现实的指导作用。
部级期刊
人气 850246 评论 75
人气 228559 评论 65
人气 211867 评论 35
省级期刊
人气 211070 评论 71
