用户名: 密码: 验证码:
私有信息检索技术研究
详细信息    本馆镜像全文|  推荐本文 |  |   获取CNKI官网全文
摘要
随着计算机、通信、网络技术的快速发展,利用网络存储、交换信息已成为人们的日常工作生活方式。然而,网络环境的复杂、用户行为的不确定等因素往往导致用户的隐私信息无法得到保障,因此提供一些方法保护用户的隐私信息十分重要。私有信息检索的提出就是为了解决这样一类问题:用户向数据库服务器提交查询时,在用户的查询信息不被泄露的条件下完成查询。针对现有的私有信息检索研究存在复杂度过高、缺乏隐私性度量方法、缺少与数据库结合的设计方法等不足,围绕私有信息检索的协议、度量等,展开了四个方面的研究工作。
     为降低私有信息检索协议的复杂度,提出了一个基于行的私有信息检索协议——Robac-PIR。该协议改进了基于二次剩余的私有信息检索协议,将用户对整个数据库服务器上数据的查询替换为对其上部分数据的查询,使得用户可以选择适量的数据块在隐私性与计算效率上进行折中。基于Robac-PIR协议,设计一个网络环境中的私有信息检索方案。将数据库服务器上已分块的数据分发给网络中的不同用户节点,把原本集中在服务器端的计算分担给多个节点并行执行,从而提高整体查询效率。实验表明,Robac-PIR协议及分布式Robac-PIR模式能够提供用户对隐私性与计算开销的灵活折中,且比起基于二次剩余的私有信息检索协议有更好的效率。
     为提高私有信息检索协议的实用性,提出了基于关键字的私有信息检索方案。首先对关键字建立哈希索引,然后以基于二次剩余的私有信息检索方法为例,将对关键字的查询转换为对索引的查询。将该方案应用于物联网,设计了支持用户查询隐私的发现服务器,以保护用户查询的目标关键字。该方法与已有的发现服务中的隐私保护方法相比,不需要复杂的密钥共享,也不用担心发现服务器节点的共谋,通过利用私有信息检索协议,能够完全保障用户的查询隐私。
     为解决私有信息检索研究中缺乏用户查询隐私性度量方法的问题,结合信息论,采用信息熵作为用户查询隐私性的量化方法。用提出的量化方法对Robac-PIR协议以及已有的一些私有信息检索协议进行量化分析。通过分析表明,该度量方法可以量化私有信息检索问题中用户查询的隐私性,具有可对不同类型的私有信息检索协议进行量化的特点。
     针对目前缺乏支持私有信息检索的数据库系统的问题,给出了支持私有信息检索的数据库系统设计的形式化分析与验证。在数据库客户端,对用户查询的私有信息检索转换是否满足隐私性要求进行分析验证;在数据库服务器端,从安全模型、形式化顶层规范等分析了数据库系统的设计。采用形式化工具COQ对形式化顶层规范进行了描述,并验证数据库系统行为、尤其是查询操作在服务器端也满足安全模型所规定的安全性质。
