Model-based testing of network security protocols in Java card applications

Abstract

This research presents a combination of verification and conformance testing techniques for systems that implement network security protocols. We investigate model-based methods for detecting vulnerabilities in network security protocols and testing for correct behavior of Java Card applications in which network security protocols are implemented. The research assumes an open environment which is insecure in which adversaries might try to gain access to restricted resources. We present techniques for model-based testing of network security protocols in Java Card applications and analyse the use and effectiveness of verification in addition to conformance testing in enhancing the quality of a software product. We analyse the use of HLPSL in modelling Kerberos network authentication protocol in an electronic banking (E-Banking) application and also use of promela in modelling behaviour of an electronic passport (EPassport). We present benefits and challenges of performing verification and conformance testing of software application using formal specifications.