Formal method is one of the kernel technologies of developing high security level computer system.But by current formal development method

assurance of security policy model correctness cannot be provided directly using machine proof which is stricter than manual proof

correspondence between security policy model and security functional specification is also hard to achieve.To solve these problems

a new and effective method was proposed for specification constructing and proving by extending the specification technique of security functional specification into the specifica-tion of security policy model.Also

BLP model was specified and analyzed as an example.