With the rapid development of the information communication technology, usingnetwork for information storage and exchange has become a normal style for people’sworking and living. However, because of the complexity of the network environment andthe uncertainty of the user behavior, the client privacy can not be protected well. It isimportant to provide some methods to protect the clients’ private information. Privateinformation retrieval (PIR) was proposed to resolve such a problem: when clients retrievedata from a database, the intension of these queries should be hidden. For the existingproblems in PIR research such as high complexity, short of privacy metric, short ofcombination with database, etc, focusing on the PIR protocol, privacy metric, etc, weconduct deep research on four aspects.
     In order to lower the complexity of PIR protocols, a row based computational PIRprotocol called Robac-PIR is designed, which is improved on quadratic residuosity PIR. InRobac-PIR, queries are made on part of the data instead of the whole data in the server, sothat the client is able to make a tradeoff between privacy and efficiency. Furtherimprovement is made on Robac-PIR to propose a network enviroment PIR scheme. In thisscheme, data blocks are distributed to different client nodes in the network to share thecomputation work and the overall efficiency is increased. The experiments show that ourRobac-PIR protocol and distributed Robac-PIR scheme are flexible and superior inefficiency.
     In order to improve the practicability of PIR protocol, a keyword based PIR scheme isproposed to protect the client privacy in discovery service (DS) of internet of things. ThePIR scheme is based on hash index and well applicable to DS environment. Comparedwith existing client privacy preserving DS architectures, this scheme doesn’t need toworry about the collaboration between servers, complex pre-distribution of keys, and cancompletely protect the client privacy by private information retrieval.
     To resolve the problem that privacy metric is lacked in PIR research, based oninformation theory, the definition and the quantitative method are made for the clientquery privacy in PIR problem. Quantification and analysis are made for our Robac-PIRprotocol and some other existing PIR protocols using the proposed formula of quantifying.Analysis shows that our privacy metric does well for the client query privacy
     Nowadays there isn’t any design of the database system providing PIR query. Toresolve this problem, formal specification and verification are made on the design of thedatabase providing PIR query. On the client side, the PIR transformations for queries areanalysed and verified. On the server side, the model and the formal top-level specification(FTLS) are proposed for the database system. Proof assistant tool COQ is used to specifyand verify the FTLS of the database system, especially the PIR query operation within.The verification shows that the design of the database system and the query operationsatisfies the security properties in the security policy.
