射频优卡多芯片操作系统隔离与安全通信方法研究
|
摘要
智能卡作为个人数据载体已广泛应用于生产生活中的各个领域。随着应用的普及，智能卡发行数量剧增，导致单个用户卡携带不便和卡资源管理的复杂。同时，智能卡的多次重复发行，且用户手中大部分智能卡大部分时间处于非工作状态，导致卡软硬件资源的重复配置与闲置浪费。由于现行多应用智能卡只支持单个芯片操作系统(Chip Operating System，简称COS)，不同COS所支持的卡应用程序间存在不兼容性，故多应用智能卡未能有效解决传统智能卡的便携性和资源闲置浪费问题。射频优卡的出现为上述问题的解决提供一个很好的技术思路。射频优卡在体系结构上集成相互独立的现行多个COS及应用；在通信接口上采用射频实现非接触通信。这些特点使得射频优卡在有效解决日益严峻的多卡携带问题，优化卡资源利用的同时，提供卡应用的快速自动处理。但同时，射频优卡的多操作系统架构及无线信道通信，引发了两大关键安全问题：卡内的多COS安全隔离与卡外的射频通信安全。
基于射频优卡体系结构特点，分析其生命周期中涉及的各种安全角色，建立多级安全依赖关系。根据每次用卡中的状态转移路径，建立运行时k-COS和k-block(存储块)的有限状态机模型。采用计算树逻辑语言对运行时安全属性进行形式化定义；使用基于有序二元决策图的符号模型验证规范语言对有限状态机模型进行系统说明：运行符号模型验证器检验安全模型对于安全属性的满足性。验证结果表明，多COS射频优卡运行时有限状态机模型满足运行时三大安全属性，并表明符号模型验证对于COS数量小于10的射频优卡运行时安全模型是一种可行的形式化验证方法。
基于可编程动态地址总线的隔离机制通过对主CPU部分地址总线进行控制来限制运行COS的存储访问。由于地址映射控制参数可能遭受非法篡改，该机制可能出现运行时的非法数据访问。从现实生活中会议的组织模式得到启发，提出一种基于席位约束会议模型的隔离机制，该机制在射频优卡的硬件层增加一个类似于会议中主席台的专用主席台存储器来存储运行COS所需的代码与数据。与可编程动态地址总线隔离机制不同，会议模型隔离机制不需对主CPU的地址总线做任何限制，而由主席台存储器提供一个隔离域来限制运行COS的存储访问。由于主席台存储器的易失性，且与其它存储器在物理上是隔离的，从而保证运行COS与其它COS的完全隔离。功能仿真表明，会议模型隔离机制能够提供很好的运行时安全隔离环境。
射频优卡系统由于射频信道的开放性，在链路层上存在多卡冲突问题。基于对单读写器系统卡输入过程、服务时间分布和服务规则的分析，建立多卡识别过程的排队模型，对系统达到统计平衡状态下读写器识别范围内卡的概率分布、平均卡数及卡的平均逗留时间进行数学分析。借鉴已有算法中的帧长及卡应答概率调整策略，设计一种双边同步动态调整SDA(Synchronous Dynamic Adjusting)算法。SDA根据上一轮阅读循环的冲突状况，在读写器和射频优卡双边分别调整帧长和应答概率。软件仿真表明，当服务卡数大于100时，若卡平均到达率在0．5与2之间变化，卡初始应答概率为0．875或1．0时，SDA算法将达到最优识别率。在相同的仿真条件下，SDA总的服务时间、卡的平均逗留时间和识别率均优于两种典型的射频识别系统多标签冲突解决算法。
射频优卡系统由于信道的开放性和非对称性，在实际应用环境中会受到各种可能的攻击。基于对攻击的分析，提出射频优卡系统应用层的安全需求；基于读写器角色分配与授权，设计一种双向认证保护协议。协议采用动态身份更新机制防止重发攻击和位置跟踪；采用单向哈希函数防止数据侦听和向前递推分析攻击；采用会话密钥备份机制防止数据异步攻击；采用读写器访问权限检测防止合法读写器的非授权数据访问。性能分析表明，所设计的协议是一种安全、高效、低成本、易实现的安全认证协议。
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.
基于射频优卡体系结构特点，分析其生命周期中涉及的各种安全角色，建立多级安全依赖关系。根据每次用卡中的状态转移路径，建立运行时k-COS和k-block(存储块)的有限状态机模型。采用计算树逻辑语言对运行时安全属性进行形式化定义；使用基于有序二元决策图的符号模型验证规范语言对有限状态机模型进行系统说明：运行符号模型验证器检验安全模型对于安全属性的满足性。验证结果表明，多COS射频优卡运行时有限状态机模型满足运行时三大安全属性，并表明符号模型验证对于COS数量小于10的射频优卡运行时安全模型是一种可行的形式化验证方法。
基于可编程动态地址总线的隔离机制通过对主CPU部分地址总线进行控制来限制运行COS的存储访问。由于地址映射控制参数可能遭受非法篡改，该机制可能出现运行时的非法数据访问。从现实生活中会议的组织模式得到启发，提出一种基于席位约束会议模型的隔离机制，该机制在射频优卡的硬件层增加一个类似于会议中主席台的专用主席台存储器来存储运行COS所需的代码与数据。与可编程动态地址总线隔离机制不同，会议模型隔离机制不需对主CPU的地址总线做任何限制，而由主席台存储器提供一个隔离域来限制运行COS的存储访问。由于主席台存储器的易失性，且与其它存储器在物理上是隔离的，从而保证运行COS与其它COS的完全隔离。功能仿真表明，会议模型隔离机制能够提供很好的运行时安全隔离环境。
射频优卡系统由于射频信道的开放性，在链路层上存在多卡冲突问题。基于对单读写器系统卡输入过程、服务时间分布和服务规则的分析，建立多卡识别过程的排队模型，对系统达到统计平衡状态下读写器识别范围内卡的概率分布、平均卡数及卡的平均逗留时间进行数学分析。借鉴已有算法中的帧长及卡应答概率调整策略，设计一种双边同步动态调整SDA(Synchronous Dynamic Adjusting)算法。SDA根据上一轮阅读循环的冲突状况，在读写器和射频优卡双边分别调整帧长和应答概率。软件仿真表明，当服务卡数大于100时，若卡平均到达率在0．5与2之间变化，卡初始应答概率为0．875或1．0时，SDA算法将达到最优识别率。在相同的仿真条件下，SDA总的服务时间、卡的平均逗留时间和识别率均优于两种典型的射频识别系统多标签冲突解决算法。
射频优卡系统由于信道的开放性和非对称性，在实际应用环境中会受到各种可能的攻击。基于对攻击的分析，提出射频优卡系统应用层的安全需求；基于读写器角色分配与授权，设计一种双向认证保护协议。协议采用动态身份更新机制防止重发攻击和位置跟踪；采用单向哈希函数防止数据侦听和向前递推分析攻击；采用会话密钥备份机制防止数据异步攻击；采用读写器访问权限检测防止合法读写器的非授权数据访问。性能分析表明，所设计的协议是一种安全、高效、低成本、易实现的安全认证协议。
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.
引文
[1]Z.Q.Chen.Java Card~(TM) Technology for Smart Cards:Architecture and Programmer's Guide (The Java Series).New Jersey:Prentice Hall PTR,2000.29～38
[2]T.F.Massey.MULTOS - The High Security Smart Card OS:[Whitepaper].MAOSCO,Inc.,2005.URL:http://www.multos.com/downloads/marketing/Whitepaper MULTOS_ Security.pdf
[3]曹计昌，邱鹏，张斌．UCard中动态地址映射的实现方法研究．计算机工程与科学，2006，28(1)：119～121，134
[4]Intemational Organization for Standardization.ISO/IEC 10536-3:Identification cards -- Contactless integrated circuit(s) cards,Part 3:Electronic signals and reset procedures.Published standard,1996
[5]International Organization for Standardization.ISO/IEC 14443-4:Identification cards -- Contactless integrated circuit cards -- Proximity cards,Part 4:Transmission protocol.Published standard,2008
[6]International Organization for Standardization.ISO/IEC 15693-3:Identification cards -- Contactless integrated circuit(s) cards,Part 3:Anticollision and transmission protocol.Published standard,2001
[7]J.-J.Vandewalle.Smart Card Research Perspectives.In:Proceedings of International Workshop on Construction and Analysis of Safe,Secure,and Interop.erable Smart Devices.Berlin / Heidelberg:Springer-Verlag,2005.250～256
[8]J.H.Saltzer,M.D.Schroeder.The protection of information in computer systems.Proceedings of the IEEE,1975,63(9):1278～1308
[9]J.E.Smith,R.Nair.The Architecture of Virtual Machines.Computer,2005,38(5):32～38
[10]VMware Inc.Security Design of the VMware Infrastructure 3 Architecture:[Technology White Paper].URL:http://www.vmware.com/pdf/vi3_security_architecture_wp.pdf,Feb.2007
[11]A.Whitaker,M.Shaw,S.D.Gribble.Denali:Lightweight Virtual Machines for Distributed and Networked Applications.Technical Report 02-02-01,University of Washington,2002
[12]A.Whitaker,M.Shaw,S.D.Gribble.Scale and performance in the Denali isolation kernel. In: Proceedings of the 5th Symposium on Operating Systems Design and Implementation. New York: ACM Press, 2002. 195-210
[13] P. Barham, B. Dragovic and K. Fraser. Xen and the art of virtualization. In: Proceedings of the 19th ACM Symposium on Operating Systems Principles. New York: ACM Press, 2003. 164-177
[14] D. Lie, C. Thekkath, M. Mitchell, et al. Architectural support for copy and tamper resistant software. In: Proceedings of the International Conference on Architectural Support for Programming Languages and Operating Systems. New York: ACM Press, 2000. 168-177
[15] D. Lie, M. Mitchell, C. Thekkath, et al. Specifying and Verifying Hardware for Tamper-Resistant Software. In: Proceedings of the 2003 IEEE Symposium on Security and Privacy. Washington, DC: IEEE, 2003. 166-177
[16] D. Lie, C. Thekkath, M. Horowitz, et al. Implementing an untrusted operating system on trusted hardware. In: Proceedings of the nineteenth ACM symposium on Operating systems principles. New York: ACM Press, 2003. 178-192
[17] B. Gassend, G E. Suh, D. Clarke, et al. Caches and Hash Trees for Efficient Memory Integrity Verification. In: Proceedings of the 9th International Symposium on High-Performance Computer Architecture. Washington, DC: IEEE, 2003. 295-306
[18] W. Shi, H. S. Lee, M. Ghosh, et al. High Efficiency Counter Mode Security Architecture via Prediction and Precomputation. In: Proceedings of the 32nd International Symposium on Computer Architecture. Washington, DC: IEEE, 2005. 14-24
[19] C. Lu, T. Zhang, W. Shi, et al. M-TREE: A High Efficiency Security Architecture for Protecting Integrity and Privacy of Software. Journal of Parallel and Distributed Computing for a special issue on Security in Grid and Distributed Systems, 2006, 66(9): 1116-1128
[20] G E. Suh, D. Clarke, B. Gassend, et al. AEGIS: Architecture for Tamper-Evident and Tamper-Resistant Processing. In: Proceedings of the 17th annual international conference on Supercomputing. New York: ACM Press, 2003. 160-171
[21] G E. Suh, C. W. O'Donnell, S. Devadas. Aegis: A Single-Chip Secure Processor. IEEE Design & Test, 2007,24(6): 570-580
[22] J. Rushby. Design and verification of secure systems. In: Proceedings of the 8th Symposium on Operating System Principles. New York: ACM Press, 1981. 12-21
[23] E. J. Koldinger, J. S. Chase, S. J. Eggers. Architectural support for single address space operating systems. ACM SIGPLAN Notices, 1992, 27(9): 175-186
[24] M. Swift, B. Bershad, H. Levy. Improving the Reliability of Commodity Operating Systems. In: Proceedings of the 19th ACM Symposium on Operating Systems Principles. New York: ACM Press, 2003. 207-222
[25] E. Witchel, J. Rhee, K. Asanovic. Mondrix: Memory Isolation for Linux using Mondriaan Memory Protection. In: Proceedings of the 20th ACM Symposium on Operating Systems Principles. New York: ACM Press, 2005. 31-44
[26] E. Witchel, J. Cates, K. Asanovic. Mondrian memory protection. In: Proceedings of the Tenth International Conference on Architectural Support for Programming Languages and Operating Systems. New York: ACM Press, 2002. 304-316
[27] S. Jain, F. Shafique, V. Djeric, et al. Application-level isolation and recovery with solitude. ACM SIGOPS Operating Systems Review, 2008,42(4): 95-107
[28] U. Erlingsson, M. Abadi, M. Vrable, et al. XFI: Software Guards for System Address Spaces. In: Proceedings of the 7th Symposium on Operating Systems Design and Implementation. Berkeley: USENIX Association, 2006. 75-88
[29] N. Aggarwal, P. Ranganathan, N. P. Jouppi, et al. Configurable Isolation: Building High Availability Systems with Commodity Multi-Core Processors. In: Proceedings of the 34th annual international symposium on Computer architecture. New York: ACM Press, 2007. 470-481
[30] I. B. Ganev. A Pliable Hybrid Architecture for Code Isolation: [PhD thesis]. Georgia Institute of Technology, 2007
[31] C. Minh, M. Trautmann, J. Chung, et al. An effective hybrid transactional memory system with strong isolation guarantees. In: Proceedings of the 34th annual international symposium on Computer architecture. New York: ACM Press, 2007. 69-80
[32] T. Shpeisman, V. Menon, A. Tabatabai, et al. Enforcing isolation and ordering in STM. In: Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation. New York: ACM Press, 2007. 78-88
[33] D. Elkaduwe, P. Derrin, K. Elphinstone. Kernel design for isolation and assurance of physical memory. In: Proceedings of the 1st workshop on Isolation and integration in embedded systems. New York: ACM Press, 2008. 35-40
[34] T. Huffmire, B. Brotherton, G Wang, et al. Moats and Drawbridges: An Isolation Primitive for Reconfigurable Hardware Based Systems. In: Proceedings of the 2007 IEEE Symposium on Security and Privacy.Washington,DC:IEEE,2007.281～295
[35]温研，王怀民．基于本地虚拟化技术的隔离执行模型研究．计算机学报，2008，31(10)：1768～1779
[36]王小光，夏克俭，张焕生．虚拟机中关于内存保护的故障隔离技术研究．计算机工程与设计，2008，29(16)：4315～4318
[37]Xue Haifeng,Qing Sihan,Zhang Huanguo.XEN Virtual Machine Technology and Its Security Analysis.Wuhan University Journal of Natural Sciences,2007,12(1):159～162
[38]吴新勇．嵌入式操作系统安全保障技术研究：[博士学位论文]．四川成都：电子科技大学，2003
[39]Global Platform.Open Platform Card Specification.Version 2.2.March 2006.URL:http://www.globalplatform.org
[40]Common Criteria.Common Criteria for Information Technology Security Evaluation (CC),Version 2.1,ISO/IEC 15408,August 1999
[41]French Certification Body PP/0010.Protection Profile Smart Card IC with Multi-Application Secure Platform,version 2.0,Eurosmart,November 2000.URL:http://www.commoncriteriaportal.org/public/files/ppfiles/PP0010.pdf
[42]J.P.Tual.MASSC:A Generic Architecture for Multiapplication Smart Cards.IEEE Micro,1999,19(5):52～61
[43]P.Girard.Which security policy for multiapplication smart cards.In:Proceedings of the USENIX Workshop on Smartcard Technology.Berkeley:USENIX Association,1999.21～28
[44]G Schellhorn,W.Reif,A.Schairer,et al.Verified formal security models for multiapplicative smart cards.Journal of Computer Security,2002,10(4):339～367
[45]I.Bakdi.Towards a Secure and Practical Multifunctional Smart Card.In:Proceedings of the 7th IFIP WG 8.8/11.2 International Conference on Smart Card Research and Advanced Applications.Berlin / Heidelberg:Springer-Verlag,2006.16～31
[46]G.Barthe,G.Dufay.Formal Methods for Smartcard Security.Foundations of Security Analysis and Design Ⅲ,2005,3655:133～177
[47]M.Witteman.Java card security.Information Security Bulletin,2003,8:291～298
[48]K.Markantonakis,K.Mayes,M.Tunstall,et al.Smart Card Security.Studies in Computational Intelligence, 2007, 57(2007): 201-233
[49] W. Mostowski, E. Poll. Malicious Code on Java Card Smartcards: Attacks and Countermeasures. In: Proceedings of the 8th IFIP WG 8.8/11.2 international conference on Smart Card Research and Advanced Applications. Berlin / Heidelberg: Springer-Verlag, 2008. 1-16
[50] Sun Microsystems, Inc. Java Card Platform Specification. Version 3.0. March 2008. URL: http://java.sun.com/javacard/3.0/specs.jsp
[51] X. Leroy. Java Bytecode Verification: Algorithms and Formalizations. Journal of Automated Reasoning, 2003, 30(3-4): 235-269
[52] D. Basin, S. Friedrich, M. Gawkowski. Bytecode Verification by Model Checking. Journal of Automated Reasoning, 2003, 30(3-4): 399-444
[53] Sun Microsystems, Inc. The Runtime Environment Specification for the Java Card ~(TM)Platform, Classic Edition, Version 3.0,2008
[54] M. Montgomery, K. Krishna. Secure object sharing in Java Card. In: Proceedings of the USENIX Workshop on Smartcard Technology. Berkeley: USENIX Association, 1999. 119-127
[55] W. Mostowski, E. Poll. Testing the Java Card Applet Firewall. Technical Report: ICIS-R07029, Radboud University Nijmegen. December 2007. URL: https://pms.cs.ru.nl/iris-diglib/src/icis tech reports.php
[56] W. Mostowski, E. Poll. Java Card Applet Firewall Exploration and Exploitation. In: Proceedings of the e-Smart 2008, Brussels: Eurosmart, 2008. 1-4
[57] W. Dietl, P. M(?)ller, A. Poetzsch-Heffter. A type system for checking applet isolation in Java Card. In: Proceedings of the International Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart devices. Berlin / Heidelberg: Springer-Verlag, 2004.129-150
[58] D. Ghindici, I. Simplot-Ryl. On Practical Information Flow Policies for Java-Enabled Multiapplication Smart Cards. In: Proceedings of the 8th IFIP WG 8.8/11.2 international conference on Smart Card Research and Advanced Applications. Berlin / Heidelberg: Springer-Verlag, 2008. 32-47
[59] P. Bieber, J. Cazin, P. Girard, et al. Checking secure interactions of smart card applets: extended version. Journal of Computer Security, 2002, 10(4): 369-398
[60] J. Andronick, B. Chetali, O. Ly. Using Coq to Verify Java Card Applet Isolation Properties. Theorem Proving in Higher Order Logics, 2003, 2758: 335-351
[61] M. Eluard, T. Jensen. Secure object flow analysis for Java card. In: Proceedings of the 5th conference on Smart Card Research and Advanced Application Conference.Berkeley:USENIX Association,2002.97～110
[62]M.(?)luard,T.Jensen.An operational semantics of the Java Card firewall.In:Proceedings of the International Conference on Research in Smart Cards:Smart Card Programming and Security.London:Springer-Verlag,2001.95～110
[63]P.Ferrara,Jail:Firewall analysis of java card by abstract interpretation.In:Proceedings of the 1 st International Workshop on Emerging Applications of Abstract Interpretation.Amsterdam:Elsevier Science Publishers B.V.,2006.1～15
[64]W.Mostowski.Formalisation and Verification of Java Card Security Properties in Dynamic Logic.In:Proceedings of the 8th International Conference on Fundamental Approaches to Software Engineering.Berlin / Heidelberg:Springer-Verlag,2005.357～371
[65]V.Almaliotis,A.Loizidis,P.Katsaros.Static Program Analysis for Java Card Applets.In:Proceedings of the 8th IFIP WG 8.8/11.2 international conference on Smart Card Research and Advanced Applications.Berlin / Heidelberg:Springer-Verlag,2008.17～31
[66]刘玉珍，张焕国．多应用安全智能卡结构的研究．武汉大学学报(理学版)，2006，52(1)：87～92
[67]董威，杨义先．一种跨行业多应用智能卡系统模型及实现．计算机工程，2007，23(8)：230～232
[68]王同洋，秦保安，吴俊军．一卡多用安全管理平台．计算机应用，2005，25(1)：154～157
[69]吴俊军，罗标．“一卡多用”中卡操作系统多应用管理的设计．计算机应用与软件，2006，23(8)：68～71
[70]胥怡心，张其善，刘建伟．Java卡的可信代码装载机制设计．北京航空航天大学学报，2009，35(1)：32～35
[71]吴俊军，马鑫龙，张新访．一种新的Java智能卡上字节码校验算法．计算机工程与科学，2008，30(3)：65～68
[72]吴俊军，马鑫龙．一种使用CFT的Java卡内字节码校验算法．小型微型计算机系统，2008，29(12)：2360～2364
[73]向文，韩晶，吴俊军．基于混合模式的Java卡字节码优化器．计算机工程与科学，2008，30(7)：155～158
[74] D-H. Shih, P.-L. Sun, D. C. Yen, et al. Taxonomy and survey of RFID anti-collision protocols. Computer Communications, 2006,29(11): 2150-2166
[75] N. Abramson. The ALOHA system - Another alternative for computer communication. In: Proceedings of the FIPS Fall Joint Computer Conference. Gaithersburg: Information Technology Laboratory, NIST, 1970. 281-285
[76] L. G Roberts. ALOHA packet system with and without slots and capture. Computer Communications Review, 1975, 5(2): 28-42
[77] F. C. Schoute. Control of ALOHA Signalling in a Mobile Radio Trunking System. In: Proceedings of the International Conference on Radio Spectrum Conservation Techniques. London: Institution of Electrical Engineers, 1980. 38-42
[78] F. C. Schoute. Dynamic Frame Length ALOHA. IEEE Transactions on Communications, 1983, 31(4): 565-568
[79] H. Vogt. Efficient Object Identification with Passive RFID Tags. In: Proceedings of the First International Conference on Pervasive Computing. London: Springer-Verlag, 2002. 98-113
[80] J. Zhai, G.-N. Wang. An Anti-collision Algorithm Using Two-Functioned Estimation for RFID Tags. In: Proceedings of the Int'l Conf. Computational Science and its Applications, Berlin / Heidelberg: Springer-Verlag, 2005. 702-711
[81] W.-T. Chen, G-H. Lin. An Efficient Anti-Collision Method for Tag Identification in a RFID System. IEICE Transactions on Communications, 2006, E89-B(12): 3386-3392
[82] S.-R. Lee, S.-D. Joo, C.-W. Lee. An Enhanced Dynamic Framed Slotted ALOHA Algorithm for RFID Tag Identification. In: Proceedings of the 2nd Annual International Conference on Mobile and Ubiquitous Systems: Networking and Services, 2005. 166-172
[83] J.-R. Cha, J.-H. Kim. Novel Anti-collision Algorithms for Fast Object Identification in RFID System. In: Proceedings of the 11th International Conference on Parallel and Distributed Systems, 2005. 63-67
[84] T.-W. Hwang, B.-G Lee, Y. S. Kim, et al. Improved Anti-collision Scheme for High Speed Identification in RFID System. In: Proceedings of the First International Conference on Innovative Computing, Information and Control, 2006. 449-452
[85] K. Ali, H. Hassanein, A. M. Taha. RFID Anti-collision Protocol for Dense Passive Tag Environments. In: Proceedings of the 32nd IEEE Conference on Local Computer Networks. Washington, DC: IEEE, 2007. 819-824
[86]王建伟，赵玉萍，T．Korhonen．RFID系统防碰撞协议研究——设计与优化．电子与信息学报，2009，3 1(1)：1～4
[87]耿淑琴，高大明，汪金辉．射频识别系统中自适应反碰撞法的实现．北京邮电大学学报，2008，3 1(6)：76～79
[88]王晓华，周晓光，孙百生．射频识别系统中的防碰撞算法设计．北京邮电大学学报，2008，30(2)：59～62
[89]S.-S.Yu,Y.Zhan,Y.-h.Wang.RFID Anti-collision algorithm Based on Bi-directional Binary Exponential Index.In:Proceedings the IEEE International Conference on Automation and Logistics.Washington,DC:IEEE,2007.2917～2921
[90]梁彪，胡爱群，秦中元．一种新的RFID防碰撞算法设计．电子与信息学报，2007，29(9)：2158～2160
[91]J.I.Capetanakis.Tree algorithms for packet broadcast channels.IEEE Transactions on Information Theory,1979,25(5):505～515
[92]K.Finkenzeller,RFID Handbook:Fundamentals and Applications in Contactless Smart Cards and Identification (2nd Edition).New York,NY,USA:John Wiley & Sons,Inc.,2003.168～192
[93]S.S.Kim,Y.H.Kim,S.J.Lee,et al.An Improved Anti Collision Algorithm using Parity Bit in RFID System.In:Proceedings of the Seventh IEEE International Symposium on Network Computing and Applications.Washington,DC:IEEE,2008.224～227
[94]H.J.Yeo,Y.H.Kim,H.Y.Lim,et al.ID Prediction Algorithm for Tag Collision Arbitration in RFID System.In:Proceedings of the 13th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications.Washington,DC:IEEE,2007.476～481
[95]C.Law,K.Lee,K.-Y.Siu.Efficient memoryless protocol for tag identification (extended abstract).In:Proceedings of the 4th International Workshop on Discrete Algorithms and Methods for Mobile Computing and Communications.New York:ACM Press,2000.75～84
[96]H.Lee,J.Kim.QT-CBP:A New RFID Tag Anti-collision Algorithm Using Collision Bit Positioning.In:Proceedings of the Workshops on Emerging Directions in Embedded and Ubiquitous Computing.Berlin / Heidelberg:Springer-Verlag,2006.591～600
[97] A. Juels, R. L. Rivest, M. Szydlo. The blocker tag: selective blocking of RFID tags for consumer privacy. In: Proceedings of the 10th ACM conference on Computer and communications security. New York: ACM Press, 2003. 103-111
[98] M. Jacomet, A. Ehrsam, U. Gehrig. Contactless Identification Device with Anticollision Algorithm. In: Proceedings of IEEE Conference on Circuits, System, Computers and Communications. Washington, DC: IEEE, 1999. 4-8
[99] H.-S. Choi, J.-R. Cha, J.-H. Kim. Fast wireless anti-collision algorithm in ubiquitous ID system. In: Proceedings of IEEE 60th Vehicular Technology Conference. Washington, DC: IEEE, 2004. 4589-4592
[100] J. H. Choi, D. Lee, Y. Youn, et al. Scanning-Based Pre-Processing for Enhanced Tag Anti-Collision Protocols. In: Proceedings of the 2006 International Symposium on Communications and Information Technologies. Washington, DC: IEEE, 2006. 1207-1211
[101] J. Myung, W. Lee. Adaptive Binary Splitting: A RFID Tag Collision Arbitration Protocol for Tag Identification. Mobile Networks and Applications, 2006,11(5): 711-722
[102] J. Myung, W. Lee, J. Srivastava, et al. Tag-Splitting: Adaptive Collision Arbitration Protocols for RFID Tag Identification. IEEE Transactions on Parallel and Distributed Systems, 2007,18(6): 763-775
[103] J. Myung, W. Lee. Adaptive splitting protocols for RFID tag collision arbitration. In: Proceedings of the 7th ACM international symposium on Mobile ad hoc networking and computing. New York: ACM Press, 2006. 202-213
[104] J. Myung, W. Lee, T. K. Shih. An adaptive memoryless protocol for RFID tag collision arbitration. IEEE transactions on multimedia, 2006, 8(5): 1096-1101
[105] X. Huang, D. Tran. Adaptive Binary Splitting for a RFID Tag Collision Arbitration Via Multi-agent Systems. In: Proceedings of the 11th International Conference on Knowledge-Based Intelligent Information and Engineering Systems. Berlin / Heidelberg: Springer-Verlag, 2007. 926-933
[106] J. H. Choi, D. Lee, H. Jeon, et al. Enhanced Binary Search with Time-Divided Responses for Efficient RFID Tag Anti-Collision. In: Proceedings of the IEEE International Conference on Communications. Washington, DC: IEEE, 2007. 3853-3858
[107] H.-S. Choi, J.-H. Kim. Anti-collision algorithm using Bin slot in RFID System. In: Proceedings of the IEEE Region 10 Conference on TENCON. Washington, DC: IEEE,2005.1～6
[108]J.-Y.Kim,B.-S.Kang,J.-W.Jwa,et al.Bin-slotted Hybrid Search Algorithm for Multiple RFID Arbitration.In:Proceedings of the 2006 International Conference on Wireless Networks.Las Vegas:CSREA Press,2006.164～172
[109]C.-H.Quan,W.-K.Hong,H.-C.Kim.Performance Analysis of Tag Anti-collision Algorithms for RFID Systems.In:Proceedings of the 2006 Workshops on Emerging Directions in Embedded and Ubiquitous Computing.Berlin / Heidelberg:Springer-Verlag,2006.382～391
[110]W.-T.Chen.Performance Comparison of Binary Search Tree and Framed ALOHA Algorithms for RFID Anti-Collision.IEICE Transactions on Communications,2008,E91-B(4):1168～1171
[111]余松森，詹宜巨，彭卫东等．基于后退式索引的二进制树形搜索反碰撞算法及其实现．计算机工程与应用，2004(16)：26～28
[112]余松森，詹宜巨，王志平等．跳跃式动态树形反碰撞算法及其分析．计算机程，2005，31(9)：19～20，26
[113]余松森，詹宜巨．基于修剪枝的二进制树形搜索反碰撞算法与实现．计算机工程，2005，31(16)：217～218，230
[114]谢振华，赖声礼，陈鹏．RFID技术和防冲撞算法．计算机工程与应用，2007，43(6)：223～225
[115]B.Feng,J.-T.Li,J.-B.Guo,et al.ID-Binary Tree Stack Anticollision Algorithm for RFID.In:Proceedings of the 11th IEEE Symposium on Computers and Communications.Washington,DC:IEEE,2006.207～212
[116]冯波，李锦涛，郑为民等．一种新的RFID标签识别防冲突算法．自动化学报，2008，34(6)：632～638
[117]K.W.Chiang,C.Hua,T.P.Yum.Prefix-Randomized Query-Tree Protocol for RFID Systems.In:Proceedings of the 11th IEEE Symposium on Computers and Communications.Washington,DC:IEEE,2006.1653～1657
[118]焦传海，王可人．多枝查询树协议在解决射频识别碰撞问题中的应用．电讯技术，2008，48(3)：95～99
[119]赵曦，张有光．一种新颖的RFID多标签防碰撞算法．北京航空航天大学学报，2008，34(13)：276～279
[120]S.E.Sarma,S.A.Weis,D.W.Engels.RFID Systems and Security and Privacy Implications.In:Proceedings of the 4th International Workshop on Cryptographic Hardware and Embedded Systems. London: Springer-Verlag, 2002. 454-469
[121] A. Juels. RFID Security and Privacy: A Research Survey. Journal of Selected Areas in Communication (J-SAC), 2006,24(2): 381-395
[122] G Avoine. RFID Security & Privacy Lounge. URL: http://www.avoine.net/rfid/, 2009
[123] A. Juels. Minimalist cryptography for low-cost RFID tags. In: Proceedings of the 4th International Conference on Security in Communication Networks. Berlin / Heidelberg: Springer-Verlag, 2004. 149-164
[124] D. Molnar, A. Soppera, D. Wagner. A Scalable, Delegatable Pseudonym Protocol Enabling Ownership Transfer of RFID Tags. In: Proceedings of the 12th International Workshop on Selected Areas in Cryptography. Berlin / Heidelberg: Springer-Verlag, 2006. 276-290
[125] G Avoine. Adversarial Model for Radio Frequency Identification. Technical Report, LASECREPORT-2005-001, Swiss Federal Institute of Technology (EPFL), Security and Cryptography Laboratory (LASEC), Lausanne, Switzerland, 2005
[126] G Avoine, P. Oechslin. RFID Traceability: A Multilayer Problem. In: Proceedings of the 9th International Conference on Financial Cryptography and Data Security. Berlin / Heidelberg: Springer-Verlag, 2005. 125-140
[127] X. L. Zhang, B. King. Modeling RFID Security. In: Proceedings of the First SKLOIS Conference on Information Security and Cryptology. Berlin / Heidelberg: Springer-Verlag, 2005. 75-90
[128] S. Vaudenay, On Privacy Models for RFID. In: Proceedings of the 13th International Conference on the Theory and Application of Cryptology and Information Security. Berlin / Heidelberg: Springer-Verlag, 2008. 68-87
[129] MIT Auto-ID Center. 860MHz-960MHz Class I Radio Frequency Identification Tag Radio Frequency & Logical communication Interface Specification Proposed Recommendation Version 1.0.0. Technical Report MIT AUTO ID-TR-007, 2002
[130] S.-C. Kim, S.-S. Yeo, S. K. Kim. MARP: Mobile Agent for RFID Privacy Protection. In: Proceedings of the 7th IFIP WG 8.8/11.2 International Conference on Smart Card Research and Advanced Applications. Berlin / Heidelberg: Springer-Verlag, 2006. 300-312
[131] S.-S. Yeo, S.-C. Kim, S. K. Kim. eMARP: Enhanced Mobile Agent for RFID Privacy Protection and Forgery Detection. In: Proceedings of the First KES International Symposium on Agent and Multi-Agent Systems: Technologies and Applications. Berlin / Heidelberg: Springer-Verlag, 2007. 318-327
[132] A. Juels, J. Brainard. Soft Blocking: Flexible Blocker Tags on the Cheap. In: Proceedings of the 2004 ACM workshop on Privacy in the electronic society. New York: ACM Press, 2004. 1-7
[133] M. Rieback, B. Crispo, A. Tanenbaum. Keep on Blockin' in the Free World: Personal Access Control for Low-Cost RFID Tags. In: Proceedings of the 13th International Workshop on Security Protocols. Berlin / Heidelberg: Springer-Verlag, 2005. 51-59
[134] M. Feldhofer, S. Dominikus, J. Wolkerstorfer. Strong Authentication for RFID Systems Using the AES Algorithm. In: Proceedings of the 6th International Workshop on Cryptographic Hardware and Embedded Systems. Berlin / Heidelberg: Springer-Verlag, 2004. 357-370
[135] M. Kim, J. Ryou, Y. Choi. Low Power AES Hardware Architecture for Radio Frequency Identification. In: Proceedings of the First International Workshop on Security. Berlin / Heidelberg: Springer-Verlag, 2006. 353-363
[136] A. Poschmann, G Leander, K. Schramm, et al. A Family of Light-Weight Block Ciphers Based on DES Suited for RFID Applications. In: Proceedings of Workshop on RFID Security. Berlin / Heidelberg: Springer-Verlag, 2006. 6-11
[137] H. J. Chae, D. J. Yeager, J. R. Smith, et al. Maximalist Cryptography and Computation on the WISP UHF RFID Tag. In: Proceedings of the Conference on RFID Security, 2007. 52-63
[138] S. Kumar, C. Paar. Are Standards Compliant Elliptic Curve Cryptosystems Feasible on RFID? In: Proceedings of Workshop on RFID Security. Berlin / Heidelberg: Springer-Verlag, 2006. 212-219
[139] M. McLoone, M. J. B. RobshaW. New Architectures for Low-Cost Public Key Cryptography on RFID Tags. In: Proceedings of IEEE International Symposium on Circuits and Systems. Washington, DC: IEEE, 2007.1827-1830
[140] Y. Oren, M. Feldhofer. A Low-Resource Public-Key Identification Scheme for RFID Tags and Sensor Nodes. In: Proceedings of the second ACM conference on Wireless network security. New York: ACM Press, 2009. 59-68
[141] M. Feldhofer. Low-Power Hardware Design of Cryptographic Algorithms for RFID Tags: [PhD Thesis]. Graz, Austria: Graz University of Technology, Institute for Applied Information Processing and Communications (IAIK), 2008
[142] S. A. Weis, S. E. Sarma, R. L. Rivest, et al. Security and Privacy Aspects of Low-Cost Radio Frequency Identification Systems. In: Proceedings of the 1st International Conference on Security in Pervasive Computing. Berlin / Heidelberg: Springer-Verlag, 2003. 201-212
[143] K. Rhee, J. Kwak, S. Kim, et al. Challenge-Response Based RFID Authentication Protocol for Distributed Database Environment. In: Proceedings of the 2rd International Conference on Security in Pervasive Computing. Berlin / Heidelberg: Springer-Verlag, 2005. 70-84
[144] D. Molnar, D. Wagner. Privacy and security in library RFID: Issues, practices, and architectures. In: Proceedings of the 11th ACM conference on Computer and communications security. New York: ACM Press, 2004. 210-219
[145] D. Henrici, P. Muller. Hash-based Enhancement of Location Privacy for Radio-Frequency Identification Devices using Varying Identifiers. In: Proceedings of the Second IEEE Annual Conference on Pervasive Computing and Communications Workshops. Washington, DC: IEEE, 2004. 149-153
[146] P. Golle, M. Jakobsson, A. Juels, et al. Universal re-encryption for mixnets. In: Proceedings of the 2004 RSA Conference, Cryptographer's track. Berlin / Heidelberg: Springer-Verlag, 2004. 163-178
[147] J. Saito, J.C. Ryou, K. Sakurai. Enhancing privacy of universal reencryption scheme for RFID tags. In: Proceedings of International Conference on Embedded and Ubiquitous Computing. Berlin / Heidelberg: Springer-Verlag, 2004. 879-890
[148] A. Juels, R. Pappu. Squealing euros: Privacy protection in RFID-enabled banknotes. In: Proceedings of Financial Cryptography. Berlin / Heidelberg: Springer-Verlag, 2003.103-121
[149] M. Ohkubo, K. Suzuki, S. Kinoshita. Efficient hash-chain based RFID privacy protection scheme. In: Proceedings of International Conference on Ubiquitous Computing - Ubicomp, Workshop Privacy: Current Status and Future Directions. 2004.160-171
[150] A. Juels, S. Weis. Authenticating Pervasive Devices with Human Protocols. In: Proceedings of the 25th Annual International Cryptology Conference on Advances in Cryptology. Berlin / Heidelberg: Springer-Verlag, 2005. 293-308
[151] J. Bringer, H. Chabanne, E. Dottax. HB++: A Lightweight Authentication Protocol Secure against Some Attacks. In: Proceedings of IEEE International Conference on Pervasive Service. Washington, DC: IEEE, 2006. 28-33
[152] S. M. Lee, Y. J. Hwang, D. H. Lee, et al. Efficient authentication for low-cost RFID systems.In:Proceedings of the International Conference on Computational Science and its Applications.Berlin / Heidelberg:Springer-Verlag,2005.619～627
[153]Ding Zhen-hua,Li Jin-tao,Feng Bo.A Taxonomy Model of RFID Security Threats.In:Proceedings of the 11 th IEEE International Conference on Communication Technology.Washington,DC:IEEE,2008.765～768
[154]周永彬，冯登国．RFID安全协议的设计与分析．计算机学报，2006，29(4)：581～589
[155]于宇，杨玉庆，闵昊．RFID标签的安全建模及对EPC C1G2协议的改进．小型微型计算机系统，2007，128(7)：1339～1444
[156]张帆，孙璇，马建峰等．供应链环境下通用可组合安全的RFID通信协议．计算机学报，2008，31(10)：1754～1767
[157]袁署光，戴宏跃，赖声礼．基于Hash函数的RFID认证协议．计算机工程，2008，34(12)：141～143
[158]李章林，卢桂章，辛运帏．基于Hash链的可扩展RFID验证协议．计算机工程，2008，34(4)：173～175
[159]李章林，卢桂章，辛运帏．重加密技术在RFID安全中的应用．计算机工程，2008，34(3)：160～162
[160]W.Rankl.Overview about attacks on smart cards.Information Security Technical Report,2003,8(1):67～84
[161]M.Huth,M.Ryan.Logic in Computer Science:Modelling and Reasoning about Systems,Second Edition.Cambridge:Cambridge University Press,2004.172～255
[162]J.R.Burch,J.M.Clarke,K.L.McMillan,et al.Symbolic model checking:10~(20) states and beyond.Information and Computation,1992,98(2):142～170
[163]K.L.McMillan.Symbolic model checking:an approach to the state explosion problem:[PhD thesis].Pittsburgh:Computer Science Documentation School of Computer Science,Carnegie Mellon University,1992
[164]K.L.McMillan.Getting started with SMV:[Technical Report].Cadence Berkeley Laboratories,Berkeley,USA,2001.URL:http://www.itu.dk/courses/ISOT/E2OO3/doc/tutorial/tutorial.html
[165]A.Cimatti,E.Clarke,E.Giunchiglia,et al.Nusmv 2:An opensource tool for symbolic model checking.In:Proceedings of the 14th International Conference on Computer Aided Verification.London:Springer-Verlag,2002.359～364
[166]曹计昌，周宇杰．基于高地址约束和按需存储分配的UCard底层调度模块研究． 计算机工程与科学，2007，29(6)：121～123，147
[167]曹计昌，冯国平．UCard中动态地址总线的安全稳定性．华中科技大学学报(自然科学版)，2006，34(11)：48～51
[168]舒林，曹计昌，卢正鼎．基于会议模型的射频优卡多COS安全模型．华中科技大学学报(自然科学版)，2008，36(12)：20～23
[169]Lin Shu,Jichang Cao,Zhengding Lu.CIM:Hardware Support for Multi-COS Isolation of RF-UCard.In:Proceedings of the 2008 International Conference on Embedded Software and Systems.Washington,DC:IEEE,2008.595～602
[170]Oregano Systems.MC8051 IP core user guide (version 1.5).URL:http://oregano.at/ger/8051.html,2006
[171]International Organization for Standardization.IS O/IEC 18000-1:Information technology -- Radio frequency identification for item management,Part 1:Reference architecture and definition of parameters to be standardized.Published standard,2008
[172]唐应辉，唐小我．排队论：基础与分析技术．北京：科学出版社，2006．1～6，75～77
[173]Jichang Cao,Lin Shu,Zhengding Lu.Synchronous Dynamic Adjusting:An Anti-collision Algorithm for an RF-UCard System.International Journal of Communications,Network and System Sciences,2009,2(1):8～20
[174]Jichang Cao,Lin Shu,Zhengding Lu.Role-based Enhancement of Secure Authentication for RF-UCard Systems.In:Proceedings of the 4th IEEE International Conference on Wireless Communications,Networking and Mobile Computing.Washington,DC:IEEE,2008.1～4
[175]Helion Technology Ltd.Fast SHA-1 Hash Core forASIC:[Datasheet].2005.URL:http://www.heliontech.com/downloads/shal_asic_fast_helioncore.pdf
[2]T.F.Massey.MULTOS - The High Security Smart Card OS:[Whitepaper].MAOSCO,Inc.,2005.URL:http://www.multos.com/downloads/marketing/Whitepaper MULTOS_ Security.pdf
[3]曹计昌，邱鹏，张斌．UCard中动态地址映射的实现方法研究．计算机工程与科学，2006，28(1)：119～121，134
[4]Intemational Organization for Standardization.ISO/IEC 10536-3:Identification cards -- Contactless integrated circuit(s) cards,Part 3:Electronic signals and reset procedures.Published standard,1996
[5]International Organization for Standardization.ISO/IEC 14443-4:Identification cards -- Contactless integrated circuit cards -- Proximity cards,Part 4:Transmission protocol.Published standard,2008
[6]International Organization for Standardization.ISO/IEC 15693-3:Identification cards -- Contactless integrated circuit(s) cards,Part 3:Anticollision and transmission protocol.Published standard,2001
[7]J.-J.Vandewalle.Smart Card Research Perspectives.In:Proceedings of International Workshop on Construction and Analysis of Safe,Secure,and Interop.erable Smart Devices.Berlin / Heidelberg:Springer-Verlag,2005.250～256
[8]J.H.Saltzer,M.D.Schroeder.The protection of information in computer systems.Proceedings of the IEEE,1975,63(9):1278～1308
[9]J.E.Smith,R.Nair.The Architecture of Virtual Machines.Computer,2005,38(5):32～38
[10]VMware Inc.Security Design of the VMware Infrastructure 3 Architecture:[Technology White Paper].URL:http://www.vmware.com/pdf/vi3_security_architecture_wp.pdf,Feb.2007
[11]A.Whitaker,M.Shaw,S.D.Gribble.Denali:Lightweight Virtual Machines for Distributed and Networked Applications.Technical Report 02-02-01,University of Washington,2002
[12]A.Whitaker,M.Shaw,S.D.Gribble.Scale and performance in the Denali isolation kernel. In: Proceedings of the 5th Symposium on Operating Systems Design and Implementation. New York: ACM Press, 2002. 195-210
[13] P. Barham, B. Dragovic and K. Fraser. Xen and the art of virtualization. In: Proceedings of the 19th ACM Symposium on Operating Systems Principles. New York: ACM Press, 2003. 164-177
[14] D. Lie, C. Thekkath, M. Mitchell, et al. Architectural support for copy and tamper resistant software. In: Proceedings of the International Conference on Architectural Support for Programming Languages and Operating Systems. New York: ACM Press, 2000. 168-177
[15] D. Lie, M. Mitchell, C. Thekkath, et al. Specifying and Verifying Hardware for Tamper-Resistant Software. In: Proceedings of the 2003 IEEE Symposium on Security and Privacy. Washington, DC: IEEE, 2003. 166-177
[16] D. Lie, C. Thekkath, M. Horowitz, et al. Implementing an untrusted operating system on trusted hardware. In: Proceedings of the nineteenth ACM symposium on Operating systems principles. New York: ACM Press, 2003. 178-192
[17] B. Gassend, G E. Suh, D. Clarke, et al. Caches and Hash Trees for Efficient Memory Integrity Verification. In: Proceedings of the 9th International Symposium on High-Performance Computer Architecture. Washington, DC: IEEE, 2003. 295-306
[18] W. Shi, H. S. Lee, M. Ghosh, et al. High Efficiency Counter Mode Security Architecture via Prediction and Precomputation. In: Proceedings of the 32nd International Symposium on Computer Architecture. Washington, DC: IEEE, 2005. 14-24
[19] C. Lu, T. Zhang, W. Shi, et al. M-TREE: A High Efficiency Security Architecture for Protecting Integrity and Privacy of Software. Journal of Parallel and Distributed Computing for a special issue on Security in Grid and Distributed Systems, 2006, 66(9): 1116-1128
[20] G E. Suh, D. Clarke, B. Gassend, et al. AEGIS: Architecture for Tamper-Evident and Tamper-Resistant Processing. In: Proceedings of the 17th annual international conference on Supercomputing. New York: ACM Press, 2003. 160-171
[21] G E. Suh, C. W. O'Donnell, S. Devadas. Aegis: A Single-Chip Secure Processor. IEEE Design & Test, 2007,24(6): 570-580
[22] J. Rushby. Design and verification of secure systems. In: Proceedings of the 8th Symposium on Operating System Principles. New York: ACM Press, 1981. 12-21
[23] E. J. Koldinger, J. S. Chase, S. J. Eggers. Architectural support for single address space operating systems. ACM SIGPLAN Notices, 1992, 27(9): 175-186
[24] M. Swift, B. Bershad, H. Levy. Improving the Reliability of Commodity Operating Systems. In: Proceedings of the 19th ACM Symposium on Operating Systems Principles. New York: ACM Press, 2003. 207-222
[25] E. Witchel, J. Rhee, K. Asanovic. Mondrix: Memory Isolation for Linux using Mondriaan Memory Protection. In: Proceedings of the 20th ACM Symposium on Operating Systems Principles. New York: ACM Press, 2005. 31-44
[26] E. Witchel, J. Cates, K. Asanovic. Mondrian memory protection. In: Proceedings of the Tenth International Conference on Architectural Support for Programming Languages and Operating Systems. New York: ACM Press, 2002. 304-316
[27] S. Jain, F. Shafique, V. Djeric, et al. Application-level isolation and recovery with solitude. ACM SIGOPS Operating Systems Review, 2008,42(4): 95-107
[28] U. Erlingsson, M. Abadi, M. Vrable, et al. XFI: Software Guards for System Address Spaces. In: Proceedings of the 7th Symposium on Operating Systems Design and Implementation. Berkeley: USENIX Association, 2006. 75-88
[29] N. Aggarwal, P. Ranganathan, N. P. Jouppi, et al. Configurable Isolation: Building High Availability Systems with Commodity Multi-Core Processors. In: Proceedings of the 34th annual international symposium on Computer architecture. New York: ACM Press, 2007. 470-481
[30] I. B. Ganev. A Pliable Hybrid Architecture for Code Isolation: [PhD thesis]. Georgia Institute of Technology, 2007
[31] C. Minh, M. Trautmann, J. Chung, et al. An effective hybrid transactional memory system with strong isolation guarantees. In: Proceedings of the 34th annual international symposium on Computer architecture. New York: ACM Press, 2007. 69-80
[32] T. Shpeisman, V. Menon, A. Tabatabai, et al. Enforcing isolation and ordering in STM. In: Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation. New York: ACM Press, 2007. 78-88
[33] D. Elkaduwe, P. Derrin, K. Elphinstone. Kernel design for isolation and assurance of physical memory. In: Proceedings of the 1st workshop on Isolation and integration in embedded systems. New York: ACM Press, 2008. 35-40
[34] T. Huffmire, B. Brotherton, G Wang, et al. Moats and Drawbridges: An Isolation Primitive for Reconfigurable Hardware Based Systems. In: Proceedings of the 2007 IEEE Symposium on Security and Privacy.Washington,DC:IEEE,2007.281～295
[35]温研，王怀民．基于本地虚拟化技术的隔离执行模型研究．计算机学报，2008，31(10)：1768～1779
[36]王小光，夏克俭，张焕生．虚拟机中关于内存保护的故障隔离技术研究．计算机工程与设计，2008，29(16)：4315～4318
[37]Xue Haifeng,Qing Sihan,Zhang Huanguo.XEN Virtual Machine Technology and Its Security Analysis.Wuhan University Journal of Natural Sciences,2007,12(1):159～162
[38]吴新勇．嵌入式操作系统安全保障技术研究：[博士学位论文]．四川成都：电子科技大学，2003
[39]Global Platform.Open Platform Card Specification.Version 2.2.March 2006.URL:http://www.globalplatform.org
[40]Common Criteria.Common Criteria for Information Technology Security Evaluation (CC),Version 2.1,ISO/IEC 15408,August 1999
[41]French Certification Body PP/0010.Protection Profile Smart Card IC with Multi-Application Secure Platform,version 2.0,Eurosmart,November 2000.URL:http://www.commoncriteriaportal.org/public/files/ppfiles/PP0010.pdf
[42]J.P.Tual.MASSC:A Generic Architecture for Multiapplication Smart Cards.IEEE Micro,1999,19(5):52～61
[43]P.Girard.Which security policy for multiapplication smart cards.In:Proceedings of the USENIX Workshop on Smartcard Technology.Berkeley:USENIX Association,1999.21～28
[44]G Schellhorn,W.Reif,A.Schairer,et al.Verified formal security models for multiapplicative smart cards.Journal of Computer Security,2002,10(4):339～367
[45]I.Bakdi.Towards a Secure and Practical Multifunctional Smart Card.In:Proceedings of the 7th IFIP WG 8.8/11.2 International Conference on Smart Card Research and Advanced Applications.Berlin / Heidelberg:Springer-Verlag,2006.16～31
[46]G.Barthe,G.Dufay.Formal Methods for Smartcard Security.Foundations of Security Analysis and Design Ⅲ,2005,3655:133～177
[47]M.Witteman.Java card security.Information Security Bulletin,2003,8:291～298
[48]K.Markantonakis,K.Mayes,M.Tunstall,et al.Smart Card Security.Studies in Computational Intelligence, 2007, 57(2007): 201-233
[49] W. Mostowski, E. Poll. Malicious Code on Java Card Smartcards: Attacks and Countermeasures. In: Proceedings of the 8th IFIP WG 8.8/11.2 international conference on Smart Card Research and Advanced Applications. Berlin / Heidelberg: Springer-Verlag, 2008. 1-16
[50] Sun Microsystems, Inc. Java Card Platform Specification. Version 3.0. March 2008. URL: http://java.sun.com/javacard/3.0/specs.jsp
[51] X. Leroy. Java Bytecode Verification: Algorithms and Formalizations. Journal of Automated Reasoning, 2003, 30(3-4): 235-269
[52] D. Basin, S. Friedrich, M. Gawkowski. Bytecode Verification by Model Checking. Journal of Automated Reasoning, 2003, 30(3-4): 399-444
[53] Sun Microsystems, Inc. The Runtime Environment Specification for the Java Card ~(TM)Platform, Classic Edition, Version 3.0,2008
[54] M. Montgomery, K. Krishna. Secure object sharing in Java Card. In: Proceedings of the USENIX Workshop on Smartcard Technology. Berkeley: USENIX Association, 1999. 119-127
[55] W. Mostowski, E. Poll. Testing the Java Card Applet Firewall. Technical Report: ICIS-R07029, Radboud University Nijmegen. December 2007. URL: https://pms.cs.ru.nl/iris-diglib/src/icis tech reports.php
[56] W. Mostowski, E. Poll. Java Card Applet Firewall Exploration and Exploitation. In: Proceedings of the e-Smart 2008, Brussels: Eurosmart, 2008. 1-4
[57] W. Dietl, P. M(?)ller, A. Poetzsch-Heffter. A type system for checking applet isolation in Java Card. In: Proceedings of the International Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart devices. Berlin / Heidelberg: Springer-Verlag, 2004.129-150
[58] D. Ghindici, I. Simplot-Ryl. On Practical Information Flow Policies for Java-Enabled Multiapplication Smart Cards. In: Proceedings of the 8th IFIP WG 8.8/11.2 international conference on Smart Card Research and Advanced Applications. Berlin / Heidelberg: Springer-Verlag, 2008. 32-47
[59] P. Bieber, J. Cazin, P. Girard, et al. Checking secure interactions of smart card applets: extended version. Journal of Computer Security, 2002, 10(4): 369-398
[60] J. Andronick, B. Chetali, O. Ly. Using Coq to Verify Java Card Applet Isolation Properties. Theorem Proving in Higher Order Logics, 2003, 2758: 335-351
[61] M. Eluard, T. Jensen. Secure object flow analysis for Java card. In: Proceedings of the 5th conference on Smart Card Research and Advanced Application Conference.Berkeley:USENIX Association,2002.97～110
[62]M.(?)luard,T.Jensen.An operational semantics of the Java Card firewall.In:Proceedings of the International Conference on Research in Smart Cards:Smart Card Programming and Security.London:Springer-Verlag,2001.95～110
[63]P.Ferrara,Jail:Firewall analysis of java card by abstract interpretation.In:Proceedings of the 1 st International Workshop on Emerging Applications of Abstract Interpretation.Amsterdam:Elsevier Science Publishers B.V.,2006.1～15
[64]W.Mostowski.Formalisation and Verification of Java Card Security Properties in Dynamic Logic.In:Proceedings of the 8th International Conference on Fundamental Approaches to Software Engineering.Berlin / Heidelberg:Springer-Verlag,2005.357～371
[65]V.Almaliotis,A.Loizidis,P.Katsaros.Static Program Analysis for Java Card Applets.In:Proceedings of the 8th IFIP WG 8.8/11.2 international conference on Smart Card Research and Advanced Applications.Berlin / Heidelberg:Springer-Verlag,2008.17～31
[66]刘玉珍，张焕国．多应用安全智能卡结构的研究．武汉大学学报(理学版)，2006，52(1)：87～92
[67]董威，杨义先．一种跨行业多应用智能卡系统模型及实现．计算机工程，2007，23(8)：230～232
[68]王同洋，秦保安，吴俊军．一卡多用安全管理平台．计算机应用，2005，25(1)：154～157
[69]吴俊军，罗标．“一卡多用”中卡操作系统多应用管理的设计．计算机应用与软件，2006，23(8)：68～71
[70]胥怡心，张其善，刘建伟．Java卡的可信代码装载机制设计．北京航空航天大学学报，2009，35(1)：32～35
[71]吴俊军，马鑫龙，张新访．一种新的Java智能卡上字节码校验算法．计算机工程与科学，2008，30(3)：65～68
[72]吴俊军，马鑫龙．一种使用CFT的Java卡内字节码校验算法．小型微型计算机系统，2008，29(12)：2360～2364
[73]向文，韩晶，吴俊军．基于混合模式的Java卡字节码优化器．计算机工程与科学，2008，30(7)：155～158
[74] D-H. Shih, P.-L. Sun, D. C. Yen, et al. Taxonomy and survey of RFID anti-collision protocols. Computer Communications, 2006,29(11): 2150-2166
[75] N. Abramson. The ALOHA system - Another alternative for computer communication. In: Proceedings of the FIPS Fall Joint Computer Conference. Gaithersburg: Information Technology Laboratory, NIST, 1970. 281-285
[76] L. G Roberts. ALOHA packet system with and without slots and capture. Computer Communications Review, 1975, 5(2): 28-42
[77] F. C. Schoute. Control of ALOHA Signalling in a Mobile Radio Trunking System. In: Proceedings of the International Conference on Radio Spectrum Conservation Techniques. London: Institution of Electrical Engineers, 1980. 38-42
[78] F. C. Schoute. Dynamic Frame Length ALOHA. IEEE Transactions on Communications, 1983, 31(4): 565-568
[79] H. Vogt. Efficient Object Identification with Passive RFID Tags. In: Proceedings of the First International Conference on Pervasive Computing. London: Springer-Verlag, 2002. 98-113
[80] J. Zhai, G.-N. Wang. An Anti-collision Algorithm Using Two-Functioned Estimation for RFID Tags. In: Proceedings of the Int'l Conf. Computational Science and its Applications, Berlin / Heidelberg: Springer-Verlag, 2005. 702-711
[81] W.-T. Chen, G-H. Lin. An Efficient Anti-Collision Method for Tag Identification in a RFID System. IEICE Transactions on Communications, 2006, E89-B(12): 3386-3392
[82] S.-R. Lee, S.-D. Joo, C.-W. Lee. An Enhanced Dynamic Framed Slotted ALOHA Algorithm for RFID Tag Identification. In: Proceedings of the 2nd Annual International Conference on Mobile and Ubiquitous Systems: Networking and Services, 2005. 166-172
[83] J.-R. Cha, J.-H. Kim. Novel Anti-collision Algorithms for Fast Object Identification in RFID System. In: Proceedings of the 11th International Conference on Parallel and Distributed Systems, 2005. 63-67
[84] T.-W. Hwang, B.-G Lee, Y. S. Kim, et al. Improved Anti-collision Scheme for High Speed Identification in RFID System. In: Proceedings of the First International Conference on Innovative Computing, Information and Control, 2006. 449-452
[85] K. Ali, H. Hassanein, A. M. Taha. RFID Anti-collision Protocol for Dense Passive Tag Environments. In: Proceedings of the 32nd IEEE Conference on Local Computer Networks. Washington, DC: IEEE, 2007. 819-824
[86]王建伟，赵玉萍，T．Korhonen．RFID系统防碰撞协议研究——设计与优化．电子与信息学报，2009，3 1(1)：1～4
[87]耿淑琴，高大明，汪金辉．射频识别系统中自适应反碰撞法的实现．北京邮电大学学报，2008，3 1(6)：76～79
[88]王晓华，周晓光，孙百生．射频识别系统中的防碰撞算法设计．北京邮电大学学报，2008，30(2)：59～62
[89]S.-S.Yu,Y.Zhan,Y.-h.Wang.RFID Anti-collision algorithm Based on Bi-directional Binary Exponential Index.In:Proceedings the IEEE International Conference on Automation and Logistics.Washington,DC:IEEE,2007.2917～2921
[90]梁彪，胡爱群，秦中元．一种新的RFID防碰撞算法设计．电子与信息学报，2007，29(9)：2158～2160
[91]J.I.Capetanakis.Tree algorithms for packet broadcast channels.IEEE Transactions on Information Theory,1979,25(5):505～515
[92]K.Finkenzeller,RFID Handbook:Fundamentals and Applications in Contactless Smart Cards and Identification (2nd Edition).New York,NY,USA:John Wiley & Sons,Inc.,2003.168～192
[93]S.S.Kim,Y.H.Kim,S.J.Lee,et al.An Improved Anti Collision Algorithm using Parity Bit in RFID System.In:Proceedings of the Seventh IEEE International Symposium on Network Computing and Applications.Washington,DC:IEEE,2008.224～227
[94]H.J.Yeo,Y.H.Kim,H.Y.Lim,et al.ID Prediction Algorithm for Tag Collision Arbitration in RFID System.In:Proceedings of the 13th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications.Washington,DC:IEEE,2007.476～481
[95]C.Law,K.Lee,K.-Y.Siu.Efficient memoryless protocol for tag identification (extended abstract).In:Proceedings of the 4th International Workshop on Discrete Algorithms and Methods for Mobile Computing and Communications.New York:ACM Press,2000.75～84
[96]H.Lee,J.Kim.QT-CBP:A New RFID Tag Anti-collision Algorithm Using Collision Bit Positioning.In:Proceedings of the Workshops on Emerging Directions in Embedded and Ubiquitous Computing.Berlin / Heidelberg:Springer-Verlag,2006.591～600
[97] A. Juels, R. L. Rivest, M. Szydlo. The blocker tag: selective blocking of RFID tags for consumer privacy. In: Proceedings of the 10th ACM conference on Computer and communications security. New York: ACM Press, 2003. 103-111
[98] M. Jacomet, A. Ehrsam, U. Gehrig. Contactless Identification Device with Anticollision Algorithm. In: Proceedings of IEEE Conference on Circuits, System, Computers and Communications. Washington, DC: IEEE, 1999. 4-8
[99] H.-S. Choi, J.-R. Cha, J.-H. Kim. Fast wireless anti-collision algorithm in ubiquitous ID system. In: Proceedings of IEEE 60th Vehicular Technology Conference. Washington, DC: IEEE, 2004. 4589-4592
[100] J. H. Choi, D. Lee, Y. Youn, et al. Scanning-Based Pre-Processing for Enhanced Tag Anti-Collision Protocols. In: Proceedings of the 2006 International Symposium on Communications and Information Technologies. Washington, DC: IEEE, 2006. 1207-1211
[101] J. Myung, W. Lee. Adaptive Binary Splitting: A RFID Tag Collision Arbitration Protocol for Tag Identification. Mobile Networks and Applications, 2006,11(5): 711-722
[102] J. Myung, W. Lee, J. Srivastava, et al. Tag-Splitting: Adaptive Collision Arbitration Protocols for RFID Tag Identification. IEEE Transactions on Parallel and Distributed Systems, 2007,18(6): 763-775
[103] J. Myung, W. Lee. Adaptive splitting protocols for RFID tag collision arbitration. In: Proceedings of the 7th ACM international symposium on Mobile ad hoc networking and computing. New York: ACM Press, 2006. 202-213
[104] J. Myung, W. Lee, T. K. Shih. An adaptive memoryless protocol for RFID tag collision arbitration. IEEE transactions on multimedia, 2006, 8(5): 1096-1101
[105] X. Huang, D. Tran. Adaptive Binary Splitting for a RFID Tag Collision Arbitration Via Multi-agent Systems. In: Proceedings of the 11th International Conference on Knowledge-Based Intelligent Information and Engineering Systems. Berlin / Heidelberg: Springer-Verlag, 2007. 926-933
[106] J. H. Choi, D. Lee, H. Jeon, et al. Enhanced Binary Search with Time-Divided Responses for Efficient RFID Tag Anti-Collision. In: Proceedings of the IEEE International Conference on Communications. Washington, DC: IEEE, 2007. 3853-3858
[107] H.-S. Choi, J.-H. Kim. Anti-collision algorithm using Bin slot in RFID System. In: Proceedings of the IEEE Region 10 Conference on TENCON. Washington, DC: IEEE,2005.1～6
[108]J.-Y.Kim,B.-S.Kang,J.-W.Jwa,et al.Bin-slotted Hybrid Search Algorithm for Multiple RFID Arbitration.In:Proceedings of the 2006 International Conference on Wireless Networks.Las Vegas:CSREA Press,2006.164～172
[109]C.-H.Quan,W.-K.Hong,H.-C.Kim.Performance Analysis of Tag Anti-collision Algorithms for RFID Systems.In:Proceedings of the 2006 Workshops on Emerging Directions in Embedded and Ubiquitous Computing.Berlin / Heidelberg:Springer-Verlag,2006.382～391
[110]W.-T.Chen.Performance Comparison of Binary Search Tree and Framed ALOHA Algorithms for RFID Anti-Collision.IEICE Transactions on Communications,2008,E91-B(4):1168～1171
[111]余松森，詹宜巨，彭卫东等．基于后退式索引的二进制树形搜索反碰撞算法及其实现．计算机工程与应用，2004(16)：26～28
[112]余松森，詹宜巨，王志平等．跳跃式动态树形反碰撞算法及其分析．计算机程，2005，31(9)：19～20，26
[113]余松森，詹宜巨．基于修剪枝的二进制树形搜索反碰撞算法与实现．计算机工程，2005，31(16)：217～218，230
[114]谢振华，赖声礼，陈鹏．RFID技术和防冲撞算法．计算机工程与应用，2007，43(6)：223～225
[115]B.Feng,J.-T.Li,J.-B.Guo,et al.ID-Binary Tree Stack Anticollision Algorithm for RFID.In:Proceedings of the 11th IEEE Symposium on Computers and Communications.Washington,DC:IEEE,2006.207～212
[116]冯波，李锦涛，郑为民等．一种新的RFID标签识别防冲突算法．自动化学报，2008，34(6)：632～638
[117]K.W.Chiang,C.Hua,T.P.Yum.Prefix-Randomized Query-Tree Protocol for RFID Systems.In:Proceedings of the 11th IEEE Symposium on Computers and Communications.Washington,DC:IEEE,2006.1653～1657
[118]焦传海，王可人．多枝查询树协议在解决射频识别碰撞问题中的应用．电讯技术，2008，48(3)：95～99
[119]赵曦，张有光．一种新颖的RFID多标签防碰撞算法．北京航空航天大学学报，2008，34(13)：276～279
[120]S.E.Sarma,S.A.Weis,D.W.Engels.RFID Systems and Security and Privacy Implications.In:Proceedings of the 4th International Workshop on Cryptographic Hardware and Embedded Systems. London: Springer-Verlag, 2002. 454-469
[121] A. Juels. RFID Security and Privacy: A Research Survey. Journal of Selected Areas in Communication (J-SAC), 2006,24(2): 381-395
[122] G Avoine. RFID Security & Privacy Lounge. URL: http://www.avoine.net/rfid/, 2009
[123] A. Juels. Minimalist cryptography for low-cost RFID tags. In: Proceedings of the 4th International Conference on Security in Communication Networks. Berlin / Heidelberg: Springer-Verlag, 2004. 149-164
[124] D. Molnar, A. Soppera, D. Wagner. A Scalable, Delegatable Pseudonym Protocol Enabling Ownership Transfer of RFID Tags. In: Proceedings of the 12th International Workshop on Selected Areas in Cryptography. Berlin / Heidelberg: Springer-Verlag, 2006. 276-290
[125] G Avoine. Adversarial Model for Radio Frequency Identification. Technical Report, LASECREPORT-2005-001, Swiss Federal Institute of Technology (EPFL), Security and Cryptography Laboratory (LASEC), Lausanne, Switzerland, 2005
[126] G Avoine, P. Oechslin. RFID Traceability: A Multilayer Problem. In: Proceedings of the 9th International Conference on Financial Cryptography and Data Security. Berlin / Heidelberg: Springer-Verlag, 2005. 125-140
[127] X. L. Zhang, B. King. Modeling RFID Security. In: Proceedings of the First SKLOIS Conference on Information Security and Cryptology. Berlin / Heidelberg: Springer-Verlag, 2005. 75-90
[128] S. Vaudenay, On Privacy Models for RFID. In: Proceedings of the 13th International Conference on the Theory and Application of Cryptology and Information Security. Berlin / Heidelberg: Springer-Verlag, 2008. 68-87
[129] MIT Auto-ID Center. 860MHz-960MHz Class I Radio Frequency Identification Tag Radio Frequency & Logical communication Interface Specification Proposed Recommendation Version 1.0.0. Technical Report MIT AUTO ID-TR-007, 2002
[130] S.-C. Kim, S.-S. Yeo, S. K. Kim. MARP: Mobile Agent for RFID Privacy Protection. In: Proceedings of the 7th IFIP WG 8.8/11.2 International Conference on Smart Card Research and Advanced Applications. Berlin / Heidelberg: Springer-Verlag, 2006. 300-312
[131] S.-S. Yeo, S.-C. Kim, S. K. Kim. eMARP: Enhanced Mobile Agent for RFID Privacy Protection and Forgery Detection. In: Proceedings of the First KES International Symposium on Agent and Multi-Agent Systems: Technologies and Applications. Berlin / Heidelberg: Springer-Verlag, 2007. 318-327
[132] A. Juels, J. Brainard. Soft Blocking: Flexible Blocker Tags on the Cheap. In: Proceedings of the 2004 ACM workshop on Privacy in the electronic society. New York: ACM Press, 2004. 1-7
[133] M. Rieback, B. Crispo, A. Tanenbaum. Keep on Blockin' in the Free World: Personal Access Control for Low-Cost RFID Tags. In: Proceedings of the 13th International Workshop on Security Protocols. Berlin / Heidelberg: Springer-Verlag, 2005. 51-59
[134] M. Feldhofer, S. Dominikus, J. Wolkerstorfer. Strong Authentication for RFID Systems Using the AES Algorithm. In: Proceedings of the 6th International Workshop on Cryptographic Hardware and Embedded Systems. Berlin / Heidelberg: Springer-Verlag, 2004. 357-370
[135] M. Kim, J. Ryou, Y. Choi. Low Power AES Hardware Architecture for Radio Frequency Identification. In: Proceedings of the First International Workshop on Security. Berlin / Heidelberg: Springer-Verlag, 2006. 353-363
[136] A. Poschmann, G Leander, K. Schramm, et al. A Family of Light-Weight Block Ciphers Based on DES Suited for RFID Applications. In: Proceedings of Workshop on RFID Security. Berlin / Heidelberg: Springer-Verlag, 2006. 6-11
[137] H. J. Chae, D. J. Yeager, J. R. Smith, et al. Maximalist Cryptography and Computation on the WISP UHF RFID Tag. In: Proceedings of the Conference on RFID Security, 2007. 52-63
[138] S. Kumar, C. Paar. Are Standards Compliant Elliptic Curve Cryptosystems Feasible on RFID? In: Proceedings of Workshop on RFID Security. Berlin / Heidelberg: Springer-Verlag, 2006. 212-219
[139] M. McLoone, M. J. B. RobshaW. New Architectures for Low-Cost Public Key Cryptography on RFID Tags. In: Proceedings of IEEE International Symposium on Circuits and Systems. Washington, DC: IEEE, 2007.1827-1830
[140] Y. Oren, M. Feldhofer. A Low-Resource Public-Key Identification Scheme for RFID Tags and Sensor Nodes. In: Proceedings of the second ACM conference on Wireless network security. New York: ACM Press, 2009. 59-68
[141] M. Feldhofer. Low-Power Hardware Design of Cryptographic Algorithms for RFID Tags: [PhD Thesis]. Graz, Austria: Graz University of Technology, Institute for Applied Information Processing and Communications (IAIK), 2008
[142] S. A. Weis, S. E. Sarma, R. L. Rivest, et al. Security and Privacy Aspects of Low-Cost Radio Frequency Identification Systems. In: Proceedings of the 1st International Conference on Security in Pervasive Computing. Berlin / Heidelberg: Springer-Verlag, 2003. 201-212
[143] K. Rhee, J. Kwak, S. Kim, et al. Challenge-Response Based RFID Authentication Protocol for Distributed Database Environment. In: Proceedings of the 2rd International Conference on Security in Pervasive Computing. Berlin / Heidelberg: Springer-Verlag, 2005. 70-84
[144] D. Molnar, D. Wagner. Privacy and security in library RFID: Issues, practices, and architectures. In: Proceedings of the 11th ACM conference on Computer and communications security. New York: ACM Press, 2004. 210-219
[145] D. Henrici, P. Muller. Hash-based Enhancement of Location Privacy for Radio-Frequency Identification Devices using Varying Identifiers. In: Proceedings of the Second IEEE Annual Conference on Pervasive Computing and Communications Workshops. Washington, DC: IEEE, 2004. 149-153
[146] P. Golle, M. Jakobsson, A. Juels, et al. Universal re-encryption for mixnets. In: Proceedings of the 2004 RSA Conference, Cryptographer's track. Berlin / Heidelberg: Springer-Verlag, 2004. 163-178
[147] J. Saito, J.C. Ryou, K. Sakurai. Enhancing privacy of universal reencryption scheme for RFID tags. In: Proceedings of International Conference on Embedded and Ubiquitous Computing. Berlin / Heidelberg: Springer-Verlag, 2004. 879-890
[148] A. Juels, R. Pappu. Squealing euros: Privacy protection in RFID-enabled banknotes. In: Proceedings of Financial Cryptography. Berlin / Heidelberg: Springer-Verlag, 2003.103-121
[149] M. Ohkubo, K. Suzuki, S. Kinoshita. Efficient hash-chain based RFID privacy protection scheme. In: Proceedings of International Conference on Ubiquitous Computing - Ubicomp, Workshop Privacy: Current Status and Future Directions. 2004.160-171
[150] A. Juels, S. Weis. Authenticating Pervasive Devices with Human Protocols. In: Proceedings of the 25th Annual International Cryptology Conference on Advances in Cryptology. Berlin / Heidelberg: Springer-Verlag, 2005. 293-308
[151] J. Bringer, H. Chabanne, E. Dottax. HB++: A Lightweight Authentication Protocol Secure against Some Attacks. In: Proceedings of IEEE International Conference on Pervasive Service. Washington, DC: IEEE, 2006. 28-33
[152] S. M. Lee, Y. J. Hwang, D. H. Lee, et al. Efficient authentication for low-cost RFID systems.In:Proceedings of the International Conference on Computational Science and its Applications.Berlin / Heidelberg:Springer-Verlag,2005.619～627
[153]Ding Zhen-hua,Li Jin-tao,Feng Bo.A Taxonomy Model of RFID Security Threats.In:Proceedings of the 11 th IEEE International Conference on Communication Technology.Washington,DC:IEEE,2008.765～768
[154]周永彬，冯登国．RFID安全协议的设计与分析．计算机学报，2006，29(4)：581～589
[155]于宇，杨玉庆，闵昊．RFID标签的安全建模及对EPC C1G2协议的改进．小型微型计算机系统，2007，128(7)：1339～1444
[156]张帆，孙璇，马建峰等．供应链环境下通用可组合安全的RFID通信协议．计算机学报，2008，31(10)：1754～1767
[157]袁署光，戴宏跃，赖声礼．基于Hash函数的RFID认证协议．计算机工程，2008，34(12)：141～143
[158]李章林，卢桂章，辛运帏．基于Hash链的可扩展RFID验证协议．计算机工程，2008，34(4)：173～175
[159]李章林，卢桂章，辛运帏．重加密技术在RFID安全中的应用．计算机工程，2008，34(3)：160～162
[160]W.Rankl.Overview about attacks on smart cards.Information Security Technical Report,2003,8(1):67～84
[161]M.Huth,M.Ryan.Logic in Computer Science:Modelling and Reasoning about Systems,Second Edition.Cambridge:Cambridge University Press,2004.172～255
[162]J.R.Burch,J.M.Clarke,K.L.McMillan,et al.Symbolic model checking:10~(20) states and beyond.Information and Computation,1992,98(2):142～170
[163]K.L.McMillan.Symbolic model checking:an approach to the state explosion problem:[PhD thesis].Pittsburgh:Computer Science Documentation School of Computer Science,Carnegie Mellon University,1992
[164]K.L.McMillan.Getting started with SMV:[Technical Report].Cadence Berkeley Laboratories,Berkeley,USA,2001.URL:http://www.itu.dk/courses/ISOT/E2OO3/doc/tutorial/tutorial.html
[165]A.Cimatti,E.Clarke,E.Giunchiglia,et al.Nusmv 2:An opensource tool for symbolic model checking.In:Proceedings of the 14th International Conference on Computer Aided Verification.London:Springer-Verlag,2002.359～364
[166]曹计昌，周宇杰．基于高地址约束和按需存储分配的UCard底层调度模块研究． 计算机工程与科学，2007，29(6)：121～123，147
[167]曹计昌，冯国平．UCard中动态地址总线的安全稳定性．华中科技大学学报(自然科学版)，2006，34(11)：48～51
[168]舒林，曹计昌，卢正鼎．基于会议模型的射频优卡多COS安全模型．华中科技大学学报(自然科学版)，2008，36(12)：20～23
[169]Lin Shu,Jichang Cao,Zhengding Lu.CIM:Hardware Support for Multi-COS Isolation of RF-UCard.In:Proceedings of the 2008 International Conference on Embedded Software and Systems.Washington,DC:IEEE,2008.595～602
[170]Oregano Systems.MC8051 IP core user guide (version 1.5).URL:http://oregano.at/ger/8051.html,2006
[171]International Organization for Standardization.IS O/IEC 18000-1:Information technology -- Radio frequency identification for item management,Part 1:Reference architecture and definition of parameters to be standardized.Published standard,2008
[172]唐应辉，唐小我．排队论：基础与分析技术．北京：科学出版社，2006．1～6，75～77
[173]Jichang Cao,Lin Shu,Zhengding Lu.Synchronous Dynamic Adjusting:An Anti-collision Algorithm for an RF-UCard System.International Journal of Communications,Network and System Sciences,2009,2(1):8～20
[174]Jichang Cao,Lin Shu,Zhengding Lu.Role-based Enhancement of Secure Authentication for RF-UCard Systems.In:Proceedings of the 4th IEEE International Conference on Wireless Communications,Networking and Mobile Computing.Washington,DC:IEEE,2008.1～4
[175]Helion Technology Ltd.Fast SHA-1 Hash Core forASIC:[Datasheet].2005.URL:http://www.heliontech.com/downloads/shal_asic_fast_helioncore.pdf