{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,4]],"date-time":"2026-06-04T16:02:20Z","timestamp":1780588940672,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":36,"publisher":"ACM","license":[{"start":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T00:00:00Z","timestamp":1780272000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/legalcode"}],"funder":[{"name":"National Natural Science Foundation of China under Grant","award":["62372268"],"award-info":[{"award-number":["62372268"]}]},{"name":"Shandong Provincial Natural Science Foundation","award":["ZR2022LZH013"],"award-info":[{"award-number":["ZR2022LZH013"]}]},{"name":"Key R&D Program of Shandong Province, China","award":["2024CXGC010114"],"award-info":[{"award-number":["2024CXGC010114"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,6]]},"DOI":"10.1145\/3779208.3785377","type":"proceedings-article","created":{"date-parts":[[2026,6,4]],"date-time":"2026-06-04T15:21:58Z","timestamp":1780586518000},"page":"1570-1583","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Analysis Framework for E2EE Protocols"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-9807-8110","authenticated-orcid":false,"given":"Yu","family":"Wang","sequence":"first","affiliation":[{"name":"School of Cyber Science and Technology, Shandong University, Qingdao, Shandong, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-6147-7119","authenticated-orcid":false,"given":"Xiaofeng","family":"Liu","sequence":"additional","affiliation":[{"name":"School of Cyber Science and Technology, Shandong University, Qingdao, Shandong, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-5054-7915","authenticated-orcid":false,"given":"Yu","family":"Hou","sequence":"additional","affiliation":[{"name":"School of Cyber Science and Technology, Shandong University, Qingdao, Shandong, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5523-2672","authenticated-orcid":false,"given":"Chengyu","family":"Hu","sequence":"additional","affiliation":[{"name":"School of Cyber Science and Technology, Shandong University, Qingdao, Shandong, China, State Key Laboratory of Cryptography and Digital Economy Security, Shandong University, Qingdao, Shandong, China and Key Laboratory of Cryptologic Technology and Information Security, Shandong University, Jinan, Shandong, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3367-0951","authenticated-orcid":false,"given":"Shanqing","family":"Guo","sequence":"additional","affiliation":[{"name":"School of Cyber Science and Technology, Shandong University, Qingdao, Shandong, China, State Key Laboratory of Cryptography and Digital Economy Security, Shandong University, Qingdao, Shandong, China and Key Laboratory of Cryptologic Technology and Information Security, Shandong University, Jinan, Shandong, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,6,4]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"[n.d.]. https:\/\/d.line-scdn.net\/stf\/linecorp\/en\/csr\/line-encryption-whitepaper-ver2.1.pdf."},{"key":"e_1_3_2_1_2_1","unstructured":"[n.d.]. line. https:\/\/line.me\/en\/."},{"key":"e_1_3_2_1_3_1","unstructured":"[n.d.]. mozilla decrypt. https:\/\/developer.mozilla.org\/en-US\/docs\/Web\/API\/SubtleCrypto\/decrypt."},{"key":"e_1_3_2_1_4_1","unstructured":"[n.d.]. mozilla deriveKey. https:\/\/developer.mozilla.org\/en-US\/docs\/Web\/API\/SubtleCrypto\/deriveKey."},{"key":"e_1_3_2_1_5_1","unstructured":"[n.d.]. rfc7517. https:\/\/datatracker.ietf.org\/doc\/html\/rfc7517."},{"key":"e_1_3_2_1_6_1","unstructured":"[n. d.]. tamarin manual. https:\/\/tamarin-prover.com\/manual\/master\/tex\/tamarin-manual.pdf."},{"key":"e_1_3_2_1_7_1","unstructured":"[n. d.]. Tamarin Prover for Security Protocol Analysis. https:\/\/tamarin-prover.com\/."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3558482.3581773"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00008"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1147\/sj.441.0145"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28641-4_2"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"crossref","unstructured":"Bruno Blanchet et al. 2016. Modeling and verifying security protocols with the applied pi calculus and ProVerif. Foundations and Trends\u00ae in Privacy and Security 1 1\u20132 (2016) 1\u2013135.","DOI":"10.1561\/3300000004"},{"key":"e_1_3_2_1_13_1","volume-title":"WhatsApp and Telegram. Cryptology ePrint Archive","author":"Bogos Corina-Elena","year":"2023","unstructured":"Corina-Elena Bogos, R\u0103zvan Mocanu, and Emil Simion. 2023. A security analysis comparison between Signal, WhatsApp and Telegram. Cryptology ePrint Archive (2023)."},{"key":"e_1_3_2_1_14_1","volume-title":"2023 IEEE 36th Computer Security Foundations Symposium (CSF). IEEE, 43\u201358","author":"Cheval Vincent","year":"2023","unstructured":"Vincent Cheval, V\u00e9ronique Cortier, and Alexandre Debant. 2023. Election verifiabilitty with proverif. In 2023 IEEE 36th Computer Security Foundations Symposium (CSF). IEEE, 43\u201358."},{"key":"e_1_3_2_1_15_1","volume-title":"31st USENIX Security Symposium (USENIX Security 22)","author":"Cheval Vincent","year":"2022","unstructured":"Vincent Cheval, Charlie Jacomme, Steve Kremer, and Robert K\u00fcnnemann. 2022. {SAPIC + }: protocol verifiers of the world, unite!. In 31st USENIX Security Symposium (USENIX Security 22). 3935\u20133952."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","unstructured":"V\u00e9ronique Cortier Steve Kremer et al. 2014. Formal models and techniques for analyzing security protocols: A tutorial. Foundations and Trends\u00ae in Programming Languages 1 3 (2014) 151\u2013267.","DOI":"10.1561\/2500000001"},{"key":"e_1_3_2_1_17_1","unstructured":"deepsec. [n. d.]. https:\/\/deepsec-prover.github.io\/."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_3_2_1_19_1","volume-title":"7th USENIX Workshop on Free and Open Communications on the Internet (FOCI 17)","author":"Espinoza Antonio M.","year":"2017","unstructured":"Antonio M. Espinoza, William J. Tolley, Jedidiah R. Crandall, Masashi Crete-Nishihata, and Andrew Hilts. 2017. Alice and Bob, who the FOCI are they?: Analysis of end-to-end encryption in the LINE messaging application. In 7th USENIX Workshop on Free and Open Communications on the Internet (FOCI 17). USENIX Association, Vancouver, BC. https:\/\/www.usenix.org\/conference\/foci17\/workshop-program\/presentation\/espinoza"},{"key":"e_1_3_2_1_20_1","volume-title":"25th USENIX Security Symposium (USENIX Security 16)","author":"Garman Christina","year":"2016","unstructured":"Christina Garman, Matthew Green, Gabriel Kaptchuk, Ian Miers, and Michael Rushanan. 2016. Dancing on the lip of the volcano: Chosen ciphertext attacks on apple {iMessage}. In 25th USENIX Security Symposium (USENIX Security 16). 655\u2013672."},{"key":"e_1_3_2_1_21_1","unstructured":"ibm.com. [n. d.]. https:\/\/www.ibm.com\/topics\/end-to-end-encryption."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-90567-5_12"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.2197\/ipsjjip.31.523"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-98989-1_13"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2017.38"},{"key":"e_1_3_2_1_26_1","volume-title":"Facebook messenger deploys signal protocol for end to end encryption. Website: https:\/\/signal.org\/blog\/facebook-messenger","author":"Marlinspike Moxie","year":"2016","unstructured":"Moxie Marlinspike. 2016. Facebook messenger deploys signal protocol for end to end encryption. Website: https:\/\/signal.org\/blog\/facebook-messenger (2016)."},{"key":"e_1_3_2_1_27_1","unstructured":"mozilla. [n. d.]. https:\/\/developer.mozilla.org\/en-US\/docs\/Web\/API\/SubtleCrypto\/generateKey."},{"key":"e_1_3_2_1_28_1","volume-title":"32nd USENIX Security Symposium (USENIX Security 23)","author":"Paterson Kenneth G","year":"2023","unstructured":"Kenneth G Paterson, Matteo Scarlata, and Kien Tuong Truong. 2023. Three lessons from threema: Analysis of a secure messenger. In 32nd USENIX Security Symposium (USENIX Security 23). 1289\u20131306."},{"key":"e_1_3_2_1_29_1","unstructured":"proverif. [n. d.]. https:\/\/bblanche.gitlabpages.inria.fr\/proverif\/."},{"key":"e_1_3_2_1_30_1","unstructured":"rocketchat. [n. d.]. https:\/\/www.rocket.chat."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2018.00036"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1587\/transinf.2018FOP0001"},{"key":"e_1_3_2_1_33_1","unstructured":"signal. [n. d.]. https:\/\/signal.org\/."},{"key":"e_1_3_2_1_34_1","unstructured":"tamarin. [n.d.]. https:\/\/docs.rocket.chat\/v1\/docs\/end-to-end-encryption-user-guide."},{"key":"e_1_3_2_1_35_1","unstructured":"threema. [n. d.]. https:\/\/threema.ch\/en\/."},{"key":"e_1_3_2_1_36_1","unstructured":"whatsapp. [n. d.]. https:\/\/web.whatsapp.com\/."}],"event":{"name":"ASIA CCS '26: ACM Asia Conference on Computer and Communications Security","location":"Bangalore India","acronym":"ASIA CCS '26","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the ACM Asia Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3779208.3785377","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,4]],"date-time":"2026-06-04T15:25:14Z","timestamp":1780586714000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3779208.3785377"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6]]},"references-count":36,"alternative-id":["10.1145\/3779208.3785377","10.1145\/3779208"],"URL":"https:\/\/doi.org\/10.1145\/3779208.3785377","relation":{},"subject":[],"published":{"date-parts":[[2026,6]]},"assertion":[{"value":"2026-06-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}