引文
[1] Yao A. C. Protocols for Secure Computations. in: Proceedings of the23rd AnnualIEEE Symposium on Foundations of Computer Science, Chicago, IL, USA,1982.New York, NY, USA: IEEE,1982.160~164
    [2] Chor B., Goldreich O., Kushilevitz E., et al. Private Information Retrieval. in:Proceedings of the36th Annual Symposium on Foundations of Computer Science,Milwaukee, WI, USA,1995. Los Alamitos, CA, USA: IEEE,1995.41~50
    [3] Bar-Yossef Z., Gurevich M. Efficient Search Engine Measurements. in: Proceedingsof the16th International World Wide Web Conference, Banff, AB, Canada,2007.New York, NY, USA: ACM,2007.401~410
    [4] Ostrovsky R., Skeith W. E. III. A Survey of Single-Database Private InformationRetrieval: Techniques and Applications. in: Proceeding of the10th InternationalConference on Practice and Theory in Public-Key Cryptography, Beijing, China,2007. Berlin, Germany: Springer,2007.393~411
    [5] Beimel A. Private Information Retrieval: A Primer. Department of Computer Science,Ben-Gurion University,2008
    [6] Yang E. Y., Xu J., Bennett Keith H. Private Information Retrieval in the Presence ofMalicious Failure. in: Proceedings of the26th Annual International ComputerSoftware and Applications Conference, Oxford, United kingdom,2002. LosAlamitos, CA, USA: IEEE,2002.805~810
    [7] Beimel A., Stahl Y. Robust Information-Theoretic Private Information Retrieval. in:Proceedings of the3rd Conference on Security in Communications Networks,Amalfi, Italy,2002. Berlin, Germany: Springer,2002.326~341
    [8] Beimel A., Ishai Y., Kushilevitz E. General Constructions for Information-TheoreticPrivate Information Retrieval. Journal of Computer and System Sciences,2005,71(2):213~247
    [9] Gentry C., Ramzan Z. Single-Database Private Information Retrieval with ConstantCommunication Rate. in: Proceedings of the32nd International Colloquium onAutomata, Languages and Programming, Lisbon, Portugal,2005. Berlin, Germany:Springer,2005.803~815
    [10] Carlos A. M., Philippe G. A Lattice-Based Computationally-Efficient PrivateInformation Retrieval Protocol. in: Western European Workshop on Research inCryptology, Bochum, Germany,2007.1~13
    [11] Chor B., Gilboa N., Naor M. Private Information Retrieval by Keywords. in:Technical Report TR CS0917, Department of Computer Science, Technion,1998
    [12] Olumofin F., Goldberg I. Privacy-Preserving Queries over Relational Databases. in:Proceedings of the10th International Symposium on Privacy EnhancingTechnologies, Berlin, Germany,2010. Heidelberg, Germany: Springer,2010.75~92
    [13] Boneh D., Kushilevitz E., Ostrovsky R., et al. Public Key Encryption that AllowsPIR Queries. in:27th Annual International Cryptology Conference, Santa Barbara,CA, USA,2007. Heidelberg, Germany: Springer,2007.50~67
    [14] Yoshida R., Cui Y., Sekino T., et al. Practical Searching over Encrypted Data byPrivate Information Retrieval. in: Proceedings of the53rd IEEE GlobalCommunications Conference, Miami, FL, USA,2010. New York, NY, USA: IEEE.1~5
    [15] Gertner Y., Ishai Y., Kushilevitz E., et al. Protecting Data Privacy in PrivateInformation Retrieval Schemes. Journal of Computer and Systems Sciences,2000,60(3):592~629
    [16] Ambainis A. Upper Bound on the Communication Complexity of PrivateInformation Retrieval. in: Proceeding of the24th International Colloquium onAutomata, Languages and Programming, Bologna, Italy,1997.401~407
    [17] Beimel A., Ishai Y. Information-Theoretic Private Information Retrieval: A UnifiedConstruction. in: Proceeding of the28th International Colloquium on Automata,Languages and Programming, Crete, Greece,2001. Berlin, Germany: Springer,2001.912~924
    [18] Itoh T. Efficient Private Information Retrieval. IEICE Transactions on Fundamentalsof Eletronics, Communications and Computer Sciences,1999, E82-A(1):11~20
    [19] Ishai Y., Kushilevitz E. Improved Upper Bounds on Information-Theoretic PrivateInformation Retrieval. in: Proceedings of the31st Annual ACM Symposium onTheory of Computing, Atlanta, GA, USA,1999. New York, NY, USA: ACM,1999.79~88
    [20] Beimel A., Ishai Y., Kushilevitz E., et al. Breaking the O(n1/2k-1) Barrier forInformation-Theoretic Private Information Retrieval. in: Proceedings of the34thAnnual IEEE Symposium on Foundations of Computer Science, Vancouver, BC,Canada,2002. Los Alamitos, CA, USA: IEEE,2002.261~270
    [21] Shamir A. How to Share a Secret. Communications of the ACM,1979,22(11):612~613
    [22] Ito M., Saito A., Nishizeki T. Secret Sharing Schemes Realizing General AccessStructure. in: IEEE/IEICE Global Telecommunications Conference1987, Tokyo, Jpn,1987. Tokyo, Jpn: Ohmsha Ltd,1987.99~102
    [23] Chor B., Gilboa N. Computationally Private Information Retrieval. in: Proceedingsof the29th Annual ACM Symposium on Theory of Computing, El Paso, TX, USA,1997. New York, NY, USA: ACM,1997.304~313.
    [24] Kushilevitz E., Ostrovsky R. Replication is Not Needed: Single Database,Computationally-Private Information Retrieval. in: Proceedings of the38th IEEESymposium on Foundations of Computer Science, Miami Beach, FL, USA,1997.Los Alamitos, CA, USA: IEEE,1997.364~373
    [25] Cachin C., Micali S., Stadler M. Computationally Private Information Retrieval withPolylogarithmic Communication. in: International Conference on the Theory andApplication of Cryptographic Techniques, Prague, Czech Republic,1999. Berlin,Germany: Springer,1999.402~414
    [26] Kushilevitz E., Ostrovsky R. One-Way Trapdoor Permutations are Sufficient forNon-Trivial Single-Server Private Information Retrieval. in: Proceedings ofAdvances in Cryptology, Bruges, Belgium,2000. Berlin, Germany: Springer,2000.104~121
    [27] Chang Y. C. Single Database Private Information Retrieval with LogarithmicCommunication. in: Information Security and Privacy:9th Australasian Conference,Sydney, Australia,2004. Berlin, Germany: Springer,2004.50~61
    [28] Lipmaa H. An Oblivious Transfer Protocol with Log-Squared Communication. in:Proceedings of the8th International Conference on Information Security, Singapore,Singapore,2005. Berlin, Germany: Springer,2005.314~328
    [29] Wang S., Agrawal D., El Abbadi A. Generalizing PIR for Practical Private Retrievalof Public Data. in:24th Annual IFIP WG11.3Working Conference on Data andApplications Security and Privacy, Rome, Italy,2010. Heidelberg, Germany:Springer,2010.1~16
    [30] Domingo-Ferrer J., Solanas A., Castella-Roca J. h(k)-Private Information Retrievalfrom Privacy-Uncooperative Queryable Databases. Online Information Review,2009,33(4):720~744
    [31] Goldberg I. Improving the Robustness of Private Information Retrieval. in: IEEESymposium on Security and Privacy, Berkeley, CA, USA,2007. New York, NY,USA: IEEE.131~145
    [32] Blundo C., D’Arco P., De Santis A. A t-Private k-Database Information RetrievalScheme. International Journal of Information Security,2001,1(1):64~68
    [33] Domingo-Ferrer J., Bras-Amorós M., Wu Q., et al. User-Private InformationRetrieval Based on a Peer-to-Peer Community. Data and Knowledge Engineering,2009,68(11):1237~1252
    [34] Stokes K., Bras-Amorós M. Optimal Configurations for Peer-to-Peer User-PrivateInformation Retrieval. Computers and Mathematics with Applications,2010,59(4):1568~1577
    [35] Stokes K., Bras-Amorós M. On Query Self-Submission in Peer-to-Peer User-PrivateInformation Retrieval. in: Proceedings of the4th International Workshop on Privacyand Anonymity in the Information Society, Uppsala, Sweden,2011. New York, NY,USA: ACM,2011. No.7
    [36] Bakiras S., Nikolopoulos K. F. Adjusting the Trade-off between Privacy Guaranteesand Computational Cost in Secure Hardware PIR. in: Proceedings of the8th VLDBWorkshop on Secure Data Management, Seattle, WA, USA,2011. Heidelberg,Germany: Springer,2011.128~144
    [37]李宏佳.相互协作中的私有信息检索方法研究:[硕士学位论文].燕山大学,2009
    [38]蓝天,秦志光,赵洋.一种实用的基于硬件的私有信息检索方案.见:中国计算机大会,天津,中国,2009.317~323
    [39]祁堃,黄刘生,罗永龙,等.一种高效的私有信息检索方案.小型微型计算机系统,2007,28(7):1185~1188
    [40] Agrawal R., Srikant R., Thomas D. Privacy Preserving OLAP. in: Proceedings of theACM SIGMOD International Conference on Management of Data, Baltimore, MD,USA,2005. New York, NY, USA: ACM,2005.251~262
    [41] Zhang N., Zhao W. Distributed Privacy Preserving Information Sharing. in:Proceedings of the31st International Conference on Very Large Data Bases,Trondheim, Norway,2005. New York, NY, USA: ACM,2005.889~900
    [42] Elgamal T. A Public Key Cryptosystem and a Signature Scheme Based on DiscreteLogarithms. IEEE Transactions on Information Theory,1985,31(4):469~472
    [43] Shamir A., Rivest R. L., Adleman L. M. Mental Poker. The Mathematical Gardner,1981.37~43
    [44] Henry R., Olumofin F., Goldberg I. Practical PIR for Electronic Commerce. in:Proceedings of the18th ACM Conference on Computer and CommunicationsSecurity, Chicago, IL, USA,2011. New York, NY, USA: ACM,2011.677~689
    [45] Brassard G., Crepeau C., Robert J. M. All-or-Nothing Disclosure of Secrets. in:Advances in Cryptology-CRYPTO’86, Santa Barbara, CA, USA,1986. Berlin,Germany: Springer,1987.234~238
    [46] Naor M., Pinkast B. Oblivious Transfer and Polynomial Evaluation. in: Proceedingsof the31th Annual ACM Symposium on the Theory of Computing, Atlanta, GA,USA,1999. New York, NY, USA: ACM,1999.245~254
    [47] Di Crescenzo G., Malkin T., Ostrovsky R. Single-Database Private InformationRetrieval Implies Oblivious Transfer. in: Proceedings of Advances in Cryptology,Bruges, Belgium,2000. Berlin, Germany: Springer,2000.122~138
    [48] Yekhanin S. Private Information Retrieval. Communications of the ACM,2010,53(4):68~73
    [49] Ishai Y., Kushilevitz E., Ostrovsky R. Sufficient Conditions for Collision-ResistantHashing. in: Second Theory of Cryptography Conference, Cambridge, MA, USA,2005. Berlin, Germany: Springer,2005.445~456
    [50] Papadopoulos S., Bakiras S., Papadias D. pCloud: A Distributed System for PracticalPIR. IEEE Transactions on Dependable and Secure Computing,2012,9(1):115~127
    [51] DEPARTMENT OF DEFENSE. Trusted Computer System Evaluation Criteria. DoD5200.28-STD, l985
    [52]中华人民共和国国家标准.计算机信息系统安全保护等级划分准则, GB17859-1999
    [53] Common Criteria. Common Criteria for Information Technology Security Evaluation.ISO/IEC15408,1999
    [54] Trostle J., Parrish A. Efficient Computationally Private Information Retrieval fromAnonymity or Trapdoor Groups. in:13th Information Security Conference, BocaRaton, FL, USA,2010. Heidelberg, Germany: Springer,2011.114~128
    [55] Zhong H., Yi L., Zhao Y., et al. Fully-Homomorphic Encryption Based SPIR. in:Proceedings of the7th International Conference on Wireless Communications,Networking and Mobile Computing, Wuhan, China,2011. Piscataway, NJ, USA:IEEE,2011.1~3
    [56] Byun, J. W., Lee D. H. On a Security Model of Conjunctive Keyword Search overEncrypted Relational Database. Journal of Systems and Software,201184(8):1364~1372
    [57] Groth J., Kiayias A., Lipmaa, H. Multi-Query Computationally-Private InformationRetrieval with Constant Communication Rate. in: Proceedings of the13thInternational Conference on Practice and Theory in Public Key Cryptography, Paris,France,2010. Heidelberg, Germany: Springer,2010.107~123
    [58] Rebollo-Monedero D., Forne J. Optimized Query Forgery for Private InformationRetrieval. IEEE Transactions on Information Theory,201056(9):4631~4642
    [59] Asonov D. Querying Databases Privately: A New Approach to Private InformationRetrieval. Monograph review. Berlin, Germany: Springer,2004. xi+113
    [60] Iliev A., Smith S. W. Protecting Client Privacy with Trusted Computing at the Server.IEEE Security and Privacy,2005.3(2):20~28
    [61] Wang S., Ding X., Deng Robert H., et al. Private Information Retrieval UsingTrusted Hardware. in:11th European Symposium on Research in Computer Security,Hamburg, Germany,2006. Berlin Germany: Springer,2006.49~64
    [62] Williams P., Sion R. Usable PIR. in: Proceedings of the15th Annual Network andDistributed System Security Symposium. San Diego, CA, USA,2008.
    [63] Barkol O., Ishai Y., Weinreb E. On Locally Decodable Codes, Self-CorrectableCodes, and t-Private PIR. Algorithmica (New York),2010,58(4):831~859
    [64] Bezzi M. An Entropy Based Method for Measuring Anonymity. in: Proceedings ofthe3rd International Conference on Security and Privacy in CommunicationNetworks, Nice, France,2007. Piscataway, NJ, USA: IEEE,2007.28~32
    [65]柯召,孙琦.数论讲义.第二版.北京,中国:高等教育出版社,2001.94~109
    [66] Botelho F. C., Ziviani N. External Perfect Hashing for Very Large Key Sets. in:Proceedings of the16th ACM Conference on Information and knowledgeManagement, Lisboa, Portugal,2007. New York, NY, USA: ACM,2007.653~662
    [67] Botelho F. C., Pagh R., Ziviani N. Simple and Space-Efficient Minimal Perfect HashFunctions. in: Proceedings of the10th International Workshop on Data Structuresand Algorithms, Halifax, Canada,2007. Heidelberg, Germany: Springer,2007.139~150
    [68] ITU. The Internet of Things. ITU News,2005,(9):13~16
    [69] EPCglobal. EPCglobal Standards. Available from: http://www.gs1.org/epcglobal,2013
    [70]赵文,李信鹏,刘殿兴,等.供应链环境下一种分布式RFID发现服务.电子学报,2010,38(2A):99~106
    [71] European Data Protection Supervisor. Opinion of the European Data ProtectionSupervisor on Promoting Trust in the Information Society by Fostering DataProtection and Privacy. Available from: http://www.edps.europa.eu,2013
    [72] EPCglobal. EPCglobal Tag Data Standards Version1.3.2006.25~31
    [73] Kaya S. V., Savas E., Levi A., et al. Public Key Cryptography Based PrivacyPreserving Multi-Context RFID Infrastructure. Ad Hoc Networks,2009,7(1):136~152
    [74] Zuo Y. Secure and Private Search Protocols for RFID Systems. Information SystemsFrontiers,2010,12(5):507~519
    [75] Khor J. H., Ismail W., Mohammed I. Y., et al. Security Problems in an RFID System.Wireless Personal Communications,2011,59(1):17~26
    [76] Shi J., Sim D., Li Y., et al. Secds: A Secure epc Discovery Service System inEpcglobal Network. in: Proceedings of the2nd ACM conference on Data andApplication Security and Privacy, San Antonio, TX, USA,2012. New York, NY,USA: ACM,2012.267~274
    [77] Grummt E., Müller M. Fine-Grained Access Control for epc Information Services. in:Proceedings of the1st International Conference on The Internet of Things, Zurich,Switzerland,2008. Heidelberg, Germany: Springer,2008.35~49
    [78] Shi J., Li Y., He W., et al. SecTTS: A Secure Track&Trace System forRFID-Enabled Supply Chains. Computers in Industry,2012,63(6):574~585.
    [79] Kerschbaum F., Oertel N., Weiss Ferreira Chaves L. Privacy-PreservingComputation of Benchmarks on Item-Level Data Using RFID. in: Proceedings of the3rd ACM Conference on Wireless Network Security, Hoboken, NJ, USA,2010. NewYork, NY, USA: ACM,2010.105~110
    [80] Fabian B., Günther O. Distributed ONS and its Impact on Privacy. in:2007IEEEInternational Conference on Communications, Glasgow, Scotland, United kingdom,2007. Piscataway, NJ, USA: IEEE,2007.1223~1228
    [81] Fabian B., Ermakova T., Muller C. SHARDIS: A Privacy-Enhanced DiscoveryService for RFID-Based Product Information. IEEE Transactions on IndustrialInformatics,2012,8(3):707~718
    [82] Scannapieco M., Figotin I., Bertino E., et al. Privacy Preserving Schema and DataMatching. in: Proceedings of the ACM SIGMOD International Conference onManagement of Data, Beijing, China,2007. New York, NY, USA: ACM,2007.653~664
    [83] Ghani N. A., Sidek Z. M. Hippocratic Database: A Privacy-Aware Database. WorldAcademy of Science, Engineering and Technology,2008.249~253
    [84] Freedman M.J., Nissim K., Pinkas B. Efficient Private Matching and Set Intersection.in: International Conference on the Theory and Applications of CryptographicTechniques, Interlaken, Switzerland,2004. Berlin, Germany: Springer,2004.1~19
    [85] Olumofin F., Goldberg I. Revisiting the Computational Practicality of PrivateInformation Retrieval. in: Proceedings of the15th International Conference onFinancial Cryptography and Data Security, Gros Islet, Saint lucia,2011. Heidelberg,Germany: Springer,2011.158~172
    [86] Nakamura T., Inenaga S., Ikeda D., et al. Password Based AnonymousAuthentication with Private Information Retrieval. Journal of Digital InformationManagement,2011,9(2):72~78
    [87] Evdokimov S., Fabian B., Kunz S., et al. Comparison of Discovery ServiceArchitectures for the Internet of Things. in:2010IEEE International Conference onSensor Networks, Ubiquitous, and Trustworthy Computing, Newport Beach, CA,USA,2010. Piscataway, NJ, USA: IEEE,2010.237~244
    [88] Fabian B., Günther O. Security Challenges of the Epcglobal Network.Communications of the ACM,2009,52(7):121~125
    [89] VeriSign. The EPC Network: Enhancing the Supply Chain. A VeriSign White Paper,2004.1~10
    [90] Kelepouris T., Harrison M., McFarlane D. Enhanced Supply Chain Tracking Basedon the EPC Network: A Bayesian Approach. in: Proceedings of the13th IFACSymposium on Information Control Problems in Manufacturing, Moscow, Russia,2009. Laxenburg, Australia: IFAC,2009.2071~2076
    [91] Shi J., Li Y., Deng R. H. A Secure and Efficient Discovery Service System inEPCglobal Network. Computers and Security,2012,31(8):870~885
    [92] Nguyen L.T., Yee W. G., Jia D., et al. A Tool for Information Retrieval Research inPeer-to-Peer File Sharing Systems. in: Proceedings of the23rd InternationalConference on Data Engineering, Istanbul, Turkey,2007. Piscataway, NJ, USA:IEEE,2007.1525~1526
    [93]沈连丰,叶芝慧.信息论与编码.第一版.北京,中国:科学出版社,2004.12~29
    [94] Lunt T. F., Denning D. E., Schell R. R., et al. The SeaView Security Model. IEEETransactions on Software Engineering,1990,16(6):593~607
    [95] Whitehurst R. A., Lunt T. F. The SeaView Verification. in: Proceedings of theComputer Security Foundations Workshop II, Franconia, NH, USA,1989.Washington, DC, USA: IEEE,1989.125~132
    [96] Lunt T. F., Denning D. E., Neumann P. G., et al. Final Report vol.1: Security Policyand Policy Interpretation for a Class A1Multilevel Secure Relational DatabaseSystem. Computer Science Lab, SRI International,1988
    [97] LaPadula L. J., Bell D. E. MITRE Technical Report2547, Volume II [Securecomputer systems: rules of operation]. Journal of Computer Security,1996,4(2-3):239~263
    [98] Zhu H., Zhu Y., Li C., et al. Formal Specification and Verification of an ExtendedSecurity Policy Model for Database Systems. in: Proceedings of the3rd Asia-PacificTrusted Infrastructure Technologies Conference, Wuhan, Hubei, China,2008.Piscataway, NJ, USA: IEEE,2008.132~141
    [99] Maximiliano Cristia. Formal Verification of an Extension of a Secure, CompatibleUNIX File System:[Master's thesis]. Instituto de Computación, Universidad de laRepública, Uruguay,2002
    [100]Coronato A., De Pietro G.. Formal Specification and Verification of Ubiquitous andPervasive Systems. ACM Transactions on Autonomous and Adaptive Systems,2011,6(1):103~112
    [101]李海龙,张维明,肖卫东,等.通用标准SQL语法分析模型.小型微型计算机系统,2003,24(11):1969~1972
    [102]The Coq Development Team. The Coq Proof Assistant Reference Manual,2006.23~316

© 2004-2018 中国地质图书馆版权所有 京ICP备05064691号 京公网安备11010802017129号

地址:北京市海淀区学院路29号 邮编:100083

电话:办公室:(+86 10)66554848;文献借阅、咨询服务、科技查新:66554700