Earticle

초록

영어

The goal of high assurance systems development by formal verification motivates the investigation of techniques whereby a systems design or implementation can be formally shown to satisfy a formal definition of security. The security of unwinding relations provides a proof method that has been applied to establish that a system satisfies noninterference properties, but it requires significant human ingenuity to define an unwinding relation that forms the basis for the proof, and typically also has involved manual driving (proof rule selection) of the theorem proving tool within which the proof is conducted. The property of purge-based definition proposed by Goguen and Meseguer, intransitive purge-based definition proposed by Haigh and Young, and some more definitions TA-secure, TO-secure, ITO-secure proposed by van der Meyden are considered in this paper. The property can be used in the proof of noninterference property without unwinding relations.

목차

Abstract
 1. Introduction
 2. Backgrounds
 3. Some Definitions for the Property
 4. The Property of P, IP, TA, TO, ITO-Secure
 5. Related Work
 6. Conclusion
 ACKNOWLEDGEMENTS
 References

키워드

저자

• Congdong Lv [ School of Computer and Information Technology, Beijing Jiaotong University, Beijing 100044, China ]
• Xiaoyong Li [ School of Computer and Information Technology, Beijing Jiaotong University, Beijing 100044, China ]
• Fei Li [ College of Computer Science and Technology, Zhejiang University, Zhejiang, China ]
• Wei Ma [ School of Computer and Information Technology, Beijing Jiaotong University, Beijing 100044, China ]

참고문헌

발행기관

간행물

표지보기 관심저널 등록

• 간행물명

  International Journal of Hybrid Information Technology

• 간기

  격월간

• pISSN

  1738-9968

• 수록기간

  2008~2016

• 십진분류

  KDC 505 DDC 605