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

关键词：限界约束 超安全性 安全策略 推理证明 

单位：中国地质大学北京信息工程学院; 北京100083; 中国科学院软件研究所计算机科学国家重点实验室; 北京100190; 深圳大学计算机与软件学院; 广东深圳518060