{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:04:02Z","timestamp":1725566642918},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540235637"},{"type":"electronic","value":"9783540301912"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30191-2_20","type":"book-chapter","created":{"date-parts":[[2010,9,22]],"date-time":"2010-09-22T16:14:16Z","timestamp":1285172056000},"page":"249-261","source":"Crossref","is-referenced-by-count":3,"title":["Automatic Covert Channel Analysis of a Multilevel Secure Component"],"prefix":"10.1007","author":[{"given":"Ruggero","family":"Lanotte","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Maggiolo-Schettini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Simone","family":"Tini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Angelo","family":"Troina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Enrico","family":"Tronci","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"20_CR1","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1145\/132271.132276","volume":"17","author":"R.K. Abbott","year":"1992","unstructured":"Abbott, R.K., Garcia-Molina, H.: Scheduling Real-Time Transactions: a Performance Evaluation. ACM Trans. Database Syst.\u00a017(3), 513\u2013560 (1992)","journal-title":"ACM Trans. Database Syst."},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"Bell, D., La Padula, L.J.: Secure Computer Systems: Unified Exposition and Multics Interpretation. Tech. Rep. ESD-TR-75-301, MITRE MTR-2997 (1976)","DOI":"10.21236\/ADA023588"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"David, R., Son, S.H.: A Secure Two Phase Locking Protocol. In: Proc. IEEE Symp. on Reliable Distributed Systems, pp. 126\u2013135 (1993)","DOI":"10.1109\/RELDIS.1993.393466"},{"key":"20_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/978-3-540-39724-3_34","volume-title":"Correct Hardware Design and Verification Methods","author":"G. Penna Della","year":"2003","unstructured":"Della Penna, G., Intrigila, B., Melatti, I., Tronci, E., Zilli, M.V.: Finite Horizon Analysis of Markov Chains with the Murphi Verifier. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 394\u2013409. Springer, Heidelberg (2003)"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-540-45208-9_6","volume-title":"Theoretical Computer Science","author":"G. Penna Della","year":"2003","unstructured":"Della Penna, G., Intrigila, B., Melatti, I., Tronci, E., Zilli, M.V.: Finite Horizon Analysis of Stochastic Systems with the Murphi Verifier. In: Blundo, C., Laneve, C. (eds.) ICTCS 2003. LNCS, vol.\u00a02841, pp. 58\u201371. Springer, Heidelberg (2003)"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Dill, D.L., Drexler, A.J., Hu, A.J., Han Yang, C.: Protocol Verification as a Hardware Design Aid. In: Proc. IEEE Int. Conf. on Computer Design on VLSI in Computer & Processors, pp. 522\u2013525 (1992)","DOI":"10.1109\/ICCD.1992.276232"},{"key":"20_CR7","volume-title":"Transaction Processing: Concepts and Techniques","author":"J. Gray","year":"1992","unstructured":"Gray, J., Reuter, A.: Transaction Processing: Concepts and Techniques. Morgan Kaufmann Publishers Inc., San Francisco (1992)"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"Kang, M.H., Froscher, J., Moskowitz, I.S.: A Framework for MLS Interoperability. In: Proc. IEEE High Assurance Systems Engineering Workshop, pp. 198\u2013205 (1996)","DOI":"10.21236\/ADA465306"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Kang, M.H., Froscher, J., Moskowitz, I.S.: An Architecture for Multilevel Security Interoperability. In: Proc. IEEE Computer Security Application Conf. (1997)","DOI":"10.21236\/ADA462626"},{"issue":"4","key":"20_CR10","doi-asserted-by":"crossref","first-page":"56","DOI":"10.1109\/2.666843","volume":"31","author":"M.H. Kang","year":"1998","unstructured":"Kang, M.H., Moore, A.P., Moskowitz, I.S.: Design and Assurance Strategy for the NRL Pump. IEEE Computer\u00a031(4), 56\u201364 (1998)","journal-title":"IEEE Computer"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Kang, M.H., Moskowitz, I.S.: A Pump for Rapid, Reliable, Secure Communication. In: Proc. ACM Conf. on Computer and Communication Security, pp. 119\u2013129 (1993)","DOI":"10.1145\/168588.168604"},{"issue":"5","key":"20_CR12","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1109\/32.502225","volume":"22","author":"M.H. Kang","year":"1996","unstructured":"Kang, M.H., Moskowitz, I.S., Lee, D.: A Network Pump. IEEE Trans. Software Eng.\u00a022(5), 329\u2013338 (1996)","journal-title":"IEEE Trans. Software Eng."},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Moskowitz, I.S., Miller, A.R.: The Channel Capacity of a Certain Noisy Timing Channel. IEEE Trans. Information Theory\u00a038(4) (1992)","DOI":"10.1109\/18.144712"},{"key":"20_CR14","unstructured":"PRISM Web Page, http:\/\/www.cs.bham.ac.uk\/~dxp\/prism\/"},{"key":"20_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/3-540-46029-2_13","volume-title":"Computer Performance Evaluation","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic Symbolic Model Checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol.\u00a02324, pp. 200\u2013204. Springer, Heidelberg (2002)"},{"key":"20_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/3-540-46002-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, p. 52. Springer, Heidelberg (2002)"},{"key":"20_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1007\/3-540-36575-3_2","volume-title":"Programming Languages and Systems","author":"C. Meadows","year":"2003","unstructured":"Meadows, C.: What Makes a Cryptographic Protocol Secure? The Evolution of Requirements Specification in Formal Cryptographic Protocol Analysis. In: Degano, P. (ed.) ESOP 2003. LNCS, vol.\u00a02618, pp. 10\u201321. Springer, Heidelberg (2003)"},{"key":"20_CR18","unstructured":"Mitchell, J.C., Mitchell, M., Stern, U.: Automated Analysis of Cryptographic Protocols using Mur\u03d5. In: Proc. IEEE Symp. on Security and Privacy, pp. 141\u2013151 (1997)"},{"key":"20_CR19","unstructured":"Mitchell, J.C., Shmatikov, V., Stern, U.: Finite-State Analysis of SSL 3.0. In: Proc. USENIX Security Symp. (1998)"},{"issue":"6","key":"20_CR20","doi-asserted-by":"publisher","first-page":"865","DOI":"10.1109\/69.895799","volume":"12","author":"S.H. Son","year":"2000","unstructured":"Son, S.H., Mukkamala, R., David, R.: Integrating Security and Real-Time Requirements Using Covert Channel Capacity. IEEE Trans. Knowl. Data Eng.\u00a012(6), 865\u2013879 (2000)","journal-title":"IEEE Trans. Knowl. Data Eng."},{"key":"20_CR21","unstructured":"Murphi Web Page, http:\/\/sprout.stanford.edu\/dill\/murphi.html"},{"key":"20_CR22","unstructured":"Cached Murphi Web Page, http:\/\/www.dsi.uniroma1.it\/~tronci\/cached.murphi.html"}],"container-title":["Lecture Notes in Computer Science","Information and Communications Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30191-2_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T23:46:32Z","timestamp":1605743192000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30191-2_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540235637","9783540301912"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30191-2_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}