The Research Of Formal Verification Application In Office Security

Office is an integrated office kit. Especially as the state, government and PLA's necessary software, Office should have perfect security functions and also important for information security safeguards.PLA helps boost the research of military Office which working on the military security OS at this stage. Owing to the specificity of PLA, Office security is the key parts of the military Office, and how to guarantee the thought of their own safety is very important.To improve the security, we usually take the common way, it only solves the problems on the surface, but it cannot solve completely problems in the deep. Formal verification techniques based on the math consequence, it can smooth differences between theories with practice. So the main idea of the subject is how to construct Office security functions and verify the design.The dissertation research on three aspects: First, we constructed the Office security function kernel which on the basis of BLP, Biba and Clark-Wilson security models and put forward the schemes with a message base of filter framework of reference monitor. Second, researched the Office security base on M-Office and combine with ((The digital signature act of the People' s Republic of China)) and "The National cryptogram administration committee" rules and designed the Office security functions which contain digitalsignature, digitalseal, scriptsignature, certencrypt and designed the Office security functions which measure up to national standard. Third, with the help of formal verification specification language-Z, we verify the coherence of Office security models and the effects, meanwhile, make a method for construct any thought of security application own safety. At last, we summarize the work and further problems.