Research on formal security policy model specification and its formal analysis
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 securit...
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | zho |
| Published: |
Editorial Department of Journal on Communications
2006-01-01
|
| Series: | Tongxin xuebao |
| Subjects: | |
| Online Access: | http://www.joconline.com.cn/zh/article/74661080/ |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1841537347641933824 |
|---|---|
| author | LI Li-ping1 QING Si-han1 ZHOU Zhou-yi1 HE Jian-bo1 WEN Hong-zi3 |
| author_facet | LI Li-ping1 QING Si-han1 ZHOU Zhou-yi1 HE Jian-bo1 WEN Hong-zi3 |
| author_sort | LI Li-ping1 |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-7eb86f294e974c6cad7c1b185dc024c1 |
| institution | Kabale University |
| issn | 1000-436X |
| language | zho |
| publishDate | 2006-01-01 |
| publisher | Editorial Department of Journal on Communications |
| record_format | Article |
| series | Tongxin xuebao |
| spelling | doaj-art-7eb86f294e974c6cad7c1b185dc024c12025-01-14T08:39:02ZzhoEditorial Department of Journal on CommunicationsTongxin xuebao1000-436X2006-01-019410174661080Research on formal security policy model specification and its formal analysisLI Li-ping1QING Si-han1ZHOU Zhou-yi1HE Jian-bo1WEN Hong-zi3Formal 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.http://www.joconline.com.cn/zh/article/74661080/security policy modelformal specificationformal analysistheorem proveBell-LaPadula model |
| spellingShingle | LI Li-ping1 QING Si-han1 ZHOU Zhou-yi1 HE Jian-bo1 WEN Hong-zi3 Research on formal security policy model specification and its formal analysis Tongxin xuebao security policy model formal specification formal analysis theorem prove Bell-LaPadula model |
| title | Research on formal security policy model specification and its formal analysis |
| title_full | Research on formal security policy model specification and its formal analysis |
| title_fullStr | Research on formal security policy model specification and its formal analysis |
| title_full_unstemmed | Research on formal security policy model specification and its formal analysis |
| title_short | Research on formal security policy model specification and its formal analysis |
| title_sort | research on formal security policy model specification and its formal analysis |
| topic | security policy model formal specification formal analysis theorem prove Bell-LaPadula model |
| url | http://www.joconline.com.cn/zh/article/74661080/ |
| work_keys_str_mv | AT liliping1 researchonformalsecuritypolicymodelspecificationanditsformalanalysis AT qingsihan1 researchonformalsecuritypolicymodelspecificationanditsformalanalysis AT zhouzhouyi1 researchonformalsecuritypolicymodelspecificationanditsformalanalysis AT hejianbo1 researchonformalsecuritypolicymodelspecificationanditsformalanalysis AT wenhongzi3 researchonformalsecuritypolicymodelspecificationanditsformalanalysis |