CoCon: A conference management system with formally verified document confidentiality
Article
Popescu, A., Lammich, P. and Hou, P. 2021. CoCon: A conference management system with formally verified document confidentiality. Journal of Automated Reasoning. 65 (2), pp. 321-356. https://doi.org/10.1007/s10817-020-09566-9
Type | Article |
---|---|
Title | CoCon: A conference management system with formally verified document confidentiality |
Authors | Popescu, A., Lammich, P. and Hou, P. |
Abstract | We present a case study in formally verified security for realistic systems: the information flow security verification of the functional kernel of a web application, the CoCon conference management system. We use the Isabelle theorem prover to specify and verify fine-grained confidentiality properties, as well as complementary safety and “traceback” properties. The challenges posed by this development in terms of expressiveness have led to bounded-deducibility security, a novel security model and verification method generally applicable to systems describable as input/output automata. |
Keywords | Article, Information-Flow Security, Confidentiality, Unwinding Proof Method, Theorem Proving, Isabelle/HOL, Conference Management System |
Publisher | Springer |
Journal | Journal of Automated Reasoning |
ISSN | 0168-7433 |
Electronic | 1573-0670 |
Publication dates | |
Online | 16 Jul 2020 |
28 Feb 2021 | |
Publication process dates | |
Deposited | 04 Mar 2021 |
Accepted | 23 May 2020 |
Output status | Published |
Publisher's version | License |
Copyright Statement | © The Author(s) 2020 |
Digital Object Identifier (DOI) | https://doi.org/10.1007/s10817-020-09566-9 |
Language | English |
https://repository.mdx.ac.uk/item/8946x
Download files
35
total views12
total downloads0
views this month0
downloads this month