{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T16:57:31Z","timestamp":1761929851465,"version":"3.40.3"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319500102"},{"type":"electronic","value":"9783319500119"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-50011-9_33","type":"book-chapter","created":{"date-parts":[[2016,11,24]],"date-time":"2016-11-24T07:10:32Z","timestamp":1479971432000},"page":"431-441","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Automated Security Proof of Cryptographic Support Commands in TPM 2.0"],"prefix":"10.1007","author":[{"given":"Weijin","family":"Wang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yu","family":"Qin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bo","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yingjun","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dengguo","family":"Feng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,11,25]]},"reference":[{"key":"33_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1007\/3-540-44448-3_41","volume-title":"Advances in Cryptology \u2013 Asiacrypt 2000","author":"M Bellare","year":"2000","unstructured":"Bellare, M., Namprempre, C.: Authenticated encryption: relations among notions and analysis of the generic composition paradigm. In: Okamoto, T. (ed.) ASIACRYPT 2000. LNCS, vol. 1976, pp. 531\u2013545. Springer, Heidelberg (2000). doi:10.1007\/3-540-44448-3_41"},{"key":"33_CR2","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: Computationally sound mechanized proofs of correspondence assertions. In: 20th IEEE Computer Security Foundations Symposium (CSF 2007), pp. 97\u2013111. IEEE, Venice, July 2007","DOI":"10.1109\/CSF.2007.16"},{"issue":"4","key":"33_CR3","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1109\/TDSC.2007.1005","volume":"5","author":"B Blanchet","year":"2008","unstructured":"Blanchet, B.: A computationally sound mechanized prover for security protocols. IEEE Trans. Dependable Secur. Comput. 5(4), 193\u2013207 (2008)","journal-title":"IEEE Trans. Dependable Secur. Comput."},{"key":"33_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1007\/11818175_32","volume-title":"Advances in Cryptology - CRYPTO 2006","author":"B Blanchet","year":"2006","unstructured":"Blanchet, B., Pointcheval, D.: Automated security proofs with sequences of games. In: Dwork, C. (ed.) CRYPTO 2006. LNCS, vol. 4117, pp. 537\u2013554. Springer, Heidelberg (2006). doi:10.1007\/11818175_32"},{"key":"33_CR5","doi-asserted-by":"crossref","unstructured":"Cachin, C., Chandran, N.: A secure cryptographic token interface. In: 22nd IEEE Computer Security Foundations Symposium, CSF 2009, pp. 141\u2013153. IEEE (2009)","DOI":"10.1109\/CSF.2009.7"},{"issue":"3\u20134","key":"33_CR6","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1504\/IJES.2015.072369","volume":"7","author":"X Chu","year":"2015","unstructured":"Chu, X., Feng, D.: On the provable security of TPM2. 0 cryptography APIs. Int. J. Embed. Syst. 7(3\u20134), 230\u2013243 (2015)","journal-title":"Int. J. Embed. Syst."},{"key":"33_CR7","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1016\/j.ic.2014.07.010","volume":"238","author":"V Cortier","year":"2014","unstructured":"Cortier, V., Steel, G.: A generic security API for symmetric key management on cryptographic devices. Inf. Comput. 238, 208\u2013232 (2014)","journal-title":"Inf. Comput."},{"key":"33_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-3-642-54792-8_4","volume-title":"Principles of Security and Trust","author":"M Daubignard","year":"2014","unstructured":"Daubignard, M., Lubicz, D., Steel, G.: A secure key management interface with asymmetric cryptography. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 63\u201382. Springer, Heidelberg (2014). doi:10.1007\/978-3-642-54792-8_4"},{"issue":"6","key":"33_CR9","doi-asserted-by":"publisher","first-page":"1211","DOI":"10.3233\/JCS-2009-0394","volume":"18","author":"S Delaune","year":"2010","unstructured":"Delaune, S., Kremer, S., Steel, G.: Formal security analysis of PKCS# 11 and proprietary extensions. J. Comput. Secur. 18(6), 1211\u20131245 (2010)","journal-title":"J. Comput. Secur."},{"key":"33_CR10","unstructured":"ISO\/IEC 11889:2015: Information Technology - Trusted Platform Module Library\u00a0- Part 1 & Part 2 & Part 3 & Part 4"},{"key":"33_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-662-46666-7_12","volume-title":"Principles of Security and Trust","author":"R K\u00fcnnemann","year":"2015","unstructured":"K\u00fcnnemann, R.: Automated backward analysis of PKCS#11 v2.20. In: Focardi, R., Myers, A. (eds.) POST 2015. LNCS, vol. 9036, pp. 219\u2013238. Springer, Heidelberg (2015). doi:10.1007\/978-3-662-46666-7_12"},{"key":"33_CR12","doi-asserted-by":"crossref","unstructured":"Scerri, G., Stanley-Oakes, R.: Analysis of key wrapping APIs: generic policies, computational security. In: 29nd IEEE Computer Security Foundations Symposium, CSF 2016. IEEE (2016)","DOI":"10.1109\/CSF.2016.27"},{"key":"33_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-319-02726-5_11","volume-title":"Information and Communications Security","author":"J Shao","year":"2013","unstructured":"Shao, J., Feng, D., Qin, Y.: Type-based analysis of protected storage in the TPM. In: Qing, S., Zhou, J., Liu, D. (eds.) ICICS 2013. LNCS, vol. 8233, pp. 135\u2013150. Springer, Heidelberg (2013). doi:10.1007\/978-3-319-02726-5_11"},{"key":"33_CR14","doi-asserted-by":"crossref","unstructured":"Shao, J., Qin, Y., Feng, D., Wang, W.: Formal analysis of enhanced authorization in the TPM 2.0. In: Proceedings of 10th ACM Symposium on Information, Computer and Communications Security (ASIACCS 2015), pp. 273\u2013284. ACM (2015)","DOI":"10.1145\/2714576.2714610"},{"key":"33_CR15","unstructured":"Trusted Computing Group: Trusted Platform Module Library Specification, Family \u201c2.0\u201d, Level 00, Revision 01.16. http:\/\/www.trustedcomputinggroup.org\/resources\/tpm_library_specification"},{"key":"33_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-319-06320-1_12","volume-title":"Information Security Practice and Experience","author":"W Wang","year":"2014","unstructured":"Wang, W., Qin, Y., Feng, D.: Automated proof for authorization protocols of TPM 2.0 in computational model. In: Huang, X., Zhou, J. (eds.) ISPEC 2014. LNCS, vol. 8434, pp. 144\u2013158. Springer, Heidelberg (2014). doi:10.1007\/978-3-319-06320-1_12"},{"key":"33_CR17","unstructured":"Wang, W.: CryptoVerif Input for Cryptographic Support Commands in TPM 2.0. https:\/\/github.com\/WangWeijin\/TPM-2.0-Cryptographic-Support-Commands"},{"issue":"32","key":"33_CR18","doi-asserted-by":"publisher","first-page":"4210","DOI":"10.1007\/s11434-014-0575-0","volume":"59","author":"Q Zhang","year":"2014","unstructured":"Zhang, Q., Zhao, S., Qin, Y., Feng, D.: Formal analysis of TPM2. 0 key management APIs. Chin. Sci. Bull. 59(32), 4210\u20134224 (2014)","journal-title":"Chin. Sci. Bull."}],"container-title":["Lecture Notes in Computer Science","Information and Communications Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-50011-9_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,25]],"date-time":"2021-11-25T01:06:00Z","timestamp":1637802360000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-50011-9_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319500102","9783319500119"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-50011-9_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"25 November 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICICS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Information and Communications Security","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Singapore","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Singapore","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 November 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 December 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"icics2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.icics2016.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}