Simulation based verification of concurrent processing on security devices

Despite the increased use of smartcards in many areas of everyday life the secure interoperability of these devices still remains a significant challenge. Common Criteria certification ensures the secure operation of a particular smartcard in a specific and closed environment and does not explicitly consider potential problems in more open environments where different types of smartcards and their corresponding applications are present at the same time. Since both the range of smartcard applications and the issuing manufacturers continue to grow, the interoperability of smartcards cannot be satisfactorily addressed in an isolated testing and certification environment. Ideally, one should be able to certify that adding a new type of smartcard and a new smartcard application to a such environment is safe without interoperability problems. To conduct this research, we focus on digital signature applications on Common Criteria certified smartcards. We investigated the vulnerabilities of smartcards in such open environments and possible ways to identify and eliminate those using Model Checking approaches. Here we simulate the interaction of many smartcards which interact with their applications via a common middleware. Each smartcard is assumed to execute a Straight Line Program which consists of a series of states or nodes connected by transitions (no loops). We discuss how these results can be taken into account in the design of new types of middleware which can identify and suppress anomalous transitions. These results will help to design systems that support multiple smartcards types and applications simultaneously and securely.