### Abstract

This entry contains the confidentiality verification of the (functional kernel of) the CoCon conference management system [1, 2]. The confidentiality properties refer to the documents managed by the system, namely papers, reviews, discussion logs and acceptance/rejection decisions, and also to the assignment of reviewers to papers. They have all been formulated as instances of BD Security [3, 4] and verified using the BD Security unwinding technique.

### License

BSD License

### Topics

- Computer science/Security

### Session CoCon

- Prelim
- System_Specification
- Automation_Setup
- Safety_Properties
- Observation_Setup
- Paper_Intro
- Paper_Value_Setup
- Paper_Aut_PC
- Paper_Aut
- Paper_All
- Review_Intro
- Review_Value_Setup
- Review_RAut
- Review_RAut_NCPC
- Review_RAut_NCPC_PAut
- Review_All
- Discussion_Intro
- Discussion_Value_Setup
- Discussion_NCPC
- Discussion_All
- Decision_Intro
- Decision_Value_Setup
- Decision_NCPC
- Decision_NCPC_Aut
- Decision_All
- Reviewer_Assignment_Intro
- Reviewer_Assignment_Value_Setup
- Reviewer_Assignment_NCPC
- Reviewer_Assignment_NCPC_Aut
- Reviewer_Assignment_All
- Traceback_Properties
- All_BD_Security_Instances_for_CoCon

### Depends on

- Bounded-Deducibility Security
- Fresh identifiers

## Cite

×

CoCon-AFP

    @article{CoCon-AFP,
      author  = {Andrei Popescu and Peter Lammich and Thomas Bauereiss},
      title   = {CoCon: A Confidentiality-Verified Conference Management System},
      journal = {Archive of Formal Proofs},
      month   = {August},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/CoCon.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1