theory voter_attendance_verification
begin
builtins: asymmetric-encryption, diffie-hellman, hashing, multiset
functions: pk/1, aenc/2, adec/2, h1/1, h2/1
equations: adec(aenc(m1, pk(sk)), sk) = m1 // Adapted from the examples given in the Tamarin manual [1].
/*===============================================================================NOTES==============================================================================================
This Tamarin .spthy file formally proves participation privacy in the proposed voter attendance verification protocol.
The results obtained from this work have been described in CHAPTER 4 of the PhD Thesis titled "Secure Voter Authentication for Poll-site Elections in Developing Countries".
The web bulletin board (WBB) will consist of unique voter IDs, in addition to their encrypted secret integer, plaintext integer, voting status and attendance ciphertext. See Table 3.1 in the applicable thesis chapter.
In this Tamarin model, any agent labelled with the 'Honest' action fact is deemed to: (1) Keep sensitive data confidential. (2) Have a private key that has not been compromised by an adversary (if applicable) [1].
It should be noted that we do not model a threshold of registrars - only one registrar has been modelled with Tamarin.
We consider a Dolev-Yao adversary in this Tamarin model.
This Tamarin model was revised and finalised on 23 November 2020.
Modeller: Olukayode Nicholas Akinyokun
Student ID: 807141
===================================================================================================================================================================================*/
rule registrar_generate_keys_pairs: // The registrar's key generation process. Here, the registrar generates their public and private keys, respectively.
[Fr(~RGR_priv_key) ] --[ OnlyOnce() ]-> // We have abbreviated the registrar as RGR.
[!RGRSecretKey($RGR, ~RGR_priv_key), !RGRPublicKey($RGR, pk(~RGR_priv_key))]
rule define_registrar: // We initialise the registrar's ID and role.
let
sec_param = 'k' // The one-time security parameter for the election.
max_voters = 'mv' // The maximum number of voters that are expected to register and vote at a specific polling station p.
in
[Fr(~rgr_id), !RGRSecretKey($RGR, ~RGR_priv_key), !RGRPublicKey($RGR, pk(~RGR_priv_key))]
--[Create_RGR(~rgr_id, $RGR), Honest($RGR), Role('RGR')]->
[St_RGR_1($RGR, ~rgr_id, ~RGR_priv_key, pk(~RGR_priv_key), max_voters, sec_param), !RGR_Data(~rgr_id)]
rule define_pollworker: // We initialise the poll worker's role and ID.
let
PCK = 'Clerk' // The poll worker's role is abbreviated as PCK.
in
[Fr(~pClerk_id)]
--[Create_PClerk(~pClerk_id, PCK), Honest(PCK), Role('PCK')]->
[St_PClerk_1(PCK, ~pClerk_id), !PClerk_Data(~pClerk_id)]
rule define_election_auth: // We initialise the election authority's role and ID.
[ ]
--[Create_EA($EA, $EA_name), Honest($EA), Role('EA')]->
[St_ElecAuth_1($EA, $EA_name), Out($EA_name), !ElecAuth_Data($EA_name, $EA)]
rule initialize_voter1: // We initialise voter 1's role and biometric data.
let
// Voter 1 biometric data.
V1_bio = 'b1'
in
[ ]
--[Create_Voter1($V1), Honest($V1), Role('V1')]->
[State_V_1($V1, V1_bio), !Voter1_Attr(V1_bio)]
rule initialize_voter2: // We initialise voter 2's role and biometric data.
let
// Voter 2 biometric data.
V2_bio = 'b2'
in
[ ]
--[Create_Voter2($V2), Honest($V2), Role('V2')]->
[State_V_1($V2, V2_bio), !Voter2_Attr(V2_bio)]
rule registrar_registers_voter_data: // Here, the registrar generates the parameters required for voter 1 and 2. Note that in this Tamarin model, we focus on just two honest voters.
let
total_voters = 'nv' // Total number of registered voters.
// Voter 1 parameters
V1_id = 'ID1' // Unique identifier for voter 1.
V1_ward = 'vp1' // Polling station assigned to voter 1.
V1_int = '1' // Secret integer for voter 1. The secret integer has been modelled as a constant because it does not change, once it has been assigned to a voter.
V1_enc_int = aenc{V1_int}pk(~RGR_priv_key) // Voter 1 encrypted secret integer. The secret integer is encrypted under the registrar's public key.
// Voter 2 parameters
V2_id = 'ID2' // Unique identifier for voter 2.
V2_ward = 'vp2' // Polling station assigned to voter 2.
V2_int = '2' // Secret integer for voter 2.
V2_enc_int = aenc{V2_int}pk(~RGR_priv_key) // Voter 2 encrypted secret integer.
in
[In($EA_name), Fr(~V1_priv_key), Fr(~V2_priv_key), !PClerk_Data(~pClerk_id), St_RGR_1($RGR, ~rgr_id, ~RGR_priv_key, pk(~RGR_priv_key), max_voters, sec_param),
!Voter1_Attr(V1_bio), !Voter2_Attr(V2_bio)]
--[Honest($RGR), Honest(~pClerk_id), Role('RGR')]->
[St_RGR_2($RGR, ~rgr_id, ~RGR_priv_key, pk(~RGR_priv_key), max_voters, total_voters, sec_param, V1_id, V1_int, V2_id, V2_int, $EA_name, ~pClerk_id),
!V1_Secret_Data(V1_id, V1_int, ~V1_priv_key, pk(~V1_priv_key), V1_ward), // The registrar will send these parameters to voter 1.
!V1_Reg_Data(V1_id, V1_bio, ~V1_priv_key, pk(~V1_priv_key), V1_ward), // The registrar will send these voter 1 parameters to the election authority.
!V2_Secret_Data(V2_id, V2_int, ~V2_priv_key, pk(~V2_priv_key), V2_ward), // The registrar will send these parameters to voter 2.
!V2_Reg_Data(V2_id, V2_bio, ~V2_priv_key, pk(~V2_priv_key), V2_ward), // The registrar will send these voter 2 parameters to the election authority.
!Main_Reg_Data(pk(~V1_priv_key), V1_ward, pk(~V2_priv_key), V2_ward, total_voters), // Placeholder for storing some of the data required in the electoral roll.
!Voter_Secret_Integers(sec_param, ~RGR_priv_key, pk(~RGR_priv_key), V1_enc_int, V2_enc_int),
Out(), Out()] // The encrypted secret integers and voter IDs for voter 1 and 2 are published (as a tuple) on the web bulletin board, respectively.
rule registrar_collates_electoral_roll: //The registrar prepares the electoral roll.
let
// Contents of the electoral roll.
elect_roll =
in
[St_RGR_2($RGR, ~rgr_id, ~RGR_priv_key, pk(~RGR_priv_key), max_voters, total_voters, sec_param, V1_id, V1_int, V2_id, V2_int, $EA_name, ~pClerk_id),
!Main_Reg_Data(pk(~V1_priv_key), V1_ward, pk(~V2_priv_key), V2_ward, total_voters)]
--[Send_Elect_Roll($RGR, <~pClerk_id, elect_roll>), Honest($RGR), Honest(~pClerk_id), Role('RGR')]->
[St_RGR_3($RGR, ~rgr_id, ~RGR_priv_key, pk(~RGR_priv_key), max_voters, total_voters, sec_param, V1_id, V1_int, V1_ward, pk(~V1_priv_key), V2_id, V2_int, V2_ward, pk(~V2_priv_key), $EA_name, ~pClerk_id),
!RGR_Send_Elect_Roll(elect_roll, max_voters, sec_param)]
rule pollworker_receives_electoral_roll: //The poll worker receives the electoral roll from the registrar and posts it publicly on the web bulletin board (and in the designated polling station).
let
elect_roll =
in
[!RGR_Data(~rgr_id), St_PClerk_1(PCK, ~pClerk_id), !RGR_Send_Elect_Roll(elect_roll, max_voters, sec_param)]
--[Receive_Elect_Roll(PCK, <~pClerk_id, elect_roll>), Honest(PCK), Role('PCK'), Honest(~rgr_id)]->
[St_PClerk_2(PCK, ~pClerk_id, elect_roll, max_voters, sec_param), Out(elect_roll)]
rule election_auth_receives_reg_data: //The election authority receives the voter registration data and sends the new voter credentials (i.e. ID cards) to the registrar.
let
V1_card = // Voter ID card for voter 1.
V2_card = // Voter ID card for voter 2.
in
[!RGR_Data(~rgr_id), St_ElecAuth_1($EA, $EA_name), !V1_Reg_Data(V1_id, V1_bio, ~V1_priv_key, pk(~V1_priv_key), V1_ward),
!V2_Reg_Data(V2_id, V2_bio, ~V2_priv_key, pk(~V2_priv_key), V2_ward)]
--[SendEA($EA, V1_card), SendEA($EA, V2_card), Honest($EA), Role('EA'), Honest(~rgr_id) ]-> //
[St_ElecAuth_2($EA, $EA_name, V1_id, V2_id, V1_ward, V2_ward), !V1Credential(V1_card), !V2Credential(V2_card)]
rule registrar_receives_voter_credentials: // The registrar receives the voter ID cards from the election authority.
let
V1_card = // Voter ID card for voter 1.
V2_card = // Voter ID card for voter 2.
in
[!V1Credential(V1_card), !V2Credential(V2_card),
St_RGR_3($RGR, ~rgr_id, ~RGR_priv_key, pk(~RGR_priv_key), max_voters, total_voters, sec_param, V1_id, V1_int, V1_ward, pk(~V1_priv_key), V2_id, V2_int, V2_ward, pk(~V2_priv_key), $EA_name, ~pClerk_id)]
--[ReceiveEA($RGR, V1_card), ReceiveEA($RGR, V2_card), Honest($RGR), Role('RGR'), Honest($EA_name), Honest(V1_id), Honest(V2_id)]->
[St_RGR_4($RGR, ~rgr_id, ~RGR_priv_key, pk(~RGR_priv_key), max_voters, total_voters, sec_param, V1_id, V1_int, V1_ward, pk(~V1_priv_key), V2_id, V2_int, V2_ward, pk(~V2_priv_key), $EA_name, ~pClerk_id),
!RGR_Send_V1Credential(V1_card), !RGR_Send_V2Credential(V2_card)]
rule voter1_receives_credentials: // Voter 1 receives their ID card and secret integer from the registrar.
[State_V_1($V1, V1_bio), !V1_Secret_Data(V1_id, V1_int, ~V1_priv_key, pk(~V1_priv_key), V1_ward), !RGR_Send_V1Credential(V1_card)]
--[Honest($V1), Role('V1')]->
[State_V_2($V1, V1_bio, V1_id, V1_int, ~V1_priv_key, pk(~V1_priv_key), V1_ward, V1_card)]
rule voter2_receives_credentials: // Voter 2 receives their ID card and secret integer from the registrar.
[State_V_1($V2, V2_bio), !V2_Secret_Data(V2_id, V2_int, ~V2_priv_key, pk(~V2_priv_key), V2_ward), !RGR_Send_V2Credential(V2_card)]
--[Honest($V2), Role('V2')]->
[State_V_2($V2, V2_bio, V2_id, V2_int, ~V2_priv_key, pk(~V2_priv_key), V2_ward, V2_card)]
rule voter1_attendance_status: // Voter 1 attends the election.
let
At_1 = diff('Y', 'N') // 'Y' indicates attendance, 'N' indicates absence.
in
[State_V_2($V1, V1_bio, V1_id, V1_int, ~V1_priv_key, pk(~V1_priv_key), V1_ward, V1_card)]
--[Honest($V1)]->
[State_V_3($V1, V1_bio, V1_id, V1_int, ~V1_priv_key, pk(~V1_priv_key), V1_ward, V1_card, At_1), !V1_Attendance_Record(At_1)]
rule voter2_attendance_status: // Voter 2 attends the election.
let
At_2 = diff('N', 'Y') // 'N' indicates absence, 'Y' indicates attendance.
in
[State_V_2($V2, V2_bio, V2_id, V2_int, ~V2_priv_key, pk(~V2_priv_key), V2_ward, V2_card)]
--[Honest($V2)]->
[State_V_3($V2, V2_bio, V2_id, V2_int, ~V2_priv_key, pk(~V2_priv_key), V2_ward, V2_card, At_2), !V2_Attendance_Record(At_2)]
rule pollworker_collates_attendance_list: // The poll worker records the attendance status for each voter. This data will be publicly accessible on the web bulletin board afterwards.
let
At_1 = diff('Y', 'N') // Attendance status for voter 1; 'Y' indicates attendance, 'N' indicates absence.
At_2 = diff('N', 'Y') // Attendance status for voter 2; 'N' indicates absence, 'Y' indicates attendance.
in
[In(V1_id), In(V2_id), !RGR_Data(~rgr_id), St_PClerk_2(PCK, ~pClerk_id, elect_roll, max_voters, sec_param), !V1_Attendance_Record(At_1), !V2_Attendance_Record(At_2)]
--[SendList(PCK, <, >), Honest(PCK), Role('PCK'), Honest(~rgr_id) ]->
[St_PClerk_3(PCK, ~pClerk_id, elect_roll, max_voters, sec_param, , ), !AttendanceList(, )]
rule registrar_computes_plaintext_int: // Registrar receives the attendance list from the poll worker, and then computes the plaintext integer for each voter.
let
V1_ptxt_int = adec(V1_enc_int, ~RGR_priv_key) // If the voter attended, plaintext integer = voter's secret integer.
V2_ptxt_int = adec(V2_enc_int, ~RGR_priv_key) // If the voter abstained from the election, plaintext integer = negation(voter's secret integer).
At_1 = diff('Y', 'N') // Attendance record for voter 1; 'Y' indicates attendance, 'N' indicates absence.
At_2 = diff('N', 'Y') // Attendance record for voter 2; 'N' indicates absence, 'Y' indicates attendance.
in
[!PClerk_Data(~pClerk_id), !Voter_Secret_Integers(sec_param, ~RGR_priv_key, pk(~RGR_priv_key), V1_enc_int, V2_enc_int), !AttendanceList(, )]
--[ReceiveList($RGR, <, >), Honest($RGR), Role('RGR'), Honest(~pClerk_id)]->
[!Publish_Interim_Attendance_Data(, )]
rule registrar_computes_attendance_cprtxt: //The registrar computes the attendance ciphertext for each voter.
let
V1_ptxt_int = adec(V1_enc_int, ~RGR_priv_key) // If voter attended, plaintext integer = voter's secret integer.
V2_ptxt_int = adec(V2_enc_int, ~RGR_priv_key) // If voter abstained from the election, plaintext integer = negation(voter's secret integer).
V1_Atd_cprtxt = // Attendance ciphertext for voter 1.
V2_Atd_cprtxt = // Attendance ciphertext for voter 2.
At_1 = diff('Y', 'N') // Attendance status for voter 1; 'Y' indicates attendance, 'N' indicates absence.
At_2 = diff('N', 'Y') // Attendance status for voter 2; 'N' indicates absence, 'Y' indicates attendance.
in
[!Publish_Interim_Attendance_Data(, ), !Voter_Secret_Integers(sec_param, ~RGR_priv_key, pk(~RGR_priv_key), V1_enc_int, V2_enc_int)]
--[OnlyOnce(), Honest($RGR), Role('RGR')]->
[!Publish_Complete_Attendance_Data(, ), Out( + )]
// NB: We have used Tamarin's associativity-commutativity operator (see [1,2,3,4]) denoted by '+' to model the shuffling of the attendance ciphertexts and plaintext integers that are posted on the web bulletin board by the registrar.
rule voter_verifies_wbb_attendance_record: // Here, the voter verifies that the attendance data that is published for them on the web bulletin board is accurate.
let
Vi_ptxt_int = adec(Vi_enc_int, ~RGR_priv_key) // If voter attended, plaintext integer = voter's secret integer.
in
[State_V_3($Vi, Vi_bio, Vi_id, Vi_int, ~Vi_priv_key, pk(~Vi_priv_key), Vi_ward, Vi_card, At_i), !Voter_Secret_Integers(sec_param, ~RGR_priv_key, pk(~RGR_priv_key), Vi_enc_int, y)] // Note that 'y' is a placeholder.
--[Verify() ]->
//[]
[Out(Vi_int), Out(Vi_ptxt_int)]
// END OF CODE
//RESTRICTIONS
restriction OnlyOnce: // This restriction ensures that the public-private key pairs (and rules, where applicable) are generated/executed only once, as required.
"All #i #j. OnlyOnce()@#i & OnlyOnce()@#j ==> #i = #j"
//SECURITY PROPERTIES
lemma verifiability: // This lemma verifies that the Tamarin file is executed as expected.
exists-trace
"Ex #i #j. Verify()@i & Verify()@j & not( #i=#j)" // The logic of this lemma was inspired by the formal verification of vote privacy (with the Tamarin prover), as described in [2,3,4].
end
/*References
1) The Tamarin Team. 2019. Tamarin-Prover manual: security protocol analysis in the symbolic model. 1–117. [Last accessed: 12 July 2020].
2) A. Bruni, E. Drewsen, and C. Schürmann. 2017. Towards a mechanized proof of Selene receipt-freeness and vote-privacy.
In Proceedings of the 2nd International Joint Conference on Electronic Voting (E-Vote-ID ’17), Bregenz, Austria, 24–27 October 2017. 110–126.
3) E. Drewsen. 2017. Formal analysis of the Selene voting protocol. Master’s thesis. IT University of Copenhagen.
4) J. Dreier, C. Duménil, S. Kremer, and R. Sasse. 2017. Beyond subterm-convergent equational theories in automated verification of stateful protocols.
In Proceedings of the 6th International Conference on Principles of Security and Trust (POST ’17), Uppsala, Sweden, 22–29 April 2017. 117–140.
*/
/*=========================================================================================================================
Table of summaries:
LHS : Verify (exists-trace): verified (21 steps) (Not the LHS/RHS raw sources; the number above without 'cases').
RHS : Verify (exists-trace): verified (21 steps).
DiffLemma: Observational_equivalence : verified.
Performance parameters:
1) Autoprove A loads the Tamarin model in approx. 0min 6secs (for both LHS and RHS).
2) Autoprove B loads the Tamarin model in approx. 0min 45secs (for both LHS and RHS).
3) Observational Equivalence using backward-search with Autoprove A loads in approx. 21mins (for LHS and RHS).
4) The Tamarin model took approx. 27mins to load (after the .spthy file was first opened in the Tamarin GUI).
NB: It is worth mentioning that these performance parameters will vary depending on the computer hardware specifications.
===========================================================================================================================*/