{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T21:33:12Z","timestamp":1648848792827},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"7","license":[{"start":{"date-parts":[[2011,10,17]],"date-time":"2011-10-17T00:00:00Z","timestamp":1318809600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Sci. China Inf. Sci."],"published-print":{"date-parts":[[2012,7]]},"DOI":"10.1007\/s11432-011-4372-y","type":"journal-article","created":{"date-parts":[[2011,10,16]],"date-time":"2011-10-16T23:53:03Z","timestamp":1318809183000},"page":"1650-1665","source":"Crossref","is-referenced-by-count":1,"title":["Symbolic algorithmic verification of intransitive generalized noninterference"],"prefix":"10.1007","volume":"55","author":[{"given":"CongHua","family":"Zhou","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"ZhiFeng","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"HaiLing","family":"Wu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Song","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"ShiGuang","family":"Ju","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,10,17]]},"reference":[{"key":"4372_CR1","first-page":"139","volume":"40","author":"C. X. Shen","year":"2010","unstructured":"Shen C X, Zhang H G, Wang H M, et al. Trusted computing research and development (in Chinese). Sci China Inf Sci, 2010, 40: 139\u2013166","journal-title":"Sci China Inf Sci"},{"key":"4372_CR2","first-page":"167","volume":"40","author":"H. G. Zhang","year":"2010","unstructured":"Zhang H G, Yan F, Fu J M, et al. Theory and key technology evaluation of trusted computing platform (in Chinese). Sci China Inf Sci, 2010, 40: 167\u2013188","journal-title":"Sci China Inf Sci"},{"key":"4372_CR3","doi-asserted-by":"crossref","first-page":"550","DOI":"10.1109\/32.629493","volume":"27","author":"R. Focardi","year":"1997","unstructured":"Focardi R, Gorrieri R. The compositional security checker: a tool for the verification of information flow security properties. IEEE Trans Softw Eng, 1997, 27: 550\u2013571","journal-title":"IEEE Trans Softw Eng"},{"key":"4372_CR4","first-page":"238","volume":"37","author":"S. H. Qing","year":"2007","unstructured":"Qing S H, Shen C X. Design on high secure operating system (in Chinese). Sci China Ser E-Tech Sci, 2007, 37: 238\u2013253","journal-title":"Sci China Ser E-Tech Sci"},{"key":"4372_CR5","first-page":"153","volume":"35","author":"W. Q. Liu","year":"2007","unstructured":"Liu W Q, Han N P, Chen Z. Identifying and dealing with covert channel of the secure OS-SLinux (in Chinese). ACTA Electron Sin, 2007, 35: 153\u2013156","journal-title":"ACTA Electron Sin"},{"key":"4372_CR6","first-page":"1837","volume":"15","author":"S. H. Qing","year":"2004","unstructured":"Qing S H. Covert channel analysis in secure operating systems with high security levels. J Softw, 2004, 15: 1837\u20131849","journal-title":"J Softw"},{"key":"4372_CR7","first-page":"11","volume-title":"IEEE Symposium On Security and Privacy","author":"J. A. Goguen","year":"1982","unstructured":"Goguen J A, Meseguer J. Security policies and security models. In: Peter G N, Robert M, eds. IEEE Symposium On Security and Privacy. Washington: IEEE Computer Society Press, 1982. 11\u201320"},{"key":"4372_CR8","first-page":"161","volume-title":"IEEE Symposium On Security and Privacy","author":"M. Daryl","year":"1987","unstructured":"Daryl M. Specifications for multi-level security and a hook-up property. In: David B, Steve L, eds. IEEE Symposium On Security and Privacy. Washington: IEEE Computer Society Press, 1987. 161\u2013166"},{"key":"4372_CR9","unstructured":"Rushby J M. Noninterference, Transitivity, and Channel Control Security Policies. Technical Report CSL-92-02, SRI International, 1992"},{"key":"4372_CR10","first-page":"75","volume-title":"IEEE Symposium On Security and Privacy","author":"J. A. Goguen","year":"1984","unstructured":"Goguen J A, Meseguer J. Unwinding and inference control. In: Dorothy E D, Jonathan K M, eds. IEEE Symposium On Security and Privacy. Washington: IEEE Computer Society Press, 1984. 75\u201386"},{"key":"4372_CR11","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1016\/j.entcs.2005.06.005","volume":"135","author":"D. Deepak","year":"2005","unstructured":"Deepak D, Raghavendra K R, Barbara S. An automata based approach for verifying information flow properties. Elec Note Theor Comput Sci, 2005, 135: 39\u201358","journal-title":"Elec Note Theor Comput Sci"},{"key":"4372_CR12","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/j.entcs.2006.11.002","volume":"168","author":"M. Ron","year":"2007","unstructured":"Ron M, Zhang C Y. Algorithmic verification of noninterference properties. Elec Note Theor Comput Sci, 2007, 168: 61\u201375","journal-title":"Elec Note Theor Comput Sci"},{"key":"4372_CR13","first-page":"1460","volume":"29","author":"X. C. Zi","year":"2006","unstructured":"Zi X C, Yao L H, Li L. A state-based approach to information flow analysis (in Chinese). Chinese J Comput, 2006, 29: 1460\u20131467","journal-title":"Chinese J Comput"},{"key":"4372_CR14","first-page":"61","volume":"3569","author":"N. Een","year":"2005","unstructured":"Een N, Biere A. Effective preprocessing in SAT through variable and clause elimination. LNCS, 2005, 3569: 61\u201375","journal-title":"LNCS"},{"key":"4372_CR15","first-page":"453","volume":"3258","author":"G. Pan","year":"2004","unstructured":"Pan G, Vardi M Y. Symbolic decision procedures for QBF. LNCS, 2004, 3258: 453\u2013567","journal-title":"LNCS"},{"key":"4372_CR16","first-page":"59","volume":"3542","author":"A. Biere","year":"2005","unstructured":"Biere A. Resolve and expand. LNCS, 2005, 3542: 59\u201370","journal-title":"LNCS"},{"key":"4372_CR17","first-page":"348","volume":"2833","author":"P. G. Ian","year":"2003","unstructured":"Ian P G, Holger H H, Andrew G D R, et al. Using stochastic local search to solve quantified Boolean formulae. LNCS, 2003, 2833: 348\u2013362","journal-title":"LNCS"},{"key":"4372_CR18","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/s11390-007-9004-z","volume":"22","author":"Z. H. Tao","year":"2007","unstructured":"Tao Z H, Zhou C H, Chen Z, et al. Bounded model checking of CTL*. J Comput Sci Technol, 2007, 22: 39\u201343","journal-title":"J Comput Sci Technol"},{"key":"4372_CR19","first-page":"386","volume":"4484","author":"C. H. Zhou","year":"2007","unstructured":"Zhou C H, Chen Z Y, Tao Z H. QBF based symbolic model checking for knowledge and time. LNCS, 2007, 4484: 386\u2013397","journal-title":"LNCS"},{"key":"4372_CR20","doi-asserted-by":"crossref","first-page":"27","DOI":"10.3724\/SP.J.1001.2008.00027","volume":"19","author":"W. X. Qu","year":"2008","unstructured":"Qu W X, Li T, Guo Y, et al. Advances in predicate abstraction (in Chinese). J Softw, 2008, 19: 27\u201338","journal-title":"J Softw"}],"container-title":["Science China Information Sciences"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-011-4372-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11432-011-4372-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-011-4372-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T15:36:15Z","timestamp":1559403375000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11432-011-4372-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,10,17]]},"references-count":20,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2012,7]]}},"alternative-id":["4372"],"URL":"https:\/\/doi.org\/10.1007\/s11432-011-4372-y","relation":{},"ISSN":["1674-733X","1869-1919"],"issn-type":[{"value":"1674-733X","type":"print"},{"value":"1869-1919","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,10,17]]}}}