{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,12]],"date-time":"2026-02-12T11:36:26Z","timestamp":1770896186890,"version":"3.50.1"},"reference-count":56,"publisher":"Springer Science and Business Media LLC","issue":"1-4","license":[{"start":{"date-parts":[[2017,12,2]],"date-time":"2017-12-02T00:00:00Z","timestamp":1512172800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100006041","name":"Innovate UK","doi-asserted-by":"publisher","award":["Knowledge Transfer Partnership 010041"],"award-info":[{"award-number":["Knowledge Transfer Partnership 010041"]}],"id":[{"id":"10.13039\/501100006041","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/N019547\/1"],"award-info":[{"award-number":["EP\/N019547\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["VRBMAS"],"award-info":[{"award-number":["VRBMAS"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"name":"DFG (German Science Foundation)","award":["Hu 737\/5-2"],"award-info":[{"award-number":["Hu 737\/5-2"]}]},{"name":"DFG (German Science Foundation)","award":["Ni 491\/13-3"],"award-info":[{"award-number":["Ni 491\/13-3"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2018,6]]},"DOI":"10.1007\/s10817-017-9443-3","type":"journal-article","created":{"date-parts":[[2017,12,2]],"date-time":"2017-12-02T07:15:18Z","timestamp":1512198918000},"page":"113-139","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["CoSMed: A Confidentiality-Verified Social Media Platform"],"prefix":"10.1007","volume":"61","author":[{"given":"Thomas","family":"Bauerei\u00df","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armando","family":"Pesenti Gritti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8747-0619","authenticated-orcid":false,"given":"Andrei","family":"Popescu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Franco","family":"Raimondi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,12,2]]},"reference":[{"key":"9443_CR1","unstructured":"OWASP top ten project. www.owasp.org\/index.php\/Top10#OWASP_Top_10_for_2013"},{"key":"9443_CR2","unstructured":"The CoSMed Homepage. http:\/\/andreipopescu.uk\/CoSMed.html"},{"key":"9443_CR3","unstructured":"The CoSMeDis Homepage. http:\/\/andreipopescu.uk\/CoSMeDis.html"},{"key":"9443_CR4","unstructured":"Jif: Java $$+$$ + information flow. http:\/\/www.cs.cornell.edu\/jif (2014)"},{"key":"9443_CR5","unstructured":"SPARK. http:\/\/www.spark-2014.org (2014)"},{"key":"9443_CR6","unstructured":"Caritas Anchor House. http:\/\/caritasanchorhouse.org.uk\/ (2016)"},{"key":"9443_CR7","unstructured":"The diaspora $$^*$$ \u2217 project. https:\/\/diasporafoundation.org\/ (2016)"},{"key":"9443_CR8","doi-asserted-by":"crossref","unstructured":"Arapinis, M., Bursuc, S., Ryan, M.: Privacy supporting cloud computing: ConfiChair, a case study. In: POST, pp. 89\u2013108 (2012)","DOI":"10.1007\/978-3-642-28641-4_6"},{"key":"9443_CR9","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., B\u00e9guelin, S.Z.: Formal certification of code-based cryptographic proofs. In: POPL, pp. 90\u2013101 (2009)","DOI":"10.1145\/1594834.1480894"},{"key":"9443_CR10","doi-asserted-by":"crossref","unstructured":"Bauerei\u00df, T., Gritti, A.P., Popescu, A., Raimondi, F.: CoSMed: a confidentiality-verified conference management system. In: ITP (2016)","DOI":"10.1007\/978-3-319-43144-4_6"},{"key":"9443_CR11","doi-asserted-by":"crossref","unstructured":"Bauerei\u00df, T., Pesenti Gritti, A., Popescu, A., Raimondi, F.: CoSMeDis: A distributed social media platform with formally verified confidentiality guarantees. In: IEEE Security and Privacy, pp. 729\u2013748 (2017)","DOI":"10.1109\/SP.2017.24"},{"key":"9443_CR12","doi-asserted-by":"crossref","unstructured":"Bichhawat, A., Rajani, V., Garg, D., Hammer, C.: Information flow control in WebKit\u2019s JavaScript bytecode. In: POST, pp. 159\u2013178 (2014)","DOI":"10.1007\/978-3-642-54792-8_9"},{"key":"9443_CR13","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. In: LICS, pp. 331\u2013340 (2005)","DOI":"10.1109\/LICS.2005.8"},{"issue":"2","key":"9443_CR14","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/s10817-015-9335-3","volume":"56","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., B\u00f6hme, S., Fleury, M., Smolka, S.J., Steckermeier, A.: Semi-intelligible Isar proofs from machine-generated proofs. J. Autom. Reason. 56(2), 155\u2013200 (2016)","journal-title":"J. Autom. Reason."},{"key":"9443_CR15","doi-asserted-by":"publisher","unstructured":"Blanchette, J.C., B\u00f6hme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. Log. Methods Comput. Sci. 12(4) (2016). https:\/\/doi.org\/10.2168\/LMCS-12(4:13)2016","DOI":"10.2168\/LMCS-12(4:13)2016"},{"key":"9443_CR16","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., H\u00f6lzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle\/HOL. In: ITP, pp. 93\u2013110 (2014)","DOI":"10.1007\/978-3-319-08970-6_7"},{"key":"9443_CR17","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Merz, S. (eds.): Interactive theorem proving. In: Proceedings on 7th International Conference of ITP 2016, Nancy, France, vol. 9807, 22\u201325 Aug 2016 (2016)","DOI":"10.1007\/978-3-319-43144-4"},{"issue":"4\u20135","key":"9443_CR18","doi-asserted-by":"crossref","first-page":"323","DOI":"10.3233\/JCS-15791","volume":"25","author":"N Broberg","year":"2017","unstructured":"Broberg, N., van Delft, B., Sands, D.: Paragon\u2014practical programming with information flow control. J. Comput. Secur. 25(4\u20135), 323\u2013365 (2017)","journal-title":"J. Comput. Secur."},{"key":"9443_CR19","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: Ur\/Web: a simple model for programming the web. In: POPL, pp. 153\u2013165 (2015)","DOI":"10.1145\/2775051.2677004"},{"issue":"2","key":"9443_CR20","doi-asserted-by":"crossref","first-page":"8:1","DOI":"10.1145\/2829949","volume":"18","author":"S Chong","year":"2015","unstructured":"Chong, S., Meyden, R.V.D.: Using architecture to reason about information security. ACM Trans. Inf. Syst. Secur. 18(2), 8:1\u20138:30 (2015)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"9443_CR21","doi-asserted-by":"crossref","unstructured":"Chugh, R., Meister, J.A., Jhala, R., Lerner, S.: Staged information flow for JavaScript. In: PLDI, pp. 50\u201362 (2009)","DOI":"10.1145\/1542476.1542483"},{"key":"9443_CR22","doi-asserted-by":"crossref","unstructured":"Dam, M., Guanciale, R., Khakpour, N., Nemati, H., Schwarz, O.: Formal verification of information flow security for a simple ARM-based separation kernel. In: CCS, pp.\u00a0223\u2013234 (2013)","DOI":"10.1145\/2508859.2516702"},{"key":"9443_CR23","doi-asserted-by":"crossref","unstructured":"de\u00a0Amorim, A.A., Collins, N., DeHon, A., Demange, D., Hri\u0163cu, C., Pichardie, D., Pierce, B.C., Pollack, R., Tolmach, A.: A verified information-flow architecture. In: POPL, pp.\u00a0165\u2013178 (2014)","DOI":"10.1145\/2578855.2535839"},{"key":"9443_CR24","doi-asserted-by":"crossref","unstructured":"de\u00a0Nivelle, H. (ed.): Automated reasoning with analytic tableaux and related methods. In: Proceedings on 24th International Conference of TABLEAUX 2015, Wroc\u0142aw, Poland, vol. 9323, 21\u201324 Sept 2015 (2015)","DOI":"10.1007\/978-3-319-24312-2"},{"key":"9443_CR25","doi-asserted-by":"crossref","unstructured":"Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.: A fully verified executable LTL model checker. In: CAV, pp.\u00a0463\u2013478 (2013)","DOI":"10.1007\/978-3-642-39799-8_31"},{"key":"9443_CR26","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Rabe, M.N., S\u00e1nchez, C.: Algorithms for model checking HyperLTL and HyperCTL $${\\hat{}}$$ ^ *. In: CAV, pp.\u00a030\u201348","DOI":"10.1007\/978-3-319-21690-4_3"},{"key":"9443_CR27","doi-asserted-by":"crossref","unstructured":"Fong, P.W.L., Anwar, M.M., Zhao, Z.: A privacy preservation model for Facebook-style social network systems. In: ESORICS, pp.\u00a0303\u2013320 (2009)","DOI":"10.1007\/978-3-642-04444-1_19"},{"key":"9443_CR28","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Unwinding and inference control. In: IEEE Symposium on Security and Privacy, pp.\u00a075\u201387 (1984)","DOI":"10.1109\/SP.1984.10019"},{"key":"9443_CR29","doi-asserted-by":"crossref","unstructured":"Groef, W.D., Devriese, D., Nikiforakis, N., Piessens, F.: FlowFox: a web browser with flexible and precise information flow control. In: CCS, pp.\u00a0748\u2013759 (2012)","DOI":"10.1145\/2382196.2382275"},{"key":"9443_CR30","doi-asserted-by":"crossref","unstructured":"Guttman, J.D., Rowe, P.D.: A cut principle for information flow. In: CSF, pp.\u00a0107\u2013121 (2015)","DOI":"10.1109\/CSF.2015.15"},{"key":"9443_CR31","unstructured":"Haftmann, F.: Code generation from specifications in higher-order logic. Ph.D. thesis, Technische Universit\u00e4t M\u00fcnchen (2009)"},{"key":"9443_CR32","first-page":"103","volume":"2010","author":"F Haftmann","year":"2010","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. FLOPS 2010, 103\u2013117 (2010)","journal-title":"FLOPS"},{"key":"9443_CR33","doi-asserted-by":"crossref","unstructured":"Haftmann, F., Wenzel, M.: Constructive type classes in Isabelle. In: TYPES, pp.\u00a0160\u2013174 (2006)","DOI":"10.1007\/978-3-540-74464-1_11"},{"key":"9443_CR34","doi-asserted-by":"crossref","unstructured":"Hardin, D.S., Smith, E.W., Young, W.D.: A robust machine code proof framework for highly secure applications. In: ACL2, pp.\u00a011\u201320 (2006)","DOI":"10.1145\/1217975.1217978"},{"key":"9443_CR35","unstructured":"Hawblitzel, C., Howell, J., Lorch, J.R., Narayan, A., Parno, B., Zhang, D., Zill, B.: Ironclad apps: end-to-end security via automated full-system verification. In: OSDI \u201914, pp.\u00a0165\u2013181 (2014)"},{"key":"9443_CR36","unstructured":"Jang, D., Tatlock, Z., Lerner, S.: Establishing browser security guarantees through formal shim verification. In: USENIX Security, pp.\u00a0113\u2013128 (2012)"},{"key":"9443_CR37","doi-asserted-by":"crossref","unstructured":"Kamm\u00fcller, F., Wenzel, M., Paulson, L.C.: Locales\u2014a sectioning concept for Isabelle. In: TPHOLs\u201999, pp.\u00a0149\u2013166 (1999)","DOI":"10.1007\/3-540-48256-3_11"},{"key":"9443_CR38","doi-asserted-by":"crossref","unstructured":"Kanav, S., Lammich, P., Popescu, A.: A conference management system with verified document confidentiality. In: CAV, pp.\u00a0167\u2013183 (2014)","DOI":"10.1007\/978-3-319-08867-9_11"},{"issue":"6","key":"9443_CR39","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1743546.1743574","volume":"53","author":"G Klein","year":"2010","unstructured":"Klein, G., Andronick, J., Elphinstone, K., Heiser, G., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: formal verification of an operating-system kernel. Commun. ACM 53(6), 107\u2013115 (2010)","journal-title":"Commun. ACM"},{"key":"9443_CR40","doi-asserted-by":"crossref","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: POPL, pp.\u00a0179\u2013192 (2014)","DOI":"10.1145\/2535838.2535841"},{"issue":"7","key":"9443_CR41","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"9443_CR42","doi-asserted-by":"crossref","unstructured":"Lochbihler, A.: Java and the Java memory model\u2014a unified, machine-checked formalisation. In: ESOP, pp.\u00a0497\u2013517 (2012)","DOI":"10.1007\/978-3-642-28869-2_25"},{"key":"9443_CR43","doi-asserted-by":"crossref","unstructured":"Mantel, H.: Possibilistic definitions of security\u2014an assembly kit. In: CSFW, pp.\u00a0185\u2013199 (2000)","DOI":"10.1109\/CSFW.2000.856936"},{"key":"9443_CR44","doi-asserted-by":"crossref","unstructured":"Mantel, H.: Information flow and noninterference. In: Encyclopedia of Cryptography and Security, 2nd edn., pp. 605\u2013607 (2011)","DOI":"10.1007\/978-1-4419-5906-5_874"},{"issue":"9","key":"9443_CR45","doi-asserted-by":"crossref","first-page":"913","DOI":"10.1109\/12.713311","volume":"47","author":"JS Moore","year":"1998","unstructured":"Moore, J.S., Lynch, T.W., Kaufmann, M.: A mechanically checked proof of the amd5 $${}_{\\text{ k }}86{}^{\\text{ tm }}$$ k 86 tm floating point division program. IEEE Trans. Comput. 47(9), 913\u2013926 (1998)","journal-title":"IEEE Trans. Comput."},{"key":"9443_CR46","doi-asserted-by":"crossref","unstructured":"Murray, T.C., Matichuk, D., Brassil, M., Gammie, P., Bourke, T., Seefried, S., Lewis, C., Gao, X., Klein, G.: seL4: from general purpose to a proof of information flow enforcement. In: IEEE Security and Privacy, pp.\u00a0415\u2013429 (2013)","DOI":"10.1109\/SP.2013.35"},{"key":"9443_CR47","doi-asserted-by":"crossref","unstructured":"Naumowicz, A., Korni\u0142owicz, A.: A brief overview of Mizar. In: TPHOLs, pp.\u00a067\u201372 (2009)","DOI":"10.1007\/978-3-642-03359-9_5"},{"key":"9443_CR48","unstructured":"Nipkow, T.: Programming and proving in Isabelle\/HOL. https:\/\/isabelle.in.tum.de\/dist\/Isabelle2016-1\/doc\/prog-prove.pdf (2017)"},{"key":"9443_CR49","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-10542-0","volume-title":"Concrete Semantics: With Isabelle\/HOL","author":"T Nipkow","year":"2014","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics: With Isabelle\/HOL. Springer, Berlin (2014)"},{"key":"9443_CR50","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Berlin (2002)"},{"key":"9443_CR51","doi-asserted-by":"crossref","unstructured":"Pardo, R., Schneider, G.: A formal privacy policy framework for social networks. In: SEFM, pp.\u00a0378\u2013392 (2014)","DOI":"10.1007\/978-3-319-10431-7_30"},{"key":"9443_CR52","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: IWIL (2010)"},{"issue":"5","key":"9443_CR53","doi-asserted-by":"crossref","first-page":"517","DOI":"10.3233\/JCS-2009-0352","volume":"17","author":"A Sabelfeld","year":"2009","unstructured":"Sabelfeld, A., Sands, D.: Declassification: dimensions and principles. J. Comput. Secur. 17(5), 517\u2013548 (2009)","journal-title":"J. Comput. Secur."},{"key":"9443_CR54","unstructured":"Sutherland, D.: A model of information. In: 9th National Security Conference, pp.\u00a0175\u2013183 (1986)"},{"key":"9443_CR55","doi-asserted-by":"crossref","unstructured":"Wenzel, M.: Isar\u2014a generic interpretative approach to readable formal proof documents. In: TPHOLs, pp.\u00a0167\u2013184 (1999)","DOI":"10.1007\/3-540-48256-3_12"},{"key":"9443_CR56","doi-asserted-by":"crossref","unstructured":"Yang, J., Yessenov, K., Solar-Lezama, A.: A language for automatically enforcing privacy policies. In: POPL, pp.\u00a085\u201396 (2012)","DOI":"10.1145\/2103656.2103669"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-017-9443-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9443-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9443-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,29]],"date-time":"2023-08-29T16:12:44Z","timestamp":1693325564000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-017-9443-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,2]]},"references-count":56,"journal-issue":{"issue":"1-4","published-print":{"date-parts":[[2018,6]]}},"alternative-id":["9443"],"URL":"https:\/\/doi.org\/10.1007\/s10817-017-9443-3","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,2]]}}}