(* CORRUPTION SCENARIO------------------------------------------------------- *)
(* ROGUE REGISTRAR----------------------------------------------------------- *)
(* HONEST VOTER AUDIT-------------------------------------------------------- *)
(* HONEST VOTING SHEET AUDIT------------------------------------------------- *)
(* HONEST VOTING DEVICE------------------------------------------------------ *)
(* HONEST VOTING SERVER------------------------------------------------------ *)
(* LOGIN-PWD STOLEN---------------------------------------------------------- *)
set traceDisplay = long.
(* TYPES--------------------------------------------------------------------- *)
type key.
type skey.
type pkey.
type sskey.
type spkey.
type rand.
type name.
type vote.
type status.
free public:channel.
free election:name.
free A:vote.
free B:vote.
free H:status.
free C:status.
(* TABLES-------------------------------------------------------------------- *)
table BULLETIN_BOARD(name,spkey,bitstring,bitstring).
(* EVENTS-------------------------------------------------------------------- *)
event VOTER(name,spkey,status).
event VOTE(name,bitstring,rand).
event VERIFIED(name,bitstring).
event GOING_TO_TALLY(name,spkey,bitstring,bitstring).
(* SYMMETRIC ENCRYPTION------------------------------------------------------ *)
fun enc(bitstring,key):bitstring.
reduc forall message:bitstring,k:key;
dec(enc(message,k),k) = message.
(* ASYMMETRIC ENCRYPTION----------------------------------------------------- *)
fun sk(name):skey [private].
fun pk(skey):pkey.
fun aenc(bitstring,pkey,spkey,rand,rand):bitstring.
reduc forall message:bitstring, seck:skey, spubk:spkey, r:rand, t:rand;
adec(aenc(message,pk(seck),spubk,r,t), seck) = message.
(* SIGNATURE----------------------------------------------------------------- *)
fun spk(sskey):spkey.
fun sign(bitstring, pkey, sskey, rand, rand):bitstring.
reduc forall message:bitstring, pubk:pkey, sseck:sskey, r:rand, t:rand, s:rand, u:rand;
verify(aenc(message,pubk,spk(sseck),r,t), sign(aenc(message,pubk,spk(sseck),r,t),pubk,sseck,s,u),spk(sseck)) = true.
(* RANDOMIZATION------------------------------------------------------------- *)
reduc forall message:bitstring, pubk:pkey, sseck:sskey,
r:rand, s:rand, t:rand, u:rand, v:rand, w:rand;
randomize_aenc (
aenc(message,pubk,spk(sseck),r,v),
sign(aenc(message,pubk,spk(sseck),r,v),pubk,sseck,s,w),
pubk, spk(sseck),t,u
)
= aenc(message,pubk,spk(sseck),r,t).
reduc forall message:bitstring, pubk:pkey, sseck:sskey,
r:rand, s:rand, t:rand, u:rand, v:rand, w:rand;
randomize_sign (
aenc(message,pubk,spk(sseck),r,v),
sign(aenc(message,pubk,spk(sseck),r,v),pubk,sseck,s,w),
pubk,spk(sseck),t,u
)
= sign(aenc(message,pubk,spk(sseck),r,t),pubk,sseck,s,u) .
letfun randomize (
ballot:bitstring,signature:bitstring,
pke:pkey,spk_n:spkey,r:rand,s:rand
)
= (
randomize_aenc(ballot,signature,pke,spk_n,r,s),
randomize_sign(ballot,signature,pke,spk_n,r,s)
).
(* ELECTION SETUP------------------------------------------------------------ *)
letfun sk_e = sk(election).
letfun pk_e = pk(sk(election)).
fun password(name):bitstring [private].
fun voter_registration(name):name [private].
reduc forall n:name;
is_registered(voter_registration(n)) = true.
(* REGISTRAR FUNCTIONS------------------------------------------------------- *)
fun tc_vote(vote):bitstring [data, typeConverter].
letfun voting_sheet(v:vote,ssk:sskey) =
new r:rand;
new s:rand;
(
aenc (tc_vote(v),pk_e,spk(ssk),r,r),
sign (aenc(tc_vote(v),pk_e,spk(ssk),r,r),pk_e,ssk,s,s),
r, s
)
.
fun valid(spkey):bitstring [private].
reduc forall s:spkey;
is_valid(valid(s),s)=true.
(* ROGUE REGISTRAR----------------------------------------------------------- *)
(*
free ALIVENESS_ROGUE_REGISTRAR:bitstring [private].
query attacker(ALIVENESS_ROGUE_REGISTRAR).
let Rogue_Registrar(voting_sheet_channel:key,a:vote,b:vote) =
new ssk:sskey;
out (public,(voting_sheet_channel,ssk,spk(ssk),valid(spk(ssk))));
out (public,ALIVENESS_ROGUE_REGISTRAR)
.
*)
(* HONEST VOTER-------------------------------------------------------------- *)
(* VOTER AUDITS VOTING SHEET------------------------------------------------- *)
free ALIVENESS_HONEST_VOTER_A_AUDIT:bitstring [private].
query attacker(ALIVENESS_HONEST_VOTER_A_AUDIT).
free ALIVENESS_VERIFICATION_A_AUDIT:bitstring [private].
query attacker(ALIVENESS_VERIFICATION_A_AUDIT).
free ALIVENESS_HONEST_VOTER_B_AUDIT:bitstring [private].
query attacker(ALIVENESS_HONEST_VOTER_B_AUDIT).
free ALIVENESS_VERIFICATION_B_AUDIT:bitstring [private].
query attacker(ALIVENESS_VERIFICATION_B_AUDIT).
let Honest_Voter_A_audit(n:name,voting_device_channel:key,public_channel:key) =
new vote_id:rand;
in (public, (spk_n:spkey,val_n:bitstring,=A,(vote_a:bitstring,sign_a:bitstring,ra:rand,sa:rand)));
event VOTER(n,spk_n,H);
if (
aenc(tc_vote(A),pk_e,spk_n,ra,ra) = vote_a
&& verify(vote_a,sign_a,spk_n) = true
)
then (
event VOTE(n,tc_vote(A),vote_id);
out (public, enc((
n,password(n),
spk_n,val_n,
vote_a,sign_a),
voting_device_channel));
out (public,ALIVENESS_HONEST_VOTER_A_AUDIT);
in (public,ack:bitstring);
let (
=n,=password(n),=spk_n,r:rand
)
= dec(ack,public_channel) in
get BULLETIN_BOARD(m,=spk_n,rand_ballot,sign_rand_ballot) in
event VERIFIED(n,tc_vote(A));
out (public,ALIVENESS_VERIFICATION_A_AUDIT)
)
.
let Honest_Voter_B_audit(n:name,voting_device_channel:key,public_channel:key) =
new vote_id:rand;
in (public, (spk_n:spkey,val_n:bitstring,=B,(vote_b:bitstring,sign_b:bitstring,rb:rand,sb:rand)));
event VOTER(n,spk_n,H);
if (
aenc(tc_vote(B),pk_e,spk_n,rb,rb) = vote_b
&& verify(vote_b,sign_b,spk_n) = true
)
then (
event VOTE(n,tc_vote(B),vote_id);
out (public, enc((
n,password(n),
spk_n,val_n,
vote_b,sign_b),
voting_device_channel));
out (public,ALIVENESS_HONEST_VOTER_B_AUDIT);
in (public,ack:bitstring);
let (
=n,=password(n),=spk_n,r:rand
)
= dec(ack,public_channel) in
get BULLETIN_BOARD(m,=spk_n,rand_ballot,sign_rand_ballot) in
event VERIFIED(n,tc_vote(B));
out (public,ALIVENESS_VERIFICATION_B_AUDIT)
)
.
(* ROGUE VOTER--------------------------------------------------------------- *)
free ALIVENESS_ROGUE_VOTER:bitstring [private].
query attacker(ALIVENESS_ROGUE_VOTER).
let Rogue_Voter(n:name) =
in (public, message:bitstring);
let (
spk_n:spkey,val_n:bitstring,
a:vote,(vote_a:bitstring,sign_a:bitstring,ra:rand,sa:rand),
b:vote,(vote_b:bitstring,sign_b:bitstring,rb:rand,sb:rand)
)
= message in
event VOTER(n,spk_n,C);
out (public,(password(n),message));
out (public,ALIVENESS_ROGUE_VOTER)
.
(* HONEST VOTING DEVICE------------------------------------------------------ *)
free ALIVENESS_HONEST_VOTING_DEVICE:bitstring [private].
query attacker(ALIVENESS_HONEST_VOTING_DEVICE).
let Honest_Voting_Device(voting_device_channel:key,server_channel:key) =
new rv:rand;
new sv:rand;
in (public,message:bitstring);
let (
n:name,pwd_n:bitstring,
spk_n:spkey,val_n:bitstring,
vote_v:bitstring,sign_v:bitstring
)
= dec(message,voting_device_channel) in
out (public, enc((
(n,pwd_n,spk_n,val_n),
randomize(vote_v,sign_v,pk_e,spk_n,rv,sv)),
server_channel));
out (public,randomize(vote_v,sign_v,pk_e,spk_n,rv,sv));
out (public,ALIVENESS_HONEST_VOTING_DEVICE)
.
(* HONEST VOTING SERVER------------------------------------------------------ *)
free ALIVENESS_HONEST_VOTING_SERVER:bitstring [private].
query attacker(ALIVENESS_HONEST_VOTING_SERVER).
let Honest_Voting_Server(server_channel:key,public_channel:key) =
new rv:rand;
new sv:rand;
new ack:rand;
in (public,message:bitstring);
let (
(n:name,pwd_n:bitstring,spk_n:spkey,val_n:bitstring),
(ballot:bitstring,signature:bitstring)
)
= dec(message,server_channel) in
if (
is_registered(n)=true
&& pwd_n=password(n)
&& is_valid(val_n,spk_n)=true
&& verify(ballot,signature,spk_n) = true
)
then (
let (rand_ballot:bitstring,rand_sign:bitstring)
= randomize(ballot,signature,pk_e,spk_n,rv,sv) in
event GOING_TO_TALLY(n,spk_n,rand_ballot,adec(rand_ballot,sk_e));
insert BULLETIN_BOARD(n,spk_n,rand_ballot,rand_sign);
out (public,enc((n,pwd_n,spk_n,ack),public_channel));
out (public,(spk_n,val_n,rand_ballot,rand_sign));
out (public,ALIVENESS_HONEST_VOTING_SERVER)
)
else 0
.
(* SECURITY PROPERTIES------------------------------------------------------- *)
(* HONEST VOTE CONSISTENCY--------------------------------------------------- *)
query n:name,v:bitstring,k:rand;
event(VERIFIED(n,v)) ==> event(VOTE(n,v,k)).
(* CAST AS INTENDED (ID)----------------------------------------------------- *)
query ID:name,v:bitstring,
b:bitstring,r:rand,
spk_n:spkey,spk_1:spkey,spk_2:spkey;
event(GOING_TO_TALLY(ID,spk_n,b,v))
==>
(
(
event(VOTER(ID,spk_1,C))
)
||
(
event(VOTER(ID,spk_2,H))
&&
event(VOTE(ID,v,r))
)
).
(* TALLIED AS CAST (ID)------------------------------------------------------ *)
query ID:name,v:bitstring,
v1:bitstring,v2:bitstring,r1:rand,r2:rand,
spk_n:spkey,b:bitstring;
event(VERIFIED(ID,v))
==>
(
event(GOING_TO_TALLY(ID,spk_n,b,v))
||
(
event(VOTE(ID,v1,r1))
&&
event(VOTE(ID,v2,r2))
&&
r1 r2
)
).
(* CAST AS INTENDED (CRED)--------------------------------------------------- *)
query ID:name,CRED:spkey,v:bitstring,
b:bitstring,r:rand,
n1:name,n2:name;
event(GOING_TO_TALLY(n1,CRED,b,v))
==>
(
(
event(VOTER(n2,CRED,C))
)
||
(
event(VOTER(ID,CRED,H))
&&
event(VOTE(ID,v,r))
)
).
(* TALLIED AS CAST (CRED)---------------------------------------------------- *)
query ID:name,v:bitstring,
v1:bitstring,v2:bitstring,r1:rand,r2:rand,
n:name,CRED:spkey,b:bitstring;
event(VERIFIED(ID,v))
==>
(
(
event(VOTER(ID,CRED,H))
&&
event(GOING_TO_TALLY(n,CRED,b,v))
)
||
(
event(VOTE(ID,v1,r1))
&&
event(VOTE(ID,v2,r2))
&&
r1 r2
)
).
(* MAIN PROCESS-------------------------------------------------------------- *)
process (
(
out (public,pk_e)
)
|
! (
new n:name;
out (public, (n,voter_registration(n),password(voter_registration(n))))
)
|
! (
new ssk:sskey;
out (public, (ssk,spk(ssk),valid(spk(ssk))))
)
|
! (
in (public, n:name);
new voting_device_channel:key;
new server_channel:key;
new public_channel:key;
(
Honest_Voter_A_audit(voter_registration(n),voting_device_channel,public_channel)
|
Honest_Voting_Device(voting_device_channel,server_channel)
|
Honest_Voting_Server(server_channel,public_channel)
)
)
|
! (
in (public, n:name);
new voting_device_channel:key;
new server_channel:key;
new public_channel:key;
(
Honest_Voter_B_audit(voter_registration(n),voting_device_channel,public_channel)
|
Honest_Voting_Device(voting_device_channel,server_channel)
|
Honest_Voting_Server(server_channel,public_channel)
)
)
|
! (
in (public,server_channel:key);
in (public,public_channel:key);
Honest_Voting_Server(server_channel,public_channel)
)
|
! (
in (public,n:name);
(
Rogue_Voter(voter_registration(n))
)
)
)
