Verification methods of secure systems based on logical specifications

基于逻辑规范的安全系统验证方法

• 批准号: 12133204
• 负责人: YONEZAKI Naoki
• 金额: $ 25.92万
• 依托单位: Tokyo Institute of Technology
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research on Priority Areas
• 财政年份: 2000
• 资助国家: 日本
• 起止时间: 2000 至 2003
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-12133204/
• 关键词: Safety critical system; specification analysis; safe program synthesis; network security analysis; security protocol; secure system architecture; security of cryptographic primitives; verification and synthesis of hardware; 安全性検証; 暗号方式; ネットワークセキ

Our research results fall into fourfold.1)Verification and synthesis method for keeping safety of reactive systems. We developed verification methods for specifications of reactive systems. These verification systems examine whether a specification satisfy the condition that for any infinite behavior of environment, the reactive system can properly react against it forever. We found various techniques for the implementation of an efficient verification system.2) Network security. We defined an axiomatic system that can verify security properties of security protocols. Based on this inference rules, we also design construction rules for security protocols. By introducing several criteria of costs of protocols, optimized protocols are generated for each purpose. We also developed an analysis method for fairness of auction protocols. A new computational model is introduced, with which we can analyze the resistivity of the system for this kind of attack.3) Construction of secure system arc … More hitecture. Once an intruder succeeds to get privilege of the super-user, he can easily intrude connecting other systems by abusing user switching mechanism. For this security problem, we gave a solution in which the user interfaces of other system components are unchanged but we introduced user authentication mechanism to the user switching mechanism. The intruder trying to avoid this mechanism is also detected in our system.4) Fundamental theories. We analyzed various encryption schemes and hash functions in axiomatic way and strictly formalized various security properties e.g. partial information of contents in cipher text cannot leak out. We also proved their sufficient conditions. Analysis of such security properties in axiomatic way is new and is not found anywhere. For verification of reactive systems, we gave a proof method for temporal logic of finite frames and prove its completeness. It is not trivial to give the complete proof method because finiteness is not first order definable. Less

我们的研究成果主要有四个方面：1）反应系统安全性的验证与综合方法。我们开发了验证方法的反应系统的规格。这些验证系统检查一个规格说明是否满足条件，对于环境的任何无限行为，反应系统可以永远正确地对它作出反应。我们发现了实现有效验证系统的各种技术。2）网络安全。我们定义了一个公理系统，可以验证安全协议的安全属性。在此基础上，我们还设计了安全协议的构造规则。通过引入多个协议代价准则，为每种目的生成优化协议。我们还提出了一种分析拍卖协议公平性的方法。介绍了一种新的计算模型，利用该模型可以分析系统对此类攻击的抵抗能力。3）安全系统弧的构建 ...更多信息 体系结构一旦入侵者成功获得超级用户的权限，他就可以通过滥用用户切换机制轻易地入侵其他系统。针对这一安全问题，我们给出了一种解决方案，在此方案中，系统其他组件的用户界面保持不变，但在用户切换机制中引入了用户认证机制。试图避开这种机制的入侵者也在我们的系统中被检测到。4）基本理论。对各种加密方案和散列函数进行了公理化的分析，并对密文内容的部分信息不能泄漏等安全性质进行了严格的形式化。我们还证明了它们的充分条件。以公理化的方式分析这样的安全属性是新的，并且在任何地方都找不到。针对反应式系统的验证问题，给出了有限框架时态逻辑的一种证明方法，并证明了其完备性。给出完整的证明方法并不简单，因为有限性不是一阶可定义的。少

项目成果

Kazuyoshi Negishi, Naoki Yonezaki: "Verification Method for Consistency and Normal Termination Agreement on Multiple Sessions with the Same Principals in a Security Protocol"IPSJ Journal. Vol.41, No.08. 2281-2290 (2000)

Kazuyoshi Negishi、Naoki Yonezaki：“安全协议中具有相同主体的多个会话的一致性和正常终止协议的验证方法”IPSJ 期刊。

Maato Suto, Shin-ya Nishizaki: "Semantics of Call-by-name Environment Calculus"IPSJ Transactions on Programming. Vol.41, No.SIG03. 52-61 (2000)

Maato Suto、Shin-ya Nishizaki：“按名称调用环境演算的语义”IPSJ 编程交易。

Takenobu Aoshima, Naoki Yonezaki: "An efficient tableau-based verification method with partia evaluation for reactive system specifications"Proc.of The 10th European-Japanese Conf.On Information Modelling and Knowledge Bases. 337-348 (2000)

Takenobu Aoshima、Naoki Yonezaki：“一种有效的基于表格的验证方法，具有反应式系统规范的部分评估”Proc.of 第 10 届欧洲-日本信息模型和知识库会议。

Curtis Nelson, Chris Myers, Tomohiro Yoneda: "Efficient Verification of Hazard-Freedom in Gate-Level Timed Asynchronous Circuits"Proc of 2003 International Conference on Computer Aided Design. 424-431 (2003)

Curtis Nelson、Chris Myers、Tomohiro Yoneda：“门级定时异步电路中无危险性的有效验证”2003 年计算机辅助设计国际会议的会议记录。

T.Kitai, Y Oguro, T.Yoneda, E.Mercer, C.Myers: "Partial Order Reduction for Timed Circuit Verification Based on a Level Oriented Model"電子情報通信学会英文論文誌. E86-D(12). 2601-2611 (2003)

T.Kitai、Y Oguro、T.Yoneda、E.Mercer、C.Myers：“基于面向水平模型的定时电路验证的部分阶次减少”IEICE 英文期刊。2601 -2611 (2003)。 ）