{"id":333,"date":"2019-05-09T22:06:14","date_gmt":"2019-05-09T20:06:14","guid":{"rendered":"http:\/\/members.loria.fr\/JLallemand\/?page_id=333"},"modified":"2019-05-21T13:18:44","modified_gmt":"2019-05-21T11:18:44","slug":"beleniosvs","status":"publish","type":"page","link":"https:\/\/members.loria.fr\/JLallemand\/beleniosvs\/","title":{"rendered":"BeleniosVS: Secrecy and Verifiability against a Corrupted Voting Device"},"content":{"rendered":"<p><strong>REQUIREMENTS TO VERIFY THE MODELS<\/strong><\/p>\n<ul>\n<li>The <a href=\"https:\/\/prosecco.gforge.inria.fr\/personal\/bblanche\/proverif\/\">ProVerif<\/a> protocol verifier. ProVerif can be installed using the Opam package manager by running<br \/>\n<code>opam install proverif<\/code><br \/>\nIt is also available directly from the <a href=\"https:\/\/prosecco.gforge.inria.fr\/personal\/bblanche\/proverif\/\">ProVerif website<\/a>. Versions 1.98pl1 and 2.00 are known to work.<br \/>\nNote that the scripts assume ProVerif is already installed and is in the shell&rsquo;s <code>PATH<\/code>.<\/li>\n<li>The <a href=\"https:\/\/en.wikipedia.org\/wiki\/Bash_(Unix_shell)\">bash<\/a> shell and the <a href=\"https:\/\/en.wikipedia.org\/wiki\/Perl\">perl<\/a> interpreter are required by the scripts used to generate and verify the models for all corruption scenarios.<br \/>\nThese scripts are optional, as we provide all generated files, and ProVerif can be run manually on them.<\/li>\n<\/ul>\n<p><strong>MODEL FILES<\/strong><\/p>\n<p><a href=\"https:\/\/members.loria.fr\/JLallemand\/files\/beleniosvs\/model-file.zip\">[Download]<\/a><\/p>\n<p>We provide all the ProVerif model files for the analysis of the BeleniosVS protocol, as well as the scripts we used to generate them.<br \/>\nThe files are organised in three folders named after the security property they model.<\/p>\n<ul>\n<li><strong>Privacy<\/strong><br \/>\nThese files formalise the privacy property for the BeleniosVS protocol, under different corruption scenarios.<br \/>\nThe scenario considered is described precisely in the beginning of each file. In a nutshell:<\/p>\n<ul>\n<li><a href=\"https:\/\/members.loria.fr\/JLallemand\/files\/beleniosvs\/priv-all-honest.pv\"><em>priv-all-honest.pv<\/em><\/a>: all entities are honest.<\/li>\n<li><a href=\"https:\/\/members.loria.fr\/JLallemand\/files\/beleniosvs\/priv-registrar.pv\"><em>priv-registrar.pv<\/em><\/a>: the registrar is dishonest (and thus the voting sheets are leaked, whether the voters lose them or not).<\/li>\n<li><a href=\"https:\/\/members.loria.fr\/JLallemand\/files\/beleniosvs\/priv-votingdevice.pv\"><em>priv-votingdevice.pv<\/em><\/a>: the voting devices are dishonest (and thus leak the passwords, whether the voters lose them or not).<\/li>\n<li><a href=\"https:\/\/members.loria.fr\/JLallemand\/files\/beleniosvs\/priv-votingserver.pv\"><em>priv-votingserver.pv<\/em><\/a>: the voting server is dishonest.<\/li>\n<li><a href=\"https:\/\/members.loria.fr\/JLallemand\/files\/beleniosvs\/priv-votingserver-votingdevice.pv\"><em>priv-votingserver-votingdevice.pv<\/em><\/a>: the voting server and voting devices are dishonest.<\/li>\n<li><a href=\"https:\/\/members.loria.fr\/JLallemand\/files\/beleniosvs\/priv-audit.pv\"><em>priv-audit.pv<\/em><\/a>: the audit devices are dishonest.<\/li>\n<li><a href=\"https:\/\/members.loria.fr\/JLallemand\/files\/beleniosvs\/priv-audit-vs.pv\"><em>priv-audit-vs.pv<\/em><\/a>: the audit devices are dishonest, and voters lose their voting sheets.<\/li>\n<li><a href=\"https:\/\/members.loria.fr\/JLallemand\/files\/beleniosvs\/priv-vs.pv\"><em>priv-vs.pv<\/em><\/a>: the voters lose their voting sheets.<\/li>\n<li><a href=\"https:\/\/members.loria.fr\/JLallemand\/files\/beleniosvs\/priv-pwd.pv\"><em>priv-pwd.pv<\/em><\/a>: the voters lose their passwords.<\/li>\n<li><a href=\"https:\/\/members.loria.fr\/JLallemand\/files\/beleniosvs\/priv-A-loses-VS-B-loses-pwd.pv\"><em>priv-A-loses-VS-B-loses-pwd.pv<\/em><\/a>: Alice loses her voting sheet and\/or her audit device is dishonest, Bob loses his password and\/or his voting device is dishonest.<\/li>\n<li><a href=\"https:\/\/members.loria.fr\/JLallemand\/files\/beleniosvs\/priv-A-loses-pwd-B-loses-VS.pv\"><em>priv-A-loses-pwd-B-loses-VS.pv<\/em><\/a>: Alice loses her password and\/or her voting device is dishonest, Bob loses his voting sheet and\/or his audit device is dishonest.<\/li>\n<\/ul>\n<\/li>\n<li><strong>Receipt-freeness<\/strong><br \/>\nThese files formalise the receipt-freeness property for the BeleniosVS protocol, under different corruption scenarios.<br \/>\nThe scenario considered is described precisely in the beginning of each file. In a nutshell:<\/p>\n<ul>\n<li><a href=\"https:\/\/members.loria.fr\/JLallemand\/files\/beleniosvs\/rf-all-honest.pv\"><em>rf-all-honest.pv<\/em><\/a>: all entities are honest.<\/li>\n<li><a href=\"https:\/\/members.loria.fr\/JLallemand\/files\/beleniosvs\/rf-audit.pv\"><em>rf-audit.pv<\/em><\/a>: the audit devices are dishonest (and thus the voting sheets are leaked, whether the voters lose them or not).<\/li>\n<li><a href=\"https:\/\/members.loria.fr\/JLallemand\/files\/beleniosvs\/rf-registrar.pv\"><em>rf-registrar.pv<\/em><\/a>: the registrar is dishonest (and thus the voting sheets are leaked, whether the voters lose them or not).<\/li>\n<\/ul>\n<\/li>\n<li><strong>Verifiability<\/strong><br \/>\nThis folder contains the scripts and files needed to generate the ProVerif files to analyse verifiability for the BeleniosVS protocol.<br \/>\nWe verify the necessary conditions established in the paper, under different corruption scenarios.<\/p>\n<ul>\n<li><strong>Source files<\/strong><br \/>\nThe <em>*.pv<\/em> files in the <em>verifiability<\/em> folder contain pieces of ProVerif processes modelling the different entities of the protocol.<br \/>\nThese are not valid ProVerif files, but instead contain some macros that allow the scripts to make the entities honest or dishonest.<br \/>\nThe scripts then combine these files to generate the complete file for each scenario.<\/li>\n<li><strong>Scripts<\/strong><br \/>\nThe <a href=\"https:\/\/members.loria.fr\/JLallemand\/files\/beleniosvs\/README\"><em>README<\/em><\/a> file contains a description of what each script does, and how to use them. In short:<\/p>\n<ul>\n<li><a href=\"https:\/\/members.loria.fr\/JLallemand\/files\/beleniosvs\/gen.pl\"><em>gen.pl<\/em><\/a>: a script that uses the source files to generate a proverif file modelling a corruption scenario that is described by the options passed to it.<br \/>\nFor instance, for a dishonest registrar and dishonest voting device:<br \/>\n<code>perl .\/gen.pl --registrar dishonest --votingdevice dishonest<\/code><\/li>\n<li><a href=\"https:\/\/members.loria.fr\/JLallemand\/files\/beleniosvs\/gen-both.pl\"><em>gen-both.pl<\/em><\/a>: a script used to generate the file for the special case where some of the voters lose their voting sheet, while others lose their password.<br \/>\nRun with:<br \/>\n<code>perl .\/gen-both.pl<\/code><\/li>\n<li><a href=\"https:\/\/members.loria.fr\/JLallemand\/files\/beleniosvs\/scan.pl\"><em>scan.pl<\/em><\/a>: a script that reads the output of ProVerif on one of the generated files, parses it, and applies the theorems stated in the article to determine whether verifiability is proved or not. The relevant theorem is applied, depending on options indicating whether the server and registrar are honest or not.<br \/>\nFor instance:<br \/>\n<code>proverif &lt;file.pv&gt; | perl .\/scan.pl --registrar honest --votingserver dishonest<\/code><\/li>\n<li><a href=\"https:\/\/members.loria.fr\/JLallemand\/files\/beleniosvs\/all.sh\"><em>all.sh<\/em><\/a>: uses the previous three scripts to generate the ProVerif files for each scenario, run ProVerif on them, and print the results of the analysis.<br \/>\nThe generated files are stored in the generated-files folder.<br \/>\nRun with:<br \/>\n<code>bash .\/all.sh<\/code><\/li>\n<\/ul>\n<\/li>\n<li><strong>Model files<\/strong><br \/>\nThe ProVerif files for each scenario have been pre-generated, and are provided in the generated-files folder.Each file contains a description of the scenario it models. The files are also named accordingly, following the format \u00ab\u00a0<em>rx ax dx sx vsx pwdx.pv<\/em>\u00ab\u00a0, which indicates the honesty or dishonesty status of each entity:<\/p>\n<ul>\n<li><em>r<\/em> for the registrar, <em>a<\/em> for the audit device, <em>d<\/em> for the voting device, <em>s<\/em> for the voting server, <em>vs<\/em> for the voting sheet, <em>pwd<\/em> for the password.<\/li>\n<li>0 indicates a honest entity\/secret data, while 1 indicates a dishonest entity\/leaked data. In the case of the audit device only, 2 indicates that no audit is performed.<br \/>\nFor instance, \u00ab\u00a0<em>r0 a2 d0 s1 vs1 pwd1.pv<\/em>\u00a0\u00bb models the scenario where the registrar is honest, no audit is performed, the voting device is honest, the voting server is dishonest, and the voters leak both their voting sheet and their password.<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>REQUIREMENTS TO VERIFY THE MODELS<\/p>\n<ul>\n<li>The <a href=\"https:\/\/prosecco.gforge.inria.fr\/personal\/bblanche\/proverif\/\">ProVerif<\/a> protocol verifier. ProVerif can be installed using the Opam package manager by running<br \/>\nopam install proverif<br \/>\nIt is also available directly from the <a href=\"https:\/\/prosecco.gforge.inria.fr\/personal\/bblanche\/proverif\/\">ProVerif website<\/a>. Versions 1.98pl1 and 2.00 are known to work.<br \/>\nNote that the scripts assume ProVerif is already installed and is in the shell&rsquo;s PATH.<\/li>\n<li>The <a href=\"https:\/\/en.wikipedia.org\/wiki\/Bash_(Unix_shell)\">bash<\/a> shell and the <a href=\"https:\/\/en.wikipedia.org\/wiki\/Perl\">perl<\/a> interpreter are required by the scripts used to generate and verify the models for all corruption scenarios.<br \/>\nThese scripts are optional,<\/li>\n<\/ul>\n","protected":false},"author":135,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-333","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/members.loria.fr\/JLallemand\/wp-json\/wp\/v2\/pages\/333","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/members.loria.fr\/JLallemand\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/members.loria.fr\/JLallemand\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/members.loria.fr\/JLallemand\/wp-json\/wp\/v2\/users\/135"}],"replies":[{"embeddable":true,"href":"https:\/\/members.loria.fr\/JLallemand\/wp-json\/wp\/v2\/comments?post=333"}],"version-history":[{"count":10,"href":"https:\/\/members.loria.fr\/JLallemand\/wp-json\/wp\/v2\/pages\/333\/revisions"}],"predecessor-version":[{"id":346,"href":"https:\/\/members.loria.fr\/JLallemand\/wp-json\/wp\/v2\/pages\/333\/revisions\/346"}],"wp:attachment":[{"href":"https:\/\/members.loria.fr\/JLallemand\/wp-json\/wp\/v2\/media?parent=333"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}