优卡系统的形式化研究.pdf

华中科技大学 硕士学位论文 优卡系统的形式化研究 姓名：冯国平 申请学位级别：硕士 专业：计算机应用技术 指导教师：曹计昌 20060511 华 中 科 技 大 学 硕 士 学 位 论 文 I 摘 要 推进国民经济的信息化是构建和谐社会的重要内容，智能卡的广泛应用为国家 的信息化工作做出了巨大的贡献随着智能卡的广泛应用，个人持有智能卡的种类 和数量增加，造成携带和使用不便提高智能卡便携性的较好解决方法是在“一卡 多用”的基础上实现“一卡多发” 优卡是采用新的软硬件技术在一张卡集成相互独立的现行多张指令相同种类不 同的 COS 及应用的一种新型智能卡优卡很好地解决了智能卡的便携性问题，一张 优卡相当于多张不同的智能卡多个智能卡的发行商都可对同一张优卡进行发卡操 作，写入自己的 COS 以及应用和数据，并且各 COS 的安全性由自己负责优卡内 部的物理隔离保证了各 COS 不能相互访问 优卡系统由主处理器系统和协处理器系统两大部分组成主处理器系统和协处 理器系统分别包括相关的硬件资源和软件资源，二者构成了优卡资源的集合优卡 的操作主要有对内操作和对外操作优卡具有独立安全性、时间互斥性和透明性等。

优卡有两种工作状态，发卡态和用卡态在发卡过程中，优卡接收来自终端的 命令并完成相关的内部操作，相应地，主处理器系统和协处理器系统的状态发生相 应的改变，据此建立了二者的状态机模型，给出了状态转换图优卡的用卡过程包 括硬件重构、交易用卡和退出清理三个阶段 优卡具有与传统智能卡不同的体系结构， 它允许多个 COS 及其应用组成的多软 件系统运行于同一硬件平台优卡的体系结构具有可重构特性实现优卡可重构的 体系结构的核心是控制性数据、控制性程序和控制性部件重构的稳定性包括两个 方面，一是控制性数据的完整性和一致性，另一是保证动态地址总线的安全稳定性 实现动态地址总线的安全稳定性有定时查询的方法以及自锁电路和地址总线信号观 测等方法 优卡与一般智能卡相同，与终端通信进行数据传输仍然采用智能卡协议的国际 标准 ISO/IEC 7816通过分析复位过程中接口的电平状态的变化，建立了复位过程 的 Petri网模型 关键词：智能卡，形式化方法，动态地址总线，重构，安全性，稳定性 华 中 科 技 大 学 硕 士 学 位 论 文 II A b s t r a c t 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 华 中 科 技 大 学 硕 士 学 位 论 文 III 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. K e y W o r d s : Smartcard, Formal Methods, Dynamic Address Bus, Reconfigure, Security, Stability 独创性声明 本人声明所呈交的学位论文是我个人在导师指导下进行的研究工作及取得的 研究成果。

尽我所知，除文中已经标明引用的内容外，本论文不包含任何其他个人 或集体已经发表或撰写过的研究成果对本文的研究做出贡献的个人和集体，均已 在文中以明确方式标明本人完全意识到，本声明的法律结果由本人承担 学位论文作者签名： 日期： 年 月 日 学位论文版权使用授权书 本学位论文作者完全了解学校有关保留、使用学位论文的规定，即：学校有权 保留并向国家有关部门或机构送交论文的复印件和电子版， 允许论文被查阅和借阅 本人授权华中科技大学可以将本学位论文的全部或部分内容编入有关数据库进行检 索，可以采用影印、缩印或扫描等复制手段保存和汇编本学位论文 保密□ ，在_____年解密后适用本授权书 不保密□ （请在以上方框内打“√” ） 学位论文作者签名： 指导教师签名： 日期： 年 月 日 日期： 年 月 日 本 论 文 华 中 科 技 大 学 硕 士 学 位 论 文 1 1 绪 论 1 . 1 课题背景、目的及意义 推进国民经济的信息化是构建和谐社会的重要内容，IC 卡技术与应用是国家信 息化工作的一个重要组成部分。

近十几年来，IC 技术得到了长足的发展，在世界各 国得到广泛应用 IC 卡（Integrated Circuit Card） ，又称作集成电路卡或者智能卡（Smart Card） ， 它是将集成电路芯片嵌于塑料基片上，封装成卡的形式，其核心技术是卡用芯片技 术根据卡中集成电路芯片的不同，可将智能卡分为两类：一是存储卡，卡中含有 半导体存储单元，通常是 EEPROM，这种类型的智能卡只能作存储数据之用，其中 的数据供外部设备读取，它本身没有计算能力另一种是 CPU 卡，卡中的集成电路 包括CPU、 EEPROM、 RAM 以及固化在 ROM中的片内操作系统COS （Chip Operating System） CPU 卡具有一定的信息处理能力，实际上就相当于一台微型计算机，它 与存储卡相比具有更强的功能和更高的安全性在后文中，如未说。