安全相关的性质如访问控制等在复杂环境下有十分重要的作用。从程序验证方面来说，不仅考虑安全性和活性的验证，还要考虑一些安全策略的性质，如非干涉性，这些不能用一般的性质来描述的安全策略可以被看作“超安全性质”。限界约束可通用地表示不同程度的访问频次限制，是安全相关性质验证中有效的辅助方法之一，在无线传感器网络协议、嵌入式系统等重要领域的性质验证方面具有广泛的应用价值。主要研究网络安全策略中的安全相关性质的限界表达及基于该限界约束的验证规则。

Security-relevant properties such as access control in a complex environment play a very important role. In terms of procedural verification, not only the safety and activity verification are considered, but the nature of some security policies, such as non-interference, should also be considered. These security policies that cannot be described by the general nature can be considered as “hypersafety”. Boundary constraints are common to represent different degrees of access frequency restrictions. They are one of the effective auxiliary methods in safety-related property verification, and have wide application value in the attribute verification of wireless sensor network protocols, embedded systems and other important fields. Based on the above description, we propose an approach for extracting deductive proof of security-relevant properties under bounded constraints.
相关文章

[1]	陈松政，魏立峰. 基于用户身份标识的外设访问控制方法[J]. J4, 2015, 37(10): 1831-1835.
[2]	付青琴1,昂正全2,袁艳芳1. 一种改进的智能卡数据传输安全策略[J]. J4, 2014, 36(11): 2229-2233.
[3]	欧嵬1，王勇军1，韩文报2. 基于用户行为的可信模型研究[J]. J4, 2013, 35(5): 46-50.
[4]	陈晓苏 林植 肖道举. 基于策略的网络安全防护系统框架研究[J]. J4, 2007, 29(6): 7-9.
[5]	林晨 李之棠. VPN系统中安全策略系统的设计与实现[J]. J4, 2007, 29(6): 21-23.
[6]	裴晋泽[1] 胡华平[1] 周金泉[1,2]. 基于APDR信息系统安全防护体系模型的分级防护策略研究[J]. J4, 2006, 28(1): 33-35.
[7]	彭倩岚 李之棠. 分布式防火墙系统的安全机制设计[J]. J4, 2003, 25(2): 11-15.
[8]	蔡志平[1] 许江[2] 等. 程序演化及其在信息安全中的应用[J]. J4, 2002, 24(6): 11-13.
[9]	戴新发 袁由光. 一种嵌入式实时分布计算系统的安全策略设计[J]. J4, 2001, 23(5): 102-104.
[10]	腾猛 邹鹏. ORB安全策略的实现[J]. J4, 1999, 21(5): 56-60.