{"id":400,"date":"2018-03-22T14:41:16","date_gmt":"2018-03-22T12:41:16","guid":{"rendered":"http:\/\/members.loria.fr\/AFilipiak\/?page_id=400"},"modified":"2018-03-22T14:41:16","modified_gmt":"2018-03-22T12:41:16","slug":"formal-analysis-of-the-belenios-vs-protocol-vote-confidentiality-voting-server-voting-device-authentication-credentials-compromised-and-voter-does-not-audit-the-voting-sheet","status":"publish","type":"page","link":"https:\/\/members.loria.fr\/AFilipiak\/formal-analysis-of-the-belenios-vs-protocol\/formal-analysis-of-the-belenios-vs-protocol-vote-confidentiality\/formal-analysis-of-the-belenios-vs-protocol-vote-confidentiality-voting-server-voting-device-authentication-credentials-compromised-and-voter-does-not-audit-the-voting-sheet\/","title":{"rendered":"Formal analysis of the Belenios VS protocol \u2013 Vote Confidentiality \u2013 Voting server, voting device, authentication credentials compromised and voter does not audit the voting sheet"},"content":{"rendered":"
(* CORRUPTION SCENARIO------------------------------------------------------- *)\r\n\r\n(* HONEST REGISTRAR---------------------------------------------------------- *)\r\n(* NO LEAK OF VOTING SHEET--------------------------------------------------- *)\r\n(* HONEST VOTER NO AUDIT----------------------------------------------------- *)\r\n(* NO NEED FOR VOTING SHEET AUDIT PROCESS------------------------------------ *)\r\n(* ROGUE VOTING DEVICE------------------------------------------------------- *)\r\n(* ROGUE VOTING SERVER NO ROGUE REGISTRAR------------------------------------ *)\r\n(* LOGIN-PWD STOLEN---------------------------------------------------------- *)\r\n\r\n(* TYPES--------------------------------------------------------------------- *)\r\n(* Since we do not use private channels to model secure network, we do that with\r\nsymmetric encryption, thus we need a type \"key\"------------------------------ *)\r\ntype key.\r\n\r\n(* Asymmetric encryption types----------------------------------------------- *)\r\ntype skey.\r\ntype pkey.\r\n\r\n(* Signature types----------------------------------------------------------- *)\r\ntype sskey.\r\ntype spkey.\r\n\r\n(* Other types used in the protocol------------------------------------------ *)\r\ntype rand.\r\ntype name.\r\ntype vote.\r\n\r\n(* NAMES--------------------------------------------------------------------- *)\r\n(* We define a public channel------------------------------------------------ *)\r\nfree public:channel.\r\n\r\n(* This name is used to generate the election asymmetric keys---------------- *)\r\nfree election:name.\r\n\r\n(* Two possible votes-------------------------------------------------------- *)\r\nfree A:vote.\r\nfree B:vote.\r\n\r\n(* Two honest voters--------------------------------------------------------- *)\r\nfree Eowyn:name.\r\nfree Mulan:name.\r\n\r\n(* A private channel for the tally model------------------------------------- *)\r\nfree tally_channel:channel[private].\r\n\r\n(* TABLES-------------------------------------------------------------------- *)\r\n(* The Public Bulletin Board------------------------------------------------- *)\r\ntable BULLETIN_BOARD(name,spkey,bitstring,bitstring).\r\n\r\n\r\n(* SYMMETRIC ENCRYPTION------------------------------------------------------ *)\r\n(* To model secure channels-------------------------------------------------- *)\r\nfun enc(bitstring,key):bitstring.\r\n\r\nreduc forall message:bitstring,k:key;\r\n dec(enc(message,k),k) = message.\r\n\r\n\r\n \r\n \r\n(* RANDOMIZED ASYMMETRIC ENCRYPTION------------------------------------------ *)\r\nfun sk(name):skey [private].\r\nfun pk(skey):pkey.\r\nfun aenc(bitstring,pkey,spkey,rand,rand):bitstring.\r\n\r\nreduc forall message:bitstring, seck:skey, spubk:spkey, r:rand, t:rand;\r\n adec(aenc(message,pk(seck),spubk,r,t), seck) = message.\r\n\r\n\r\n \r\n \r\n(* RANDOMIZED SIGNATURE------------------------------------------------------ *)\r\nfun spk(sskey):spkey.\r\nfun sign(bitstring, pkey, sskey, rand, rand):bitstring.\r\n\r\nreduc forall message:bitstring, pubk:pkey, sseck:sskey, r:rand, t:rand, s:rand, u:rand;\r\n verify(aenc(message,pubk,spk(sseck),r,t), sign(aenc(message,pubk,spk(sseck),r,t),pubk,sseck,s,u),spk(sseck)) = true.\r\n\r\n\r\n \r\n \r\n(* RANDOMIZATION------------------------------------------------------------- *)\r\nreduc forall message:bitstring, pubk:pkey, sseck:sskey,\r\n r:rand, s:rand, t:rand, u:rand, v:rand, w:rand;\r\n randomize_aenc (\r\n aenc(message,pubk,spk(sseck),r,v),\r\n sign(aenc(message,pubk,spk(sseck),r,v),pubk,sseck,s,w),\r\n pubk, spk(sseck),t,u\r\n )\r\n = aenc(message,pubk,spk(sseck),r,t).\r\n\r\nreduc forall message:bitstring, pubk:pkey, sseck:sskey,\r\n r:rand, s:rand, t:rand, u:rand, v:rand, w:rand;\r\n randomize_sign (\r\n aenc(message,pubk,spk(sseck),r,v),\r\n sign(aenc(message,pubk,spk(sseck),r,v),pubk,sseck,s,w),\r\n pubk,spk(sseck),t,u\r\n )\r\n = sign(aenc(message,pubk,spk(sseck),r,t),pubk,sseck,s,u) .\r\n\r\nletfun randomize (\r\n ballot:bitstring,signature:bitstring,\r\n pke:pkey,spk_n:spkey,r:rand,s:rand\r\n )\r\n = (\r\n randomize_aenc(ballot,signature,pke,spk_n,r,s),\r\n randomize_sign(ballot,signature,pke,spk_n,r,s)\r\n ).\r\n\r\n\r\n(* ELECTION SETUP------------------------------------------------------------ *)\r\n(* The election asymetric pair of keys--------------------------------------- *)\r\nletfun sk_e = sk(election).\r\nletfun pk_e = pk(sk(election)).\r\n\r\n(* The password associated to a voter ID------------------------------------- *)\r\nfun password(name):bitstring [private].\r\n\r\n(* The voter ID. To check if a voter ID is a valid one, is_registered is used *)\r\nfun voter_registration(name):name [private].\r\nreduc forall n:name;\r\n is_registered(voter_registration(n)) = true.\r\n\r\n\r\n \r\n \r\n(* REGISTRAR FUNCTIONS------------------------------------------------------- *)\r\n(* Type converting function-------------------------------------------------- *)\r\nfun tc_vote(vote):bitstring [data, typeConverter].\r\n\r\n(* A voting sheet generation function. It takes a vote and a signature key in in\r\nput and outputs the encrypted vote, its signature and the nonces (rand) used to \r\ngenerate the ballot---------------------------------------------------------- *)\r\nletfun voting_sheet(v:vote,ssk:sskey) =\r\n new r:rand;\r\n new s:rand;\r\n (\r\n aenc (tc_vote(v),pk_e,spk(ssk),r,r),\r\n sign (aenc(tc_vote(v),pk_e,spk(ssk),r,r),pk_e,ssk,s,s),\r\n r, s\r\n )\r\n .\r\n \r\n(* The list of valid credentials generated by the registrar is public. The funct\r\nion valid generates a certificate for the public signature key (it can only be u\r\nsed by the registrar) and is_valid is run to check if a public credential was in\r\ndeed produced by the registrar----------------------------------------------- *)\r\nfun valid(spkey):bitstring [private].\r\nreduc forall s:spkey;\r\n is_valid(valid(s),s)=true.\r\n\r\n\r\n(* HONEST REGISTRAR---------------------------------------------------------- *)\r\n(* The honest registrar process with rogue voters. It produces the voting sheets\r\nand outputs them on the public channel since voters are rogue---------------- *)\r\nlet Honest_Registrar_Rogue_Voter() =\r\n new ssk:sskey;\r\n out (public, (\r\n spk(ssk),valid(spk(ssk)),\r\n A,voting_sheet(A,ssk),\r\n B,voting_sheet(B,ssk)))\r\n .\r\n\r\n(* HONEST VOTER-------------------------------------------------------------- *)\r\n(* VOTER DOES NOT AUDIT VOTING SHEET AND CASTS BALLOT WITH ROGUE VOTING DEVICE*)\r\nlet Honest_Voter_no_audit(n:name,v:vote) =\r\n (* Freshly generated nonce used during the process. They are generated a\r\n t the beginning of the process to help ProVerif---------------------- *)\r\n new ssk_n:sskey;\r\n new rv:rand;\r\n new sv:rand;\r\n \r\n (* We model the registrar process alltogether with the voter process sin\r\n ce it is a honest entity. The public signature credentials are publicly \r\n output--------------------------------------------------------------- *)\r\n let spk_n = spk(ssk_n) in\r\n let val_n = valid(spk(ssk_n)) in \r\n out (public,(spk_n,val_n));\r\n \r\n (* Since the registrar is honest, the ballot scanned by the voter matche\r\n s her voting choice-------------------------------------------------- *)\r\n let vote_v = aenc(tc_vote(v),pk_e,spk_n,rv,rv) in\r\n let sign_v = sign(vote_v,pk_e,ssk_n,sv,sv) in\r\n \r\n (* For the election tally model, we need to send the association of the \r\n voter and her credential to the process modeling the tally----------- *) \r\n out (tally_channel, (n,spk_n));\r\n \r\n (* The voting device is rogue so the ballot is publicly output along the\r\n voter's authentication credentials----------------------------------- *) \r\n out (public, ((n,password(n),spk_n,val_n),(vote_v,sign_v)));\r\n \r\n (* The voter verifies her vote appears on the Public Bulletin Board-- *) \r\n get BULLETIN_BOARD(m,=spk_n,rand_ballot,sign_rand_ballot) in\r\n out (tally_channel, (n,spk_n))\r\n .\r\n\r\n(* ROGUE VOTING SERVER NO ROGUE REGISTRAR------------------------------------ *)\r\nlet Rogue_Voting_Server() =\r\n in (public,message:bitstring);\r\n let (\r\n (n:name,pwd_n:bitstring,spk_n:spkey,val_n:bitstring),\r\n (ballot:bitstring,signature:bitstring)\r\n )\r\n = message in\r\n \r\n (* Since the Bulletin Board can be audited by anyone, we made the assump\r\n tion that at least all displayed ballots are correctly signed-------- *)\r\n if (\r\n verify(ballot,signature,spk_n) = true\r\n && is_valid(val_n,spk_n)=true\r\n )\r\n then (\r\n (* The rogue voting server does not proceed to any verification\r\n other than the signature and publish all ballots it gets----- *)\r\n insert BULLETIN_BOARD(n,spk_n,ballot,signature);\r\n out (public,(spk_n,ballot,signature))\r\n )\r\n .\r\n\r\n(* TALLY PROCESS------------------------------------------------------------- *)\r\n(* The tally process is separated into two subprocesses. One that only tally the\r\nballots (Tally_Honest_Voter) and the other one that tally all ballots coming fro\r\nm all voters except our two honest ones (Tally)------------------------------ *)\r\n\r\nlet Tally_Honest_Voter() =\r\n (* The association between a honest voter and her public verification ke\r\n y is made------------------------------------------------------------ *)\r\n in (tally_channel, (=voter_registration(Eowyn),spk_Eowyn:spkey));\r\n in (tally_channel, (=voter_registration(Mulan),spk_Mulan:spkey));\r\n if spk_Eowyn <> spk_Mulan\r\n \r\n (* The tallying authority retrieves the ballots registered with our two \r\n honest voters' public signature verification key--------------------- *)\r\n then (\r\n get BULLETIN_BOARD(m_E,=spk_Eowyn,rand_ballot_Eowyn,sign_rand_ballot_Eowyn) in\r\n get BULLETIN_BOARD(m_M,=spk_Mulan,rand_ballot_Mulan,sign_rand_ballot_Mulan) in\r\n \r\n (* We model a mixnet ---------------------------------------- *)\r\n new mixnet:channel;\r\n (\r\n (\r\n out (mixnet,choice[rand_ballot_Eowyn,rand_ballot_Mulan])\r\n |\r\n out (mixnet,choice[rand_ballot_Mulan,rand_ballot_Eowyn])\r\n )\r\n |\r\n in (mixnet,b1:bitstring);\r\n in (mixnet,b2:bitstring);\r\n out (public,(adec(b1,sk_e),adec(b2,sk_e)))\r\n )\r\n )\r\n .\r\n \r\nlet Tally(spk_n:spkey) =\r\n (* The association between a honest voter and her public verification ke\r\n y is made------------------------------------------------------------ *)\r\n in (tally_channel, (=voter_registration(Eowyn),spk_Eowyn:spkey));\r\n in (tally_channel, (=voter_registration(Mulan),spk_Mulan:spkey));\r\n \r\n in (public, (=spk_n,b_n:bitstring,sign_n:bitstring));\r\n \r\n (* If the signature verification key used to cast the ballot is differen\r\n t from our honest voters' one, the ballot is simply decrypted and public\r\n ly output------------------------------------------------------------ *)\r\n if (\r\n spk_n <> spk_Eowyn\r\n && spk_n <> spk_Mulan\r\n && verify(b_n,sign_n,spk_n) = true\r\n )\r\n then (\r\n out (public, adec(b_n,sk_e))\r\n )\r\n . \r\n \r\n \r\n(* MAIN PROCESS-------------------------------------------------------------- *)\r\nprocess (\r\n (\r\n out (public,pk_e);\r\n out (public,voter_registration(Eowyn));\r\n out (public,voter_registration(Mulan))\r\n )\r\n |\r\n out (public, password(voter_registration(Eowyn)));\r\n out (public, password(voter_registration(Mulan)))\r\n |\r\n ! (\r\n new n:name;\r\n out (public, (n,voter_registration(n),password(voter_registration(n))))\r\n )\r\n |\r\n ! (\r\n Rogue_Voting_Server()\r\n )\r\n |\r\n ! (\r\n Honest_Registrar_Rogue_Voter()\r\n )\r\n |\r\n (\r\n Honest_Voter_no_audit(voter_registration(Eowyn),choice[A,B])\r\n )\r\n |\r\n (\r\n Honest_Voter_no_audit(voter_registration(Mulan),choice[B,A])\r\n )\r\n |\r\n (\r\n Tally_Honest_Voter()\r\n )\r\n |\r\n ! (\r\n in (public,spk_n:spkey);\r\n Tally(spk_n)\r\n )\r\n )<\/pre>\n","protected":false},"excerpt":{"rendered":"
(* CORRUPTION SCENARIO——————————————————- *)<\/p>\n
(* HONEST REGISTRAR———————————————————- *)
\n(* NO LEAK OF VOTING SHEET————————————————— *)
\n(* HONEST VOTER NO AUDIT—————————————————– *)
\n(* NO NEED FOR VOTING SHEET AUDIT PROCESS———————————— *)
\n(* ROGUE VOTING DEVICE——————————————————- *)
\n(* ROGUE VOTING SERVER NO ROGUE REGISTRAR———————————— *)
\n(* LOGIN-PWD STOLEN———————————————————- *)<\/p>\n
(* TYPES——————————————————————— *)
\n(* Since we do not use private channels to model secure network, we do that with
\nsymmetric encryption, thus we need a type \u00ab\u00a0key\u00a0\u00bb—————————— *)
\ntype key.<\/p>\n
(* Asymmetric encryption types———————————————– *)
\ntype skey.
\ntype pkey.<\/p>\n
(* Signature types———————————————————– *)
\ntype sskey.
\ntype spkey.<\/p>\n
(* Other types used in the protocol—————————————— *)
\ntype rand. <\/p>\n","protected":false},"author":159,"featured_media":0,"parent":371,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"page-fullwidth.php","meta":{"footnotes":""},"class_list":["post-400","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/members.loria.fr\/AFilipiak\/wp-json\/wp\/v2\/pages\/400","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/members.loria.fr\/AFilipiak\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/members.loria.fr\/AFilipiak\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/members.loria.fr\/AFilipiak\/wp-json\/wp\/v2\/users\/159"}],"replies":[{"embeddable":true,"href":"https:\/\/members.loria.fr\/AFilipiak\/wp-json\/wp\/v2\/comments?post=400"}],"version-history":[{"count":1,"href":"https:\/\/members.loria.fr\/AFilipiak\/wp-json\/wp\/v2\/pages\/400\/revisions"}],"predecessor-version":[{"id":402,"href":"https:\/\/members.loria.fr\/AFilipiak\/wp-json\/wp\/v2\/pages\/400\/revisions\/402"}],"up":[{"embeddable":true,"href":"https:\/\/members.loria.fr\/AFilipiak\/wp-json\/wp\/v2\/pages\/371"}],"wp:attachment":[{"href":"https:\/\/members.loria.fr\/AFilipiak\/wp-json\/wp\/v2\/media?parent=400"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}