{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T04:28:03Z","timestamp":1780633683388,"version":"3.54.1"},"publisher-location":"Cham","reference-count":50,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030634056","type":"print"},{"value":"9783030634063","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-63406-3_16","type":"book-chapter","created":{"date-parts":[[2020,12,18]],"date-time":"2020-12-18T16:05:19Z","timestamp":1608307519000},"page":"268-283","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Formal Foundations for Intel SGX Data Center Attestation Primitives"],"prefix":"10.1007","author":[{"given":"Muhammad Usama","family":"Sardar","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rasha","family":"Faqeh","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christof","family":"Fetzer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,12,19]]},"reference":[{"issue":"1","key":"16_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3127586","volume":"65","author":"M Abadi","year":"2017","unstructured":"Abadi, M., Blanchet, B., Fournet, C.: The applied pi calculus: mobile values, new names, and secure communication. J. ACM (JACM) 65(1), 1\u201341 (2017)","journal-title":"J. ACM (JACM)"},{"issue":"3","key":"16_CR2","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1145\/373243.360213","volume":"36","author":"M Abadi","year":"2001","unstructured":"Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. ACM SIGPLAN Not. 36(3), 104\u2013115 (2001)","journal-title":"ACM SIGPLAN Not."},{"key":"16_CR3","unstructured":"Anati, I., Gueron, S., Johnson, S., Scarlata, V.: Innovative technology for CPU based attestation and sealing. In: International Workshop on Hardware and Architectural Support for Security and Privacy, 2013. ACM, New York (2013). https:\/\/software.intel.com\/en-us\/articles\/innovative-technology-for-cpu-based-attestation-and-sealing"},{"key":"16_CR4","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1016\/j.protcy.2013.12.525","volume":"12","author":"MG Avram","year":"2014","unstructured":"Avram, M.G.: Advantages and challenges of adopting cloud computing from an enterprise perspective. Procedia Technol. 12, 529\u2013534 (2014)","journal-title":"Procedia Technol."},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Handbook of Automated Reasoning, pp. 19\u201399. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11804192_17"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Design Automation Conference, pp. 317\u2013320. ACM\/IEEE (1999)","DOI":"10.21236\/ADA360973"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14"},{"issue":"1\u20132","key":"16_CR9","first-page":"1","volume":"1","author":"B Blanchet","year":"2016","unstructured":"Blanchet, B.: Modeling and verifying security protocols with the applied pi calculus and ProVerif. Found. Trends Priv. Secur. 1(1\u20132), 1\u2013135 (2016)","journal-title":"Found. Trends Priv. Secur."},{"key":"16_CR10","unstructured":"Blanchet, B.: CryptoVerif: a computationally-sound security protocol verifier. Technical report (2017)"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Brickell, E., Li, J.: Enhanced privacy ID: a direct anonymous attestation scheme with enhanced revocation capabilities. In: Privacy in Electronic Society, pp. 21\u201330. ACM (2007)","DOI":"10.1145\/1314333.1314337"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Brickell, E., Li, J.: Enhanced privacy ID from bilinear pairing for hardware authentication and attestation. In: Social Computing, pp. 768\u2013775. IEEE (2010)","DOI":"10.1109\/SocialCom.2010.118"},{"issue":"1\u20132","key":"16_CR13","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"MC Browne","year":"1988","unstructured":"Browne, M.C., Clarke, E.M., Gr\u00fcmberg, O.: Characterizing finite Kripke structures in propositional temporal logic. Theor. Comput. Sci. 59(1\u20132), 115\u2013131 (1988)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR14","first-page":"760","volume":"14","author":"G Cabodi","year":"2015","unstructured":"Cabodi, G., Camurati, P., Loiacono, C., Pipitone, G., Savarese, F., Vendraminetto, D.: Formal verification of embedded systems for remote attestation. WSEAS Trans. Comput. 14, 760\u2013769 (2015)","journal-title":"WSEAS Trans. Comput."},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-030-32409-4_17","volume-title":"Formal Methods and Software Engineering","author":"S Conchon","year":"2019","unstructured":"Conchon, S., Roux, M.: Reasoning about universal cubes in MCMT. In: Ait-Ameur, Y., Qin, S. (eds.) ICFEM 2019. LNCS, vol. 11852, pp. 270\u2013285. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32409-4_17"},{"key":"16_CR16","unstructured":"Costan, V., Devadas, S.: Intel SGX explained. IACR Cryptology ePrint Archive (2016)"},{"key":"16_CR17","unstructured":"Costan, V., Lebedev, I., Devadas, S.: Sanctum: minimal hardware extensions for strong software isolation. In: USENIX Security Symposium, pp. 857\u2013874 (2016)"},{"issue":"2","key":"16_CR18","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198\u2013208 (1983)","journal-title":"IEEE Trans. Inf. Theory"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Fraer, R., et al.: From visual to logical formalisms for SoC validation. In: Formal Methods and Models for Codesign (MEMOCODE), pp. 165\u2013174. ACM\/IEEE (2014)","DOI":"10.1109\/MEMCOD.2014.6961855"},{"issue":"4","key":"16_CR20","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1145\/2611429.2617811","volume":"12","author":"A Gill","year":"2014","unstructured":"Gill, A.: Domain-specific languages and code synthesis using Haskell. Queue 12(4), 30\u201343 (2014)","journal-title":"Queue"},{"key":"16_CR21","unstructured":"Goel, A., Krstic, S., Leslie, R., Tuttle, M.: SMT-based system verification with DVF. In: Satisfiability Modulo Theories, vol. 20, pp. 32\u201343. EasyChair (2013)"},{"key":"16_CR22","unstructured":"Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463\u2013492 (1990)"},{"key":"16_CR23","unstructured":"Hyperledger: Hyperledger Avalon (2020). https:\/\/www.hyperledger.org\/use\/avalon. Accessed 24 July 2020"},{"key":"16_CR24","unstructured":"Intel: Attestation service for Intel$$\\textregistered $$ Software Guard Extensions (Intel$$\\textregistered $$ SGX): API documentation. https:\/\/api.trustedservices.intel.com\/documents\/sgx-attestation-api-spec.pdf, revision 6.0. Accessed 24 July 2020"},{"key":"16_CR25","unstructured":"Intel: Intel\u00aeSoftware Guard Extensions (Intel\u00aeSGX) Data Center Attestation Primitives: ECDSA Quote Library API, March 2020\u201308 July 2020. https:\/\/download.01.org\/intel-sgx\/sgx-dcap\/1.7\/linux\/docs\/Intel_SGX_ECDSA_QuoteLibReference_DCAP_API.pdf. Accessed 24 July 2020"},{"key":"16_CR26","unstructured":"Intel: SGX Data Center Attestation Primitives. https:\/\/github.com\/intel\/SGXDataCenterAttestationPrimitives. Accessed on 24 July 2020"},{"key":"16_CR27","unstructured":"Intel: Intel\u00aeSoftware Guard Extensions (Intel\u00ae SGX), June 2015. https:\/\/software.intel.com\/sites\/default\/files\/332680-002.pdf, revision 1.1. Accessed 24 July 2020"},{"key":"16_CR28","unstructured":"Intel: Intel\u00ae 64 and IA-32 architectures: software developer\u2019s manual. Order Number: 325462\u2013071US, October 2019. https:\/\/software.intel.com\/sites\/default\/files\/managed\/39\/c5\/325462-sdm-vol-1-2abcd-3abcd.pdf. Accessed 24 July 2020"},{"key":"16_CR29","unstructured":"Intel: Intel\u00ae SGX data center attestation primitives (Intel\u00ae SGX DCAP) (2019). https:\/\/download.01.org\/intel-sgx\/sgx-dcap\/1.7\/linux\/docs\/Intel_SGX_DCAP_ECDSA_Orientation.pdf, revision 08\u201307-2020, Accessed 24 July 2020"},{"key":"16_CR30","unstructured":"Intel: Intel\u00aePCK Certificate and Certificate Revocation List Profile Specification, March 2020. https:\/\/download.01.org\/intel-sgx\/sgx-dcap\/1.7\/linux\/docs\/Intel_SGX_PCK_Certificate_CRL_Spec-1.4.pdf, revision 1.4, 30 March 2020, updated 08\u201307-2020. Accessed 24 July 2020"},{"key":"16_CR31","unstructured":"Intel: Intel\u00aeSoftware Guard Extensions (Intel\u00aeSGX): developer guide, April 2020. https:\/\/download.01.org\/intel-sgx\/sgx-linux\/2.9.1\/docs\/Intel_SGX_Developer_Guide.pdf, revision 2.9.1, April 2020. Accessed 24 July 2020"},{"key":"16_CR32","unstructured":"Johnson, S., Scarlata, V., Rozas, C., Brickell, E., Mckeen, F.: Intel\u00ae Software Guard Extensions: EPID provisioning and attestation services (2016), https:\/\/software.intel.com\/content\/www\/us\/en\/develop\/download\/intel-sgx-intel-epid-provisioning-and-attestation-services.html"},{"key":"16_CR33","unstructured":"Kaplan, D.: AMD x86 memory encryption technologies. USENIX Association, Austin, TX, August 2016"},{"key":"16_CR34","unstructured":"Knauth, T., Steiner, M., Chakrabarti, S., Lei, L., Xing, C., Vij, M.: Integrating remote attestation with transport layer security. arXiv preprint:1801.05863 (2018)"},{"key":"16_CR35","volume-title":"Introduction to Embedded Systems: A Cyber-Physical Systems Approach","author":"EA Lee","year":"2017","unstructured":"Lee, E.A., Seshia, S.A.: Introduction to Embedded Systems: A Cyber-Physical Systems Approach. MIT Press, Cambridge (2017)"},{"key":"16_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-319-21668-3_9","volume-title":"Computer Aided Verification","author":"R Leslie-Hurd","year":"2015","unstructured":"Leslie-Hurd, R., Caspi, D., Fernandez, M.: Verifying linearizability of Intel\u00ae software guard extensions. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 144\u2013160. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21668-3_9"},{"issue":"1","key":"16_CR37","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/s13389-016-0145-2","volume":"7","author":"F Lugou","year":"2017","unstructured":"Lugou, F., Apvrille, L., Francillon, A.: SMASHUP: a toolchain for unified verification of hardware\/software co-designs. J. Cryptograph. Eng. 7(1), 63\u201374 (2017)","journal-title":"J. Cryptograph. Eng."},{"key":"16_CR38","unstructured":"Marlow, S., et al.: Haskell 2010 language report (2010). https:\/\/www.haskell.org\/onlinereport\/haskell2010"},{"key":"16_CR39","doi-asserted-by":"crossref","unstructured":"McKeen, F., et al.: Intel$$\\textregistered $$ software guard extensions (Intel$$\\textregistered $$ SGX) support for dynamic memory management inside an enclave. In: Hardware and Architectural Support for Security and Privacy, pp. 1\u20139. ACM (2016)","DOI":"10.1145\/2948618.2954331"},{"key":"16_CR40","unstructured":"Nunes, I.D.O., Eldefrawy, K., Rattanavipanon, N., Steiner, M., Tsudik, G.: VRASED: a verified hardware\/software co-design for remote attestation. In: 28th USENIX Security Symposium, pp. 1429\u20131446. USENIX Association, Santa Clara (2019)"},{"key":"16_CR41","volume-title":"Understanding Cryptography: A Textbook for Students and Practitioners","author":"C Paar","year":"2009","unstructured":"Paar, C., Pelzl, J.: Understanding Cryptography: A Textbook for Students and Practitioners. Springer, Cham (2009)"},{"issue":"6","key":"16_CR42","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3291047","volume":"51","author":"S Pinto","year":"2019","unstructured":"Pinto, S., Santos, N.: Demystifying ARM TrustZone: a comprehensive survey. ACM Comput. Surv. (CSUR) 51(6), 1\u201336 (2019)","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"16_CR43","doi-asserted-by":"crossref","unstructured":"Sabt, M., Achemlal, M., Bouabdallah, A.: Trusted execution environment: what it is, and what it is not. In: Trustcom\/BigDataSE\/ISPA, vol. 1, pp. 57\u201364. IEEE (2015)","DOI":"10.1109\/Trustcom.2015.357"},{"key":"16_CR44","doi-asserted-by":"crossref","unstructured":"Sardar, M.U., Quoc, D.L., Fetzer, C.: Towards formalization of EPID-based remote attestation in Intel SGX, Euromicro Conference on Digital System Design (To appear, 2020)","DOI":"10.1109\/DSD51259.2020.00099"},{"key":"16_CR45","unstructured":"Scarlata, V., Johnson, S., Beaney, J., Zmijewski, P.: Supporting third party attestation for Intel\u00ae SGX with Intel\u00ae data center attestation primitives. White paper (2018)"},{"key":"16_CR46","doi-asserted-by":"crossref","unstructured":"Subramanyan, P., Sinha, R., Lebedev, I., Devadas, S., Seshia, S.A.: A formal foundation for secure remote execution of enclaves. In: SIGSAC Conference on Computer and Communications Security, pp. 2435\u20132450. ACM (2017)","DOI":"10.1145\/3133956.3134098"},{"key":"16_CR47","doi-asserted-by":"crossref","unstructured":"Tuttle, M.R., Goel, A.: Protocol proof checking simplified with SMT. In: Network Computing and Applications, pp. 195\u2013202. IEEE (2012)","DOI":"10.1109\/NCA.2012.46"},{"key":"16_CR48","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/3-540-48660-7_29","volume-title":"Automated Deduction \u2014 CADE-16","author":"C Weidenbach","year":"1999","unstructured":"Weidenbach, C.: Towards an automatic analysis of security protocols in first-order logic. CADE 1999. LNCS (LNAI), vol. 1632, pp. 314\u2013328. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48660-7_29"},{"key":"16_CR49","unstructured":"Woo, T.Y.C., Lam, S.S.: A semantic model for authentication protocols. In: IEEE Computer Society Symposium on Research in Security and Privacy, pp. 178\u2013194, May 1993"},{"key":"16_CR50","doi-asserted-by":"crossref","unstructured":"Zeller, A.: Why Programs Fail: A Guide to Systematic Debugging. Elsevier (2009)","DOI":"10.1016\/B978-0-12-374515-6.00006-X"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-63406-3_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,2,24]],"date-time":"2021-02-24T14:43:17Z","timestamp":1614177797000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-63406-3_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030634056","9783030634063"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-63406-3_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"19 December 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICFEM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Engineering Methods","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":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 March 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 March 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"icfem2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/formal-analysis.com\/icfem\/2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"41","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"39% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1 Doctoral symposium paper in the back matter","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}