{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,15]],"date-time":"2025-03-15T04:06:01Z","timestamp":1742011561195,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":50,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642252822"},{"type":"electronic","value":"9783642252839"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-25283-9_5","type":"book-chapter","created":{"date-parts":[[2011,11,17]],"date-time":"2011-11-17T16:31:18Z","timestamp":1321547478000},"page":"67-86","source":"Crossref","is-referenced-by-count":2,"title":["Modeling TCG-Based Secure Systems with Colored Petri Nets"],"prefix":"10.1007","author":[{"given":"Liang","family":"Gu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yao","family":"Guo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yanjiang","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Feng","family":"Bao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hong","family":"Mei","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-30232-2_1","volume-title":"Formal Techniques for Networked and Distributed Systems \u2013 FORTE 2004","author":"M. Abadi","year":"2004","unstructured":"Abadi, M., Wobber, T.: A Logical Account of NGSCB. In: de Frutos-Escrig, D., N\u00fa\u00f1ez, M. (eds.) FORTE 2004. LNCS, vol.\u00a03235, pp. 1\u201312. Springer, Heidelberg (2004)"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Ahmed, T., Tripathi, A.R.: Static verification of security requirements in role based cscw systems. In: The Eighth ACM Symposium on Access Control Models and Technologies (SACMAT), pp. 196\u2013203 (2003)","DOI":"10.1145\/775412.775438"},{"key":"5_CR3","unstructured":"AMD. AMD64 Virtualization Codenamed Pacifica Technology\u2013Secure Virtual Machine Architecture Reference Manual. Technical Report Publication Number 33047, Revision 3.01, AMD (May 2005)"},{"key":"5_CR4","unstructured":"AMD. Amd64 architecture programmer\u2019s manual, vol. 2: System programming (2007)"},{"key":"5_CR5","unstructured":"Berger, S., Caceres, R., Goldman, K.A., Perez, R., Sailer, R., van Doorn, L.: vTPM: Virtualizing the Trusted Platform Module. In: Proceedings of the 15th USENIX Security Symposium, pp. 305\u2013320. USENIX (August 2006)"},{"key":"5_CR6","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1145\/1346281.1346286","volume-title":"Proceedings of the 13th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2008)","author":"R. Bhargava","year":"2008","unstructured":"Bhargava, R., Serebrin, B., Spadini, F., Manne, S.: Accelerating two-dimensional page walks for virtualized systems. In: Proceedings of the 13th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2008), Seattle, WA, USA, pp. 26\u201335. ACM, New York (March 2008)"},{"key":"5_CR7","first-page":"127","volume-title":"ACSAC","author":"D. Bruschi","year":"2005","unstructured":"Bruschi, D., Cavallaro, L., Lanzi, A., Monga, M.: Replay attack in TCG specification and solution. In: ACSAC, pp. 127\u2013137. IEEE Computer Society, Los Alamitos (2005)"},{"key":"5_CR8","first-page":"7","volume-title":"STC 2006","author":"L. Chen","year":"2006","unstructured":"Chen, L., Landfermann, R., L\u00f6hr, H., Rohe, M., Sadeghi, A.-R., St\u00fcble, C.: A protocol for property-based attestation. In: STC 2006, pp. 7\u201316. ACM Press, New York (2006)"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/978-3-540-73547-2_37","volume-title":"Autonomic and Trusted Computing","author":"S.-Y. Chen","year":"2007","unstructured":"Chen, S.-Y., Wen, Y., Zhao, H.: Formal analysis of secure bootstrap in trusted computing. In: Xiao, B., Yang, L.T., Ma, J., Muller-Schloer, C., Hua, Y. (eds.) ATC 2007. LNCS, vol.\u00a04610, pp. 352\u2013360. Springer, Heidelberg (2007)"},{"key":"5_CR10","unstructured":"CPN group at the Department of Computer Science in University of Aarhus. Examples of Industrial Use of CP-nets (2010), http:\/\/www.daimi.au.dk\/CPnets\/intro\/example_indu.html"},{"key":"5_CR11","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1016\/j.entcs.2007.02.012","volume":"172","author":"A. Datta","year":"2007","unstructured":"Datta, A., Derek, A., Mitchell, J.C., Roy, A.: Protocol Composition Logic (PCL). Electron. Notes Theor. Comput. Sci.\u00a0172, 311\u2013358 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"5_CR12","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1109\/SP.2009.16","volume-title":"Proceedings of the 2009 30th IEEE Symposium on Security and Privacy","author":"A. Datta","year":"2009","unstructured":"Datta, A., Franklin, J., Garg, D., Kaynar, D.: A logic of secure systems and its application to trusted computing. In: Proceedings of the 2009 30th IEEE Symposium on Security and Privacy, pp. 221\u2013236. IEEE Computer Society, Washington, DC, USA (2009)"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Garfinkel, T., Pfaff, B., Chow, J., Rosenblum, M., Boneh, D.: Terra: A Virtual Machine-Based Platform for Trusted Computing. In: SOSP 2003, Bolton Landing, New York, USA, October 19-22 (2003)","DOI":"10.1145\/945445.945464"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Garg, D., Franklin, J., Kaynar, D., Datta, A.: Compositional system security with interface-confined adversaries. In: Mathematical Foundations of Programming Semantics (MFPS) Conference (April 6, 2010)","DOI":"10.1016\/j.entcs.2010.08.005"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-642-14597-1_4","volume-title":"Trusted Systems","author":"L. Gu","year":"2010","unstructured":"Gu, L., Cheng, Y., Ding, X., Deng, R.H., Guo, Y., Shao, W.: Remote attestation on function execution. In: Chen, L., Yung, M. (eds.) INTRUST 2009. LNCS, vol.\u00a06163, pp. 60\u201372. Springer, Heidelberg (2010)"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Gu, L., Ding, X., Deng, R.H., Xie, B., Mei, H.: Remote attestation on program execution. In: ACM workshop on Scalable Trusted Computing (STC), held in conjunction with the 15th ACM Conference on Computer and Communications Security (ACM CCS 2008) (2008)","DOI":"10.1145\/1456455.1456458"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Gu, L., Ding, X., Deng, R.H., Xie, B., Mei, H.: Remote platform attestation - the testimony for trust management. In: Yan, Z. (ed.) Trust Modeling and Management in Digital Environments: from Social Concept to System Development. IGI Global (2010), doi:10.4018\/978-1-61520-682-7, ISBN-13: 978-1615206827","DOI":"10.4018\/978-1-61520-682-7"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/978-3-540-74835-9_29","volume-title":"Computer Security \u2013 ESORICS 2007","author":"S. G\u00fcrgens","year":"2007","unstructured":"G\u00fcrgens, S., Rudolph, C., Scheuermann, D., Atts, M., Plaga, R.: Security Evaluation of Scenarios Based on the TCG\u2019s TPM Specification. In: Biskup, J., L\u00f3pez, J. (eds.) ESORICS 2007. LNCS, vol.\u00a04734, pp. 438\u2013453. Springer, Heidelberg (2007)"},{"key":"5_CR19","unstructured":"Intel Corporation. Intel Trusted Execution Technology \u2014 Preliminary Architecture Specification. Technical Report Document Number: 31516803, Intel Corporation (2006)"},{"key":"5_CR20","unstructured":"Intel Corporation. Intel Virtualization Technology for Directed I\/O Architecture Specification. Technical Report Order Number: D51397-001, Intel Corporation (February 2006)"},{"key":"5_CR21","first-page":"19","volume-title":"SACMAT 2006","author":"T. Jaeger","year":"2006","unstructured":"Jaeger, T., Sailer, R., Shankar, U.: PRIMA: policy-reduced integrity measurement architecture. In: SACMAT 2006, pp. 19\u201328. ACM Press, New York (2006)"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"248","DOI":"10.1007\/978-3-540-47919-2_10","volume-title":"Advances in Petri Nets 1986. Proceedings of an Advanced Course, Bad Honnef, 8.-19. September 1986","author":"K. Jensen","year":"1987","unstructured":"Jensen, K.: Colored Petri Nets. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) APN 1986. LNCS, vol.\u00a0254, pp. 248\u2013299. Springer, Heidelberg (1987)"},{"key":"5_CR23","series-title":"EATCS Monographs on Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-06289-0","volume-title":"Coloured Petri Nets : Basic Concepts, Analysis Methods and Practical Use","author":"K. Jensen","year":"1992","unstructured":"Jensen, K.: Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use. EATCS Monographs on Theoretical Computer Science, vol.\u00a01. Springer, Heidelberg (1992)"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-48654-1","volume-title":"A Decade of Concurrency","author":"K. Jensen","year":"1994","unstructured":"Jensen, K.: An Introduction to the Theoretical Aspects of Coloured Petri Nets. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1993. LNCS, vol.\u00a0803. Springer, Heidelberg (1994)"},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"Y.\u00a0Jiang, C.\u00a0Lin, H.\u00a0Yin, and Z.\u00a0Tan. Security analysis of mandatory access control model. In IEEE International Conference on Systems, Man and Cybernetics, volume vol. 6, page 5013\u20135018, 2004.","DOI":"10.1109\/ICSMC.2004.1400987"},{"key":"5_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/3-540-61363-3_14","volume-title":"Application and Theory of Petri Nets 1996","author":"J.B. J\u00f8rgensen","year":"1996","unstructured":"J\u00f8rgensen, J.B., Mortensen, K.H.: Modelling and Analysis of Distributed Program Execution in BETA Using Coloured Petri Nets. In: Billington, J., Reisig, W. (eds.) ICATPN 1996. LNCS, vol.\u00a01091, pp. 249\u2013268. Springer, Heidelberg (1996)"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Katt, B., Hafner, M., Zhang, X.: Building a stateful reference monitor with Coloured Petri Nets. In: CollaborateCom, pp. 1\u201310 (2009)","DOI":"10.4108\/ICST.COLLABORATECOM2009.8375"},{"key":"5_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"905","DOI":"10.1007\/978-3-642-05151-7_11","volume-title":"On the Move to Meaningful Internet Systems: OTM 2009","author":"B. Katt","year":"2009","unstructured":"Katt, B., Zhang, X., Hafner, M.: Towards a Usage Control Policy Specification with Petri Nets. In: Meersman, R., Dillon, T., Herrero, P. (eds.) OTM 2009. LNCS, vol.\u00a05871, pp. 905\u2013912. Springer, Heidelberg (2009)"},{"key":"5_CR29","first-page":"1","volume-title":"Proceedings of 16th USENIX Security Symposium","author":"B. Kauer","year":"2007","unstructured":"Kauer, B.: OSLO: improving the security of trusted computing. In: Proceedings of 16th USENIX Security Symposium, pp. 1\u20139. USENIX Association, Berkeley (2007)"},{"key":"#cr-split#-5_CR30.1","doi-asserted-by":"crossref","unstructured":"14. Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. In: Proceedings of the 22nd Symposium on Operating Systems Principles (SOSP 2009), Operating Systems Review","DOI":"10.1145\/1629575.1629596"},{"key":"#cr-split#-5_CR30.2","unstructured":"15. (OSR), Big Sky, MT, pp. 207-220. ACM SIGOPS (October 2009)"},{"key":"5_CR31","doi-asserted-by":"crossref","unstructured":"Knorr, K.: Dynamic access control through Petri Net workflows. In: 16th Annual Computer Security Applications Conference (ACSAC), page 159 (2000)","DOI":"10.1109\/ACSAC.2000.898869"},{"key":"5_CR32","volume-title":"Object Oriented Programming in the Beta Programming Language","author":"O.L. Madsen","year":"1993","unstructured":"Madsen, O.L., Moller-Pedersen, B., Nygaard, K.: Object Oriented Programming in the Beta Programming Language. Addison-Wesley Publishing Company, Reading (1993)"},{"key":"5_CR33","doi-asserted-by":"crossref","unstructured":"McCune, J.M., Li, Y., Qu, N., Zhou, Z., Datta, A., Gligor, V., Perrig, A.: TrustVisor: Efficient TCB Reduction and Attestation. In: IEEE Symposium on Security and Privacy (2010)","DOI":"10.1109\/SP.2010.17"},{"key":"5_CR34","first-page":"315","volume-title":"3rd ACM SIGOPS\/EuroSys European Conference on Computer Systems","author":"J.M. McCune","year":"2008","unstructured":"McCune, J.M., Parno, B.J., Perrig, A., Reiter, M.K., Isozaki, H.: Flicker: an execution infrastructure for TCB minimization. In: 3rd ACM SIGOPS\/EuroSys European Conference on Computer Systems, pp. 315\u2013328. ACM, New York (2008), 1352625"},{"key":"5_CR35","unstructured":"Microsoft Corporation. BitLocker Drive Encryption: Technical Overview. New (optionally) TPM-based secure boot and filesystem encryption from MS Vista (2006)"},{"key":"5_CR36","unstructured":"Poritz, J., Schunter, M., Van Herreweghen, E., Waidner, M.: Property attestation\u2014scalable and privacy-friendly security assessment of peer computers. Technical Report RZ 3548, IBM Research (May 2004)"},{"key":"5_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-642-01004-0_9","volume-title":"Transactions on Computational Science IV","author":"H. Rakkay","year":"2009","unstructured":"Rakkay, H., Boucheneb, H.: Security analysis of role based access control models using colored petri nets and CPNtools. In: Gavrilova, M.L., Tan, C.J.K., Moreno, E.D. (eds.) Transactions on Computational Science IV. LNCS, vol.\u00a05430, pp. 149\u2013176. Springer, Heidelberg (2009)"},{"key":"5_CR38","doi-asserted-by":"crossref","unstructured":"Sadeghi, A.-R., Selhorst, M., St\u00fcble, C., Wachsmann, C., Winandy, M.: TCG inside?: a note on TPM specification compliance, pp. 47\u201356 (2006), 1179487","DOI":"10.1145\/1179474.1179487"},{"key":"5_CR39","unstructured":"Sadeghi, A.-R., St\u00fcble, C.: Property-based attestation for computing platforms: caring about properties, not mechanisms. New Security Paradigms (2004)"},{"key":"5_CR40","unstructured":"Sailer, R., Zhang, X., Jaeger, T., van Doorn, L.: Design and Implementation of a TCG-based Integrity Measurement Architecture. In: Proceedings of the 13th USENIX Security Symposium, San Diego, CA, USA, August 9-13 (2004)"},{"key":"5_CR41","unstructured":"Shi, E., Perrig, A.: Van Doorn, L.: BIND: A Fine-Grained Attestation Service for Secure Distributed Systems. In: 2005 IEEE Symposium on Security and Privacy, S&P 2005 (2005)"},{"key":"5_CR42","unstructured":"Shin, W.: An extension of role based access control for trusted operating systems and its coloured petri net model, PhD thesis. Gwangju Institute of Science and Technology, Korea (2005), http:\/\/itslab.csce.kyushu-u.ac.jp\/ssr\/SSR-1\/thesis-main.pdf"},{"key":"5_CR43","doi-asserted-by":"crossref","unstructured":"Trusted\u00a0Computing Group. TPM main specification. Main Specification Version 1.2 rev. 85, Trusted Computing Group (February 2005)","DOI":"10.1049\/PBPC006E_ch1"},{"key":"5_CR44","unstructured":"Trusted Computing Group. TCG Specification Architecture Overview (Revision 1.4) (2007)"},{"key":"5_CR45","doi-asserted-by":"crossref","unstructured":"Varadharajan, V.: Hook-up property for information flow secure nets. In: Computer Security Foundations Workshop IV, pp. 154\u2013175 (1991)","DOI":"10.1109\/CSFW.1991.151582"},{"key":"5_CR46","first-page":"2335","volume-title":"ICYCS","author":"J. Zhan","year":"2008","unstructured":"Zhan, J., Zhang, H., Zou, B., Li, X.: Research on automated testing of the trusted platform model. In: ICYCS, pp. 2335\u20132339. IEEE Computer Society, Los Alamitos (2008)"},{"issue":"3","key":"5_CR47","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/s11432-010-0059-z","volume":"53","author":"J. Zhang","year":"2010","unstructured":"Zhang, J., Ma, J., Moon, S.: Universally composable secure tnc model and eap-tnc protocol in if-t. Science China Information Sciences\u00a053(3), 465\u2013482 (2010)","journal-title":"Science China Information Sciences"},{"key":"5_CR48","first-page":"162","volume-title":"CIT 2006: Proceedings of the Sixth IEEE International Conference on Computer and Information Technology","author":"Z. Zhang","year":"2006","unstructured":"Zhang, Z., Hong, F., Liao, J.: Modeling Chinese Wall Policy Using Colored Petri Nets. In: CIT 2006: Proceedings of the Sixth IEEE International Conference on Computer and Information Technology, p. 162. IEEE Computer Society, Washington, DC, USA (2006)"},{"key":"5_CR49","doi-asserted-by":"crossref","unstructured":"Zhang, Z., Hong, F., Liao, J.-G.: Verification of strict integrity policy via petri nets. In: The International Conference on Systems and Networks Communication (ICSNC), p. 23 (2006)","DOI":"10.1109\/ICSNC.2006.76"}],"container-title":["Lecture Notes in Computer Science","Trusted Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-25283-9_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,14]],"date-time":"2025-03-14T05:27:50Z","timestamp":1741930070000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-25283-9_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642252822","9783642252839"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-25283-9_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}