theory voter_authentication_protocol
begin
builtins: hashing, xor, asymmetric-encryption, diffie-hellman, multiset
functions: pk/1, open/3, commit/3, fake/4, aenc/2, adec/2, XOR/2, h1/1, h2/1
equations: open(commit(m1, r, pk(sk)), r, sk) = m1, // Adapted from the works of [1,2,3,4,5].
adec(aenc(m2, pk(sk)), sk) = m2 // Adapted from the examples given in the Tamarin manual [7].
/*===============================================================================NOTES===================================================================================
This Tamarin .spthy file formally proves participation privacy in the proposed voter authentication protocol.
The results obtained from this work have been described in CHAPTER 5 of the PhD Thesis titled "Secure Voter Authentication for Poll-site Elections in Developing Countries".
The primary web bulletin board (WBB 1) will contain the voter's unique identifier, the voter's public key, the attendance bit of the voter, the voter's assigned polling station,
as well as the encrypted confirmation code. We do not model the inclusion of the message publication time and the 1-bit voter card status on the primary WBB.
The confirmation code committed by the poll worker will first be encrypted with the voter's public key BEFORE being encrypted with the election public key and token.
The fuzzy verifier for voter v_{i} is defined as follows: A_{i} = H(H(ID_{i}) ⊕ H(PW_{i}||w)); where ⊕ denotes exclusive-or (XOR) in Tamarin.
Note that commit(m,r,pk) has been used to model the commitment to a plaintext m, with the public key pk = pk(sk) and random value r [1].
In this protocol, any agent labelled with '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) [7].
Finally, note that we do not model the inner workings of the fuzzy extractor. According to Dodis et al. [6], fuzzy extractors have information-theoretic security.
In the trust model for this scheme, we assume that the registrar is honest and will keep the election token and private key confidential.
We consider a Dolev-Yao adversary in this protocol.
This Tamarin model was revised and finalised on 12 July 2020.
Modeller: Olukayode Nicholas Akinyokun
Student ID: 807141
==========================================================================================================================================================================*/
rule voter1_generate_longterm_keys: // Voter 1 generates their longterm keys.
[Fr(~V1_priv_key) ] -->
[ !V1SecretKey($V1, ~V1_priv_key), !V1PublicKey($V1, pk(~V1_priv_key))]
rule voter2_generate_longterm_keys: // Voter 2 generates their longterm keys.
[Fr(~V2_priv_key) ] -->
[ !V2SecretKey($V2, ~V2_priv_key), !V2PublicKey($V2, pk(~V2_priv_key))]
// The registrar's key generation process begins here.
rule registrar_generate_longterm_keys: // The registrar generates their longterm keys.
[Fr(~RGR_priv_key) ] --[ OnlyOnce() ]-> // RGR is our abbreviation for the registrar.
[ !RGRSecretKey($RGR, ~RGR_priv_key), !RGRPublicKey($RGR, pk(~RGR_priv_key))]
rule initialize_registrar: // The registrar's ID and role is initialised.
[Fr(~rgr_id), !RGRSecretKey($RGR, ~RGR_priv_key), !RGRPublicKey($RGR, pk(~RGR_priv_key))]
--[Create($RGR, ~rgr_id), Role('RGR') ]->
[St_RGR_1($RGR, ~rgr_id, ~RGR_priv_key, pk(~RGR_priv_key)), !RGRID(~rgr_id)]
// Registrar's key generation process ends here.
rule initialize_pollworker: // The poll worker's ID and role is initialised.
let
PCK = 'Clerk' // PCK is our abbreviation for the poll worker.
in
[Fr(~pClerk_id)]
--[Create(PCK, ~pClerk_id), Honest(PCK), Role('PCK')]->
[St_PClerk_1(PCK, ~pClerk_id), Out(~pClerk_id), !PClerk_Data(PCK, ~pClerk_id)]
rule define_voter1_secret_data:
let
// Voter 1 parameters
V1_id = 'ID1' // Unique identifier.
V1_bio = 'b1' // Derived biometric.
V1_pword = 'PW1' // Password.
V1_quest = 'Wq1' // Voter's security question.
V1_ans = 'w1' // Answer to security question.
a1 = h(V1_id)
V1_hpword = h(< V1_pword, V1_ans >) // Hashed password.
V1_fuzzy = h(< a1 XOR V1_hpword>) // Fuzzy verifier.
in
[!V1SecretKey($V1, ~V1_priv_key), !V1PublicKey($V1, pk(~V1_priv_key))]
--[Create($V1, pk(~V1_priv_key)), Role('V1')]->
[State_V_1($V1, diff('Y', 'N'), ~V1_priv_key, pk(~V1_priv_key), V1_id, V1_bio, V1_pword, V1_quest, V1_ans, V1_hpword, V1_fuzzy), Out(V1_id)] // Initial state fact for voter 1.
// Y implies that voter authentication was successful AND the voter is registered as having attended their assigned polling station on the primary WBB.
// N implies that voter authentication was unsuccessful AND the voter is registered as absent from their polling station on the primary WBB.
// Recall that in the protocol specification, the attendance bit is 1 (i.e. Y) if the voter's authentication was successful and 0 (i.e. N) otherwise.
rule define_voter2_secret_data:
let
// Voter 2 parameters
V2_id = 'ID2' // Unique identifier.
V2_bio = 'b2' // Derived biometric.
V2_pword = 'PW2' // Password.
V2_quest = 'Wq2' // Voter's security question.
V2_ans = 'w2' // Answer to security question.
x2 = h(V2_id)
V2_hpword = h(< V2_pword, V2_ans >) // Hashed password.
V2_fuzzy = h(< x2 XOR V2_hpword>) // Fuzzy verifier.
in
[!V2SecretKey($V2, ~V2_priv_key), !V2PublicKey($V2, pk(~V2_priv_key))]
--[Create($V2, pk(~V2_priv_key)), Role('V2')]->
[State_V_1($V2, diff('N', 'Y'), ~V2_priv_key, pk(~V2_priv_key), V2_id, V2_bio, V2_pword, V2_quest, V2_ans, V2_hpword, V2_fuzzy), Out(V2_id)] // Initial state fact for voter 2.
rule voter1_sends_reg_data: // ~vp1 denotes the polling station assigned to voter 1.
[Fr(~vp1), !RGRID(~rgr_id), State_V_1($V1, diff('Y', 'N'), ~V1_priv_key, pk(~V1_priv_key), V1_id, V1_bio, V1_pword, V1_quest, V1_ans, V1_hpword, V1_fuzzy)]
--[Send(), Honest($V1), Honest(~rgr_id), Role('V1')]->
[State_V_2($V1, diff('Y', 'N'), ~V1_priv_key, pk(~V1_priv_key), V1_id, V1_bio, V1_pword, V1_quest, V1_ans, V1_hpword, V1_fuzzy, ~vp1, ~rgr_id), !V1SendRegData(V1_hpword, pk(~V1_priv_key), V1_quest, ~vp1, V1_bio)]
rule voter2_sends_reg_data: // ~vp2 denotes the polling station assigned to voter 2.
[Fr(~vp2), !RGRID(~rgr_id), State_V_1($V2, diff('N', 'Y'), ~V2_priv_key, pk(~V2_priv_key), V2_id, V2_bio, V2_pword, V2_quest, V2_ans, V2_hpword, V2_fuzzy)]
--[Send(), Honest($V2), Honest(~rgr_id), Role('V2')]->
[State_V_2($V2, diff('N', 'Y'), ~V2_priv_key, pk(~V2_priv_key), V2_id, V2_bio, V2_pword, V2_quest, V2_ans, V2_hpword, V2_fuzzy, ~vp2, ~rgr_id), !V2SendRegData(V2_hpword, pk(~V2_priv_key), V2_quest, ~vp2, V2_bio)]
rule registrar_collates_voter_data: // The registrar collates the registration details of voter 1 and voter 2.
[In(V1_id), In(V2_id), !PClerk_Data(PCK, ~pClerk_id), !V1SendRegData(V1_hpword, pk(~V1_priv_key), V1_quest, ~vp1, V1_bio), !V2SendRegData(V2_hpword, pk(~V2_priv_key), V2_quest, ~vp2, V2_bio),
St_RGR_1($RGR, ~rgr_id, ~RGR_priv_key, pk(~RGR_priv_key))]
--[Receive(), Receive(), Honest($RGR), Role('RGR'), Honest(~pClerk_id) ]->
[St_RGR_2($RGR, ~rgr_id, ~RGR_priv_key, pk(~RGR_priv_key), ~pClerk_id, V1_id, V1_hpword, pk(~V1_priv_key), V1_quest, ~vp1, V1_bio, V2_id, V2_hpword, pk(~V2_priv_key), V2_quest, ~vp2, V2_bio),
Out(<~vp1, pk(~V1_priv_key)>), Out(<~vp2, pk(~V2_priv_key)>), !Voters_Reg_Data(V1_id, V1_hpword, pk(~V1_priv_key), V1_quest, ~vp1, V1_bio, V2_id, V2_hpword, pk(~V2_priv_key), V2_quest, ~vp2, V2_bio)]
rule registrar_sends_voter_credentials: // The registrar sends each voter their nonce and voter card, respectively.
let
V1_card = 'SC_v1' // Voter card for voter 1.
V2_card = 'SC_v2' // Voter card for voter 2.
in
[Fr(~V1_nonce), Fr(~V2_nonce), St_RGR_2($RGR, ~rgr_id, ~RGR_priv_key, pk(~RGR_priv_key), ~pClerk_id, V1_id, V1_hpword, pk(~V1_priv_key), V1_quest, ~vp1, V1_bio, V2_id, V2_hpword, pk(~V2_priv_key), V2_quest, ~vp2, V2_bio)]
//Note that ~V1_nonce = voter 1's secret nonce; ~V2_nonce = voter 2's secret nonce.
--[Send(<~V1_nonce, V1_card>), Send(<~V2_nonce, V2_card>), Honest($RGR), Role('RGR'), Honest(V1_id), Honest(V2_id), Honest(~pClerk_id) ]->
[St_RGR_3($RGR, ~rgr_id, ~RGR_priv_key, pk(~RGR_priv_key), V1_id, V1_hpword, pk(~V1_priv_key), V1_quest, ~vp1, V1_bio, V2_id, V2_hpword, pk(~V2_priv_key), V2_quest, ~vp2, V2_bio, ~V1_nonce, ~V2_nonce),
!RGR_Send_V1Credentials(<~V1_nonce, V1_card>), !RGR_Send_V2Credentials(<~V2_nonce, V2_card>), RGRSendNonces(<~V1_nonce, ~V2_nonce>)]
rule registrar_generate_election_keys:
[Fr(~tok), Fr(~election_priv_key), RGRSendNonces(<~V1_nonce, ~V2_nonce>), // ~tok = Election token.
St_RGR_3($RGR, ~rgr_id, ~RGR_priv_key, pk(~RGR_priv_key), V1_id, V1_hpword, pk(~V1_priv_key), V1_quest, ~vp1, V1_bio, V2_id, V2_hpword, pk(~V2_priv_key), V2_quest, ~vp2, V2_bio, ~V1_nonce, ~V2_nonce)]
--[Setup(), Honest($RGR)]->
[ConfCodeData(pk(~election_priv_key), ~tok), ElectionSecretKey(~election_priv_key, ~tok),
St_RGR_4($RGR, ~rgr_id, ~RGR_priv_key, pk(~RGR_priv_key), V1_id, V1_hpword, pk(~V1_priv_key), V1_quest, ~vp1, V1_bio, V2_id, V2_hpword, pk(~V2_priv_key), V2_quest, ~vp2, V2_bio, ~V1_nonce, ~V2_nonce, pk(~election_priv_key)),
!ElectoralRoll(V1_id, ~vp1, pk(~V1_priv_key), V2_id, ~vp2, pk(~V2_priv_key)), Out(pk(~election_priv_key))]
rule pollworker_receives_election_data: // Here, the poll worker receives the election data from the registrar, as well as the electoral roll.
[!RGRID(~rgr_id), In(V1_id), In(V2_id), ConfCodeData(pk(~election_priv_key), ~tok), St_PClerk_1(PCK, ~pClerk_id),
!ElectoralRoll(V1_id, ~vp1, pk(~V1_priv_key), V2_id, ~vp2, pk(~V2_priv_key)), RGRSendNonces(<~V1_nonce, ~V2_nonce>)]
--[Receive(<~V1_nonce, ~V2_nonce>), Honest(PCK), Honest(~rgr_id), Role('PCK') ]->
[St_PClerk_2(PCK, ~pClerk_id, ~rgr_id, ~V1_nonce, ~V2_nonce, pk(~V1_priv_key), pk(~V2_priv_key), V1_id, V2_id, pk(~election_priv_key), ~tok)]
rule voter1_receives_credential: // Voter 1 receives their voting credentials (i.e. the voter card and secret nonce).
let
V1_card = 'SC_v1' // Voter card for voter 1.
in
[!RGR_Send_V1Credentials(<~V1_nonce, V1_card>),
State_V_2($V1, diff('Y', 'N'), ~V1_priv_key, pk(~V1_priv_key), V1_id, V1_bio, V1_pword, V1_quest, V1_ans, V1_hpword, V1_fuzzy, ~vp1, ~rgr_id)]
--[Receive(<~V1_nonce, V1_card>), Honest($V1), Honest(~rgr_id), Role('V1')]->
[State_V_3($V1, diff('Y', 'N'), ~V1_priv_key, pk(~V1_priv_key), V1_id, V1_bio, V1_pword, V1_quest, V1_ans, V1_hpword, V1_fuzzy, ~vp1, ~rgr_id, ~V1_nonce, V1_card)]
rule voter2_receives_credential: // Voter 2 receives their voting credentials.
let
V2_card = 'SC_v2' // Voter card for voter 2.
in
[!RGR_Send_V2Credentials(<~V2_nonce, V2_card>),
State_V_2($V2, diff('N', 'Y'), ~V2_priv_key, pk(~V2_priv_key), V2_id, V2_bio, V2_pword, V2_quest, V2_ans, V2_hpword, V2_fuzzy, ~vp2, ~rgr_id)]
--[Receive(<~V2_nonce, V2_card>), Honest($V2), Honest(~rgr_id), Role('V2')]->
[State_V_3($V2, diff('N', 'Y'), ~V2_priv_key, pk(~V2_priv_key), V2_id, V2_bio, V2_pword, V2_quest, V2_ans, V2_hpword, V2_fuzzy, ~vp2, ~rgr_id, ~V2_nonce, V2_card)]
rule voter_attends_election: // Here, the voter's attends the election.
let
At_i = diff('Y', 'N') // This represents the voter attendance record/data, where 'Y' implies that the voter attended (and voted in) the election.
in
[State_V_3($Vi, At_i, ~Vi_priv_key, pk(~Vi_priv_key), Vi_id, Vi_bio, Vi_pword, Vi_quest, Vi_ans, Vi_hpword, Vi_fuzzy, ~vpi, ~rgr_id, ~Vi_nonce, Vi_card)]
--[Honest($Vi)]->
[RecordAttendance(),
State_V_4($Vi, At_i, ~Vi_priv_key, pk(~Vi_priv_key), Vi_id, Vi_bio, Vi_pword, Vi_quest, Vi_ans, Vi_hpword, Vi_fuzzy, ~vpi, ~rgr_id, ~Vi_nonce, Vi_card)]
rule pollworker_compute_confirm_code: // Here, the poll worker computes the confirmation code for each voter.
let
V1_timestamp = 'time1' // Voter 1 attendance timestamp.
V2_timestamp = 'time2' // Voter 2 attendance timestamp.
V1_code = <~V1_nonce, V1_timestamp> // Plaintext of voter 1 confirmation code. The content of this confirmation code include the nonce issued to the voter, as well as the time the voter's eligibility was verified.
V2_code = <~V2_nonce, V2_timestamp> // Plaintext of voter 2 confirmation code.
eV1_code = aenc(V1_code, pk(~V1_priv_key)) // Encryption of V1_code with voter 1's public key. This code could also be written as: // eV1_code = aenc{V1_code}pk(~V1_priv_key). See [7].
eV2_code = aenc(V2_code, pk(~V2_priv_key)) // Encryption of V2_code with voter 2's public key.
in
[St_PClerk_2(PCK, ~pClerk_id, ~rgr_id, ~V1_nonce, ~V2_nonce, pk(~V1_priv_key), pk(~V2_priv_key), V1_id, V2_id, pk(~election_priv_key), ~tok)]
--[Honest(PCK)]->
[!Shuffle_codes_0_V1(), !Shuffle_codes_0_V2(), !ComputeConfCode(eV1_code + eV2_code),
St_PClerk_3(PCK, ~pClerk_id, ~rgr_id, ~V1_nonce, ~V2_nonce, pk(~V1_priv_key), pk(~V2_priv_key), V1_id, V2_id, pk(~election_priv_key), ~tok, eV1_code, eV2_code)]
rule pollworker_reencrypt_conf_code_post_attendance:
// Here, the poll worker re-encrypts (and commits to) the previous ciphertext of each voter's confirmation code with the election public key and token, respectively.
let
// The token-controlled public-key encryption code snippet.
ecV1_code = commit(eV1_code, ~tok, pk(~election_priv_key)) // Encrypted confirmation code of voter 1.
ecV2_code = commit(eV2_code, ~tok, pk(~election_priv_key)) // Encrypted confirmation code of voter 2.
ecVi_code = commit(eVi_code, ~tok, pk(~election_priv_key))
in
[!Shuffle_codes_0_V1(), !Shuffle_codes_0_V2(), !ComputeConfCode(eVi_code + p), // where p is a placeholder.
St_PClerk_3(PCK, ~pClerk_id, ~rgr_id, ~V1_nonce, ~V2_nonce, pk(~V1_priv_key), pk(~V2_priv_key), V1_id, V2_id, pk(~election_priv_key), ~tok, eV1_code, eV2_code),
RecordAttendance()]
--[Honest(PCK), Secret(ecV1_code,ecV2_code)]->
[ Out( + ), // The poll worker shuffles and publishes the encrypted confirmation code for each voter on the primary WBB.
!PublishCommitment( + ),
St_PClerk_4(PCK, ~pClerk_id, ~rgr_id, ~V1_nonce, ~V2_nonce, pk(~V1_priv_key), pk(~V2_priv_key), V1_id, V2_id, pk(~election_priv_key), ~tok, eV1_code, eV2_code, ecV1_code, ecV2_code),
!PostAttendanceBit(), Out()]
rule voter_checks_confirm_code:
let
eVi_code = open(ecVi_code, ~tok, ~election_priv_key) // This code opens the encrypted confirmation code.
in
[ElectionSecretKey(~election_priv_key, ~tok), !PublishCommitment( + y), !ComputeConfCode(eVi_code + p), // where y, p are placeholders.
State_V_4($Vi, At_i, ~Vi_priv_key, pk(~Vi_priv_key), Vi_id, Vi_bio, Vi_pword, Vi_quest, Vi_ans, Vi_hpword, Vi_fuzzy, ~vpi, ~rgr_id, ~Vi_nonce, Vi_card)]
--[Verify() ]-> //--[ Verify(eVi_code) ]->
[ ]
//RESTRICTIONS
restriction RuleSetup: // This restriction ensures that the applicable rules are executed only once.
"All #i #j. Setup() @#i & Setup() @#j ==> #i = #j "
restriction OnlyOnce: // This restriction ensures that the public-private key pairs are generated 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.
all-traces
"All #i #j. Verify()@i & Verify()@j ==> #i = #j"
end
// END OF CODE
/*References
1) 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.
2) E. Drewsen. 2017. Formal analysis of the Selene voting protocol. Master’s thesis. IT University of Copenhagen.
3) R. Chadha, V. Cheval, Ş. Ciobâcă, and S. Kremer. 2016. Automated verification of equivalence properties of cryptographic protocols.
ACM Transactions on Computational Logic 17, 4 (2016), 1–32.
4) Ş. Ciobâcă, S. Delaune, and S. Kremer. 2012. Computing knowledge in security protocols under convergent equational theories.
Journal of Automated Reasoning 48, February 2012 (2012), 219–262.
5) 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.
6) Y. Dodis, R. Ostrovsky, L. Reyzin, and A. Smith. 2008. Fuzzy extractors: how to generate strong keys from biometrics and other noisy data.
SIAM Journal on Computing 38, 1 (2008), 97–139.
7) The Tamarin Team. 2019. Tamarin-Prover manual: security protocol analysis in the symbolic model. 1–117. [Last accessed: 30 June 2020].
8) D. Wong. 2017. Tamarin prover introduction. Available online: https://www.youtube.com/watch?v=XptJG19hDcQ. [Last accessed: 30 June 2020].
*/
/*Acknowledgements
The logic we have applied in this formal verification has been inspired by the tutorial of David Wong [8], and the work described in [1,2]. The author wishes to
thank Eva Drewsen for sharing the PDF copy of her MSc thesis via email.
*/
/*========================================================================================================================
Table of summaries:
LHS : Verify (all-traces): verified (21 steps) (Not the LHS/RHS raw sources; the number above without 'cases').
RHS : Verify (all-traces): verified (21 steps).
DiffLemma: Observational_equivalence : verified.
Performance parameters:
1) Autoprove A loads the Tamarin model in approx. 0mins 8secs (for both LHS and RHS).
2) Autoprove B loads the Tamarin model in approx. 0mins 7secs (for both LHS and RHS).
3) Observational Equivalence using backward-search with Autoprove A loads in 5secs (for LHS and RHS).
4) The Tamarin model took approx. 4mins 15secs 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.
===========================================================================================================================*/