All Rights Reserved
Copyright (c) 2017-2021 Ajay K. Eeralla
-Do not copy any proofs without my permission
We have formalized the proofs of vote privacy of the FOO voting protocol presented in the paper using the CCSA technique in the Coq proof assistant.
This work can be seen as an extension of the stuff presented in the following paper:
- Gergei Bana, Rohit Chadha, and Ajay Kumar Eeralla. Formal Analysis of Vote Privacy using Computationally Complete Symbolic Attacker, pp. 350-372, Computer Security: 23rd European Symposium on Research in Computer Security (ESORICS), Lecture Notes in Computer Science, Springer, September 2018.
- To compile the files, you will need to have installed Coq on your local machine.
- To download and install Coq on your machine, click on the link install coq.
-
To compile all the files simply type
make
-
To compile a single file
> coqc filename.v
- HTML Coqdoc files can be generated by
> coqdoc --html --toc --coqlib http://coq.inria.fr/stdlib/ -d _dirname_ *.v
- The directory webpages/coqdoc contains all the html files of the corresponding .v files
I have compiled the proofs using the Coq version 8.12.2 on MacOS with memory 32 GB.
- Ajay Kumar Eeralla --University of Missouri-Columbia
Copyright (c) 2017-2021, Ajay Kumar Eeralla ae266@mail.missouri.edu, University of Missouri-Columbia, USA