Abstract
We present a case study in verified security for realistic systems: the implementation of a conference management system, whose functional kernel is faithfully represented in the Isabelle theorem prover, where we specify and verify confidentiality properties. The various theoretical and practical challenges posed by this development led to a novel security model and verification method generally applicable to systems describable as input-output automata. © 2014 Springer International Publishing.
Cite
CITATION STYLE
Kanav, S., Lammich, P., & Popescu, A. (2014). A conference management system with verified document confidentiality. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8559 LNCS, pp. 167–183). Springer Verlag. https://doi.org/10.1007/978-3-319-08867-9_11
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
