Commit 2d8dd4bb authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

started the bounded recursion implementation:

- added an example with the new syntax: helios.api
parent 944e5dbe
Pipeline #1634 passed with stage
in 1 minute and 3 seconds
let Voter[cid] sksig v pk =
new r0.
let ballot = enc(v,r0,pk) in
let zk = zkp(r0, v, ballot) in
out(cid, <<ballot,zk>,sign(<ballot, zk>, sksig)>);
let Outcome v1 v2 v3 sk =
(* We check for replayed ballots *)
if EQ(v1,v2) then
out(cres,replayedBallot())
else if EQ(v1,v3) then
out(cres,replayedBallot())
else if EQ(v2,v3) then
out(cres,replayedBallot())
else
(* No replay, we compute the result *)
let res1 = dec(v1,sk) in
let res2 = dec(v2,sk) in
let res3 = dec(v3,sk) in
let acount = count(A(),res1,res2,res3) in
let bcount = count(B(),res1,res2,res3) in
out(cres,<acount,bcount>);
letrec SubTally{i} v1 v2 v3 bv1 bv2 pksig1 pksig2 pksig3 sk =
in(c, x).
let content = pi1(x) in
if EQ(checksig(pi1(x),pi2(x),pksig1),sigok()) then
(if EQ(checkzkp(pi2(pi1(x)),pi1(pi1(x))),zkpok()) then
(SubTally
(pi1(pi1(x))) v2 v3
true bv2
pksig1 pksig2 pksig3 sk)
else
(SubTally v1 v2 v3 bv1 bv2 pksig1 pksig2 pksig3 sk))
else if EQ(checksig(pi1(x),pi2(x),pksig2),sigok()) then
(if EQ(checkzkp(pi2(pi1(x)),pi1(pi1(x))),zkpok()) then
(SubTally
v1 (pi1(pi1(x))) v3
bv1 true
pksig1 pksig2 pksig3 sk)
else
(SubTally v1 v2 v3 bv1 bv2 pksig1 pksig2 pksig3 sk))
else if EQ(checksig(pi1(x),pi2(x),pksig3),sigok()) then
(if EQ(checkzkp(pi2(pi1(x)),pi1(pi1(x))),zkpok()) then
(SubTally
v1 v2 (pi1(pi1(x)))
bv1 bv2
pksig1 pksig2 pksig3 sk)
else
(SubTally v1 v2 v3 bv1 bv2 pksig1 pksig2 pksig3 sk))
else
(SubTally v1 v2 v3 bv1 bv2 pksig1 pksig2 pksig3 sk);
letrec SubTally{0} v1 v2 v3 bv1 bv2 pksig1 pksig2 pksig3 sk =
if bv1 then
(if bv2 then
(Outcome v1 v2 v3 sk)
else
out(cres,badVotes()))
else
out(cres,badVotes());
let P vc1 vc2 =
new n.
let pk = pk(n) in
let sk = sk(n) in
out(cinit,pk).
new nksig1.
new nksig2.
new nksig3.
let sksig1 = sksig(nksig1) in
let pksig1 = pksig(nksig1) in
out(cinit,pksig1).
let sksig2 = sksig(nksig2) in
let pksig2 = pksig(nksig2) in
out(cinit,pksig2).
let sksig3 = sksig(nksig3) in
let pksig3 = pksig(nksig3) in
out(cinit,pksig3).
out(cinit,sksig3).
((Vote[c1] sksig1 vc1 pk) | (Vote[c2] sksig2 vc2 pk)
| (SubTally{3} (N()) (N()) (N()) false false pksig1 pksig2 pksig3 sk));
goal: P (A()) (B()) ~ P (B()) (A())
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment