A Verified Formal Specification of A Secured Communication Method For Smart Card Applications

• 발행기관: 적정기술학회
• 저자명: Donald D. Kim
• 간행물 정보: 『적정기술학회지』Vol.7 No.2, 172~187쪽, 전체 16쪽
• 주제분류: 공학 > 기타공학
• 파일형태: PDF
• 발행일자: 2021.11.30

영문 초록

In remote villages without access to modern IT technology, simple devices such as smartcards can be used to carry out business transactions. These devices typically store multiple business applications from multiple vendors. Although devices must prevent malicious or accidental security breaches among the applications, a secure communication channel between two applications from different vendors is often required. In this paper, first, we propose a method of establishing secure communication channels between applications in embedded operating systems that run on multi-applet smart cards. Second, we enforce the high assurance using an intransitive noninterference security policy. Thirdly, we formalize the method through the Z language and create the formal specification of the proposed secure system. Finally, we verify its correctness using Rushby s unwinding theorem.

목차

Introduction

Security Policies

The Unwinding Theorem

Smart Card Entities

Creating a Secure Channel

Formal Verification of the Method

Conclusion

키워드

Formal verification High assurance embedded operating systems Intransitive noninterference security policy Secure communication channels The unwinding theorem Z language