Formal Analysis Of UCard System

The improvement of information economy is important for harmonious society construction. Smartcards makes a great contribution to the information construction of our country. As smartcards are widely being used, the amount of smartcards we are holding grows quickly. But that is very inconvenient for all of us, because we have to bring so many cards. An appropriate way to solve this problem is to implement multi-issue based on multi-application.UCard (Universal Smartcard) is a new kind of smartcard which integrates several independent COSes and applications with different instruction sets, while these COSes and applications are from different issuers. UCard is a perfect solution. We need to bring only a single UCard in our pockets as if we have some conventional cards. More than one issuers are able to execute their issuing operation and write their COSes, applications and data into a UCard. In addition, the security of every COSes is answered for by itself. The physical isolation guarantees that each COS can not access other memory spaces.UCard system consists of tow subsystems, master processor system and coprocessor system. The two subsystems contain hardware and software resource respectively, which make up of the resource set of UCard. The operation set of UCard is composed of inner and outer operations. Actually, UCard owns some features, such as independent security, timing exclusion, inaccessibility, independence etc.UCard has two working states, issuing state and using state. In the process of issuing a card, UCard receives commands from the terminal and finishes some inner operations. At the same time, the states of the master processor system and the coprocessor system change continuously. So we get FSM models for the two subsystems and the state transition diagrams are made. The process of using goes through three steps. The fist step is hardware reconfiguration, the second is transaction processing and the third is quitting and clearing.The architecture of UCard is different from conventional smartcards. It allows more than one software systems consisting of COSes and applications to run on the same hardware platform. So the architecture is reconfigurable. The kernel of reconfigurable architecture is the control data, the control program and the control part. The stability of this architecture includes two ways, one is the completeness and consistency of the control data, the other is the security and stability of the dynamic address bus. There are some approaches to keep the security and stability of dynamic address bus, such as timing query, self-lock circuit and bus address observer.As conventional smartcards do, UCard communicates with the terminal as the international protocol standard ISO/IEC 7816 indicates. A Petri Net model for the reset process of UCard is constructed after analyzing the level states of five points changing in the process of UCard reset.