Research On The Multi-COS Isolation And Secure Communication For RF-UCards

Smart cards are becoming widely spread and are typically used for commercial and security-critical applications. With the popularity of card applications, the number of cards increases largely, which results in inconveniency and mistakes because users have to take a lot of cards in their pockets. Moreover, the same smart cards are issued repeatedly, and the most cards held by users are often in sleep. All of these result in the hardware/software resources of cards are duplicated and wasted in most applications. Most existing multi-application smart cards just run the single chip operating system (referred as COS). Due to the applications developed by different providers are mostly compatible with different COSes, the multi-application smart cards are unable to solve the card portability and resource optimization issues perfectly. To address these issues, a novel smart card architecture, namely the Radio Frequency Universal Smart Card (RF-UCard) is proposed. An RF-UCard is a contactless smartcard with multiple chip operating systems and multiple applications environment. The multi-COS architecture and the non-contact communication of RF-UCard will not only solve the card portability and resource optimization issues perfectly, but enable rapid card processing. Unfortunately, these features also raise two considerable security issues: the on-card multi-COS isolation and the radio frequency (RF) communications security.Based on the characteristics of the RF-UCard architecture, various security roles involved in the card's life-cycle are defined, and a multi-level security dependencies model is constructed. According to the state transition path the RF-UCard undergoes in a use-cycle, the RF-UCard run-time k-COS and k-block (memory block) finite state machine (referred as FSM) are established. The run-time security properties are formal defined using the computation tree logic firstly. Then, the proposed FSM models are described using the symbolic model verifier (referred as SMV) specification language, which based on the ordered binary decision diagrams technique. Finally, running the Cadence version SMV to verify the satisfactions of security property on the propose security model. The checking results show that all required security properties are satisfied, and the Cadence SMV is a useful tool for formal verification on the security and the correctness of the RF-UCard run-time model.An isolation mechanism based on the programmable dynamic address bus limits the memory access of the running COS by controlling the high-bit address bus interface with the main CPU. However, since the control parameters used in the address mapping may be tampered, the illegal run-time data access may be occurred. By inspiring from the traditional conference processes, a conference-based isolation model (referred as CIM) that providing strong security isolation between multiple on-card COSes, is proposed. By adding a physical isolated chair memory to host the running COS and its apps, whereas the other idle COSes are stored in another physical memory, the strong isolations are achieved in CIM. The behavioral simulation shows that CIM isolation mechanism can provide a strong run-time isolation environment.Since the openness of the RF channel, a multi-card collision occurs when more than one cards within the reader's read field. An M/G/1/?queueing model for the multi-card identification in a single reader RF-UCard system is built. Based on the queueing model, a detailed mathematical analysis for the distribution of the number of cards, the mean number of cards, and the mean sojourn time needed are given when the system is in stochastic equilibrium. A novel and enhanced algorithm to solve the multi-card collision problems in an RF-UCard system is then proposed. The algorithm was originally inspired from framed ALOHA-based anti-collision algorithms applied in RFID systems. To maximize the system efficiency, a synchronous dynamic adjusting (referred as SDA) scheme that adjusts both the frame size in the reader and the response probability in cards is developed and evaluated. Simulation results show that SDA shows the optimal identification efficiency when the card quantity is more than 100, the arrival rate varies from 0.5 to 2, and the card initial response probability is 0.875 or 1.0. Furthermore, SDA outperforms other ALOHA-based anti-collision algorithms on several performance measures under the same simulation environment.RF-UCard system opens up the possibility for various attacks violating security and privacy due to the openness and the asymmetry of the RF channel. Some strong security requirements are modeled based on the detailed attack analysis. Readers equipped with the same COS may be deployed at different places, and then need different requirements to access the on-card date. So it is preferable to assign a role to each reader and authorize the specific rights. A strong and lightweight role-based mutual authentication (referred as RBMA) protocol that protects security and privacy of RF-UCard systems is proposed. Security analysis shows that RBMA can against most active/passive attacks, which benefiting from its dynamic and random ID update scheme. Performance analysis shows that, RBMA is a secure, efficient, feasible and low-cost authentication protocol.