J Appropr Technol > Volume 7(2); 2021 > Article
Journal of Appropriate Technology 2021;7(2):172-187.
DOI: https://doi.org/10.37675/jat.2021.7.2.172    Published online November 20, 2021.
A Verified Formal Specification of A Secured Communication Method For Smart Card Applications
Donald D. Kim
Information and Communication Engineering Dept. Dongguk University 
Correspondence:  Donald D. Kim, Email: ddwkim10@dongguk.edu
Received: 22 October 2021   • Revised: 28 October 2021   • Accepted: 28 October 2021
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.
Key Words: Formal verification, High assurance embedded operating systems, Intransitive noninterference security policy, Secure communication channels, The unwinding theorem, Z language
METRICS Graph View
  • 0 Crossref
  •  0 Scopus
  • 40 View
  • 2 Download
Related articles

Editorial Office
1F, 9-ho, 79, Seoun-ro, Seocho-gu, Seoul 06630, Republic of Korea
Tel: +82-2-887-0226    E-mail: editor.ejat@gmail.com                

Copyright © 2021 by Academic Society for Appropriate Technology.

Developed in M2PI

Close layer
prev next