Abstract:

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.

Key words: bounded constraints, hypersafety, security-relevant properties, deductive proof