coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>
- To: Stefan Monnier <monnier AT iro.umontreal.ca>, coq-club AT inria.fr
- Subject: Re: [Coq-Club] Electronic Voting Machines in French Elections
- Date: Sun, 1 May 2022 14:38:43 +0100
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mukeshtiwari.iiitm AT gmail.com; spf=Pass smtp.mailfrom=mukeshtiwari.iiitm AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f43.google.com
- Ironport-data: A9a23:EXL4iKpcTu86svUcWpzTWVSaZ1FeBmImYxIvgKrLsJaIsI4StFCzt garIBmFOKyOa2XzL4okaoS2/EwGu8LRzYI1QFBqqn9jFikUpOPIVI+TRqvSF3PLf5ebFCqLz O1HN4KedJhsJpP4jk3wWlQ0hSAkjclkfpKlVKicfHoZqTZMEE/Nszo68wICqtMu0IHR7z+l4 4uo+ZWCYAb9glaYD0pNg069gEM31BjNkGhA1rAOTagjUIj2yhH5pLpGTU2AByOQrrt8RoZWd M6fpF2NxV41yj92Yj+TfhkXRWVRKlLaFVDmZnO7wMFOiDAazsA5+v5T2Pbx9S67hh3R9+2dx umhurSoW18UYarwiNgnUj5jCB9nGbwf0q/IdC3XXcy7lyUqclPpyvRqSUw6ZMgWpr0xDmZJ+ vgVbjsKa3hvhcrsmOP9GrQq3JxzapWwVG8ckikIITXxCOslTIvDX6TV7MVZmjYxh9xLNfnbb ssdLzFoaXwsZjUUZg5MVsNuxY9EgFH/Xi9ahWmF5pMn7lbx6SVQ+5bjMuTaL4niqcJ9xx7E/ Aoq5V/RCRYDcdeb1DCt6WOpnuaJnCXhWYtUGqfQyxJxqFiax2hWBRFPEFXn+r+2jUmxX98ZI EsRksYzkUQs3FS5FuSiWCGonESFmSUHZcN0ArQQ+A7Yn8I4/D2lLmQDSzdAbvkvu8k3WSEm2 ze1czXBVWwHXFq9GSL1y1uEkd+hEXNKcjJaNEfoWSNAsoaz+thi5v7aZo87SPbdszHjJd3nL 9m3QMUWgrwSiYsG2/z+8wycxT2roZfNQ0g+4QC/soOZAuFRNN/Ni2+AswCzARN8wGCxEALpU J8sxZT20Qz2JcvR/BFhuc1UdF1T296LMSfHnXlkFIQ7+jKm9haLJN4NuWgmfRY2bZxeJlcFh XM/XysBtPe/21P6PcdKj36ZVqzGMIC7RY+7B6yKBjawSsEpL1XZpkmCmnJ8L0i0yBR2+U3OE ZicdsmoAB4n5VdPnVKLqxMm+eZznEgWnDuNLbiilkjP+efAORa9FOhdWHPTP7hRxP7V+239r ocPX+PUkUk3eLOlOUH/r9VDRW3m2FBhWvgaXeQMJrDdSuencUl9Y8LsLUQJJtI1wvwJxruZl px/M2cBoGfCabT8AV3iQhhehHnHBP6TdFo3Yn4hO0iGwX8mbdr95asTbcplcrwu9eglxvlxF qFXd8KFC/VJazLG5zVNNcmn/NI+LEym1VCUIi6oQDkjZJo/FQHE/9nTeAGwpiQDCyyAs9Qz/ u+73QTBTJtfHAlvVZ6EaP+mw16rk2IaneZ+AxnBLtVJKRfj9YFrL2r6ifpue5MALhDKxz270 QeKAEdA9bOd/dNtqNSQ3PKKtYakFed6D3F2JWiD4ObkLzTe80qi3ZRED7SFcDXbY2X+p/eva OBT+PfjaaFVkVtPtb18JLZl16cJ4dXi+u1BxQN+EXSXNlmmB+8yInSC2sUT5KRByqUD4lmzU 0OLv9RWYPCHZJijH1kWKw4oKO+E0KhMyDXV6P00JmT85TN2rOXbCxQMZ0HUhXwPNqZxPaMk3 fwl5Jwc5Tu5h0d4Kd2BlC1VqzmBIyBSSakhrZ1GUobnhhBxkQNHaJ3YTyL6udSBN44KPU4tL TuZwqHFgu0ElEbFdnMyE1nL3PZc1ctS4kEUlAdaKgTbgMfBi982wAZVrWY9QDNTw0gVyOl0I GVqaxB4KKjmE+2EXySfs71A2j2tBSF1PmT0wloN0WDVFgymCjeLI2o6NuKAukse9gqwu9SdE K6wkA7YvfTCJakdHRfenWZqrvXiSZp68QiqdAWPAZGeB5djCdb6qvbGWIfLwicLxes+gUTGo a9h++MYhWgX88IPi/VTNrR2Hoj8hPxJyKKujB2hEG408bngRQyP
- Ironport-hdrordr: A9a23:NdiG/K1yQWwC7zWokRo0cAqjBIskLtp133Aq2lEZdPU1SL3gqy nKpp4mPHDP+VMssR0b6LK90ey7MBDhHP1OgLX5X43SODUO0VHAROpfBMnZowEIcBeOkdK1u5 0QFZSWy+edMbG5t6vHCcWDfOrICePozJyV
- Ironport-phdr: A9a23:NFygnRbUgNdBcw3damJ607f/LTHa2YqcDmcuAnoPtbtCf+yZ8oj4O wSHvLMx1gSPB96Qta4My7KP9fy6AypYudfJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnF t9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+M hu7oR/PusQYjodvK6k8wQbNrndUZuha32xlKUyNkxrm+su84Jtv+DlMtvw88MJNTb/0dLkiQ 7xCCzQmPWE15Mn1uhTGUACC+HgSXHgInxRRGwTK4w30UZn3sivhq+pywzKaMtHsTbA1Qjut8 aFmQwL1hSgdNj459GbXitFsjK9evRmsqQBzz5LSbYqIL/d1YL/Tcs0GSmpARsZRVjJOAoWgb 4sUEuENOf9Uo5Thq1cSqBezAxSnCuHyxT9SnnL50qM63OYhHw/I3wIuAswAv2jPodXpKKsfS /y5wLXUwTjBaf5dxDfz6JLPchAkufyMWK9wccnPxkk0FwPOk0mQqY3rPjyPzOQNsnWQ4u1lV eKyiG4otRpxojizxscthIjGnJgVylHe+SV4wYY1JMG4SEtgbN6rFZtfrSCaN49sTsw+RGFov T83x7sbspG0YCYE0o4oxwLDa/OZaYiI5AruWuafLDl4hn9oebKxigq9/EW8xOPwStS53VhXo yRLjtXBt3QA2h7O5sWERfVw/UWs1DWT2w3N5O9JIk46mbTHJpMn37U+mJ0TsUHZES/3nkX7l KGXdkQn+uip8+TofKjppp6GOINujQH+KKsultSlDuskLggCRWeb+eOi1LH550L5Xa1Ggecon abFqpzaKsMbprCjDwBPz4Yv8xiyAyq73NQZm3kHN05FeBObj4j0J1HBPur0Auu4g1Spljpg2 vPIPqX5D5nTMnTOlK3tcLV95kJG1gY/0dNS64hbB7wPJv/4R1X/u8bCDhAjNgy52+bnB8t51 oMZQW+PB7WWMKLWsVOR+O0gPvSAaJYbuDvyJfUp/fHujXg+mV8Seammw4EbZ2y/HvRjO0mZY HzsjckdEWoSoAYyUOjnhEeBXDNTfXq+Qb4w6zIhBI+pA4rPXoWtj6aA3Ce/EJ1WfGdGClWUH HftaoWEWOkDaDmSIs99kzwFW6KuS5Ug1R20tQ/6yrtnLvbR+iADupLj0cJ65+zXlR0o6TN0C MGd33mLT25vhmwIXSM53LhjoUxhzVeOybV0j+RCFdNP//NJThs6NZnEwuNmDNDyQxvNccuNS Fa7WdqrGioxT9I0w98WeUlxAdSijhbZ3yqrGbAZjbKLBIZnup7bikPtKsh0zT7j068njlQ8C p9KMmugh6Nl3wnJAMjUlkKfi7ynfKBa1yebsC+IynPLt0VFWiZxV7/EVDYRfBj4t9P8s0bfT LK1Cfw7MxRI08/Kfq5XadDyjUlHW/75OZLfYmOtnk+/AB+JwvWHa4+8KDZV5znUFEVRy1Nbx n2BLwVrQ375+wo2bRRrHFPrOQb39PVm7Wm8RQkyxh2LaEto0/y0/AQUjLqSUaBbxaoK7QEmr Tg8B1Ohx5TOEdPVohdicb5cfdIi6U1Gk2PYthB4FpOlJqFmwFUZdlc/pFvggi1+EZ4Iis02t DUvxQt2J7if1QZEajCVxpDsO6LeMGi0/RGud6v+1VTX0dLQ8aAKu7wjs1u2mgavGwI59ml/l dlY13zJ/pLREA8bSo78SG4y/hl+4rzWO2wzu9iS2nprPq259DTF3rrFHcMDzRCtN5daOaKAT krpFtECQtKpI6oskkSoaRQNOKZT8rQ1NoWobanO3qnjJ+tmkD+86AYPqIlgzkKB8TZ9Qe/Uz t4Exf+fxA6OSzb7ih+orMn2nYlOYTxaEHC4zGDoA4tYZ6s6eohuay/mJtC0y85+m5/yUmRZs l+iBk8D8MCscBuWKVf62EwY1Egap2CmhTrt1yZ9wFRL5uKU2C3DxfindQJSYDYaAjk/yw20c c7o1IN/PgDgdQUimRq76FyvwqFaoP46NGzPWQJSeCOwKWh+U6y2v77EYshV6Zpuvz8ENYb0K V2cVLP5pAMXli35GG4LjjUmdDyxuon4gBVgiSScLXdvqVLWfMhxwVHU49mWFpszlnIWATJ1j zXaHA32OsSq8M6Ui5bcu/q/EWOgV4FWWSbuxIKE8iC84Cc5ZH/31+D2kdrhHw8g1Cb93NQ/T iTEoiH3ZYzz3ri7O+ZqFqVxLGf18NEyWoR3k49qwYoVxWBfnJKeu3wOjWb0N9xfn6P4dnsEA zARkZbZ5w3s2UsrKXzspcqxU2iez9Bhe9ila3kXnCM87txPIKiR5b1A2yBypxK0oBnQbv50g joGgaF2uThK3qdT4Fprkn7VC6t3fwEQJSH2khWU892y5L5aYmqia/n41UZzm8ygEKDXpwhdX HjjfZJxVSR078h5LBfNyCipstCiKISWN4pD8EHPwHKix6BPJZk8l+QHn39iMGP55zg+zvIjy AZp1te8tZSGLGNk+OS4BARZP3v7fZB2mHmlgKBAk8KRx43qEI9mH2BBWYbrQOmoDDMNvO7mc QePESE5gnieELvbWwSY7Q01yhCHW4DuLHyRKHQDmJ9nWRqQP0xDgR8dRjR8n584CgWCy8noc UM/7TcUrA2dyFME2qdjMB/xVX3arQGjZ2IvSZSRGxFR6xlL+0bfNcHNpvI2BSxT+Yet6RCcM mHOLRodFnkHAwbXYjKrdqnr/9TL9PKUQ/azP+ebK6vbsvRQDr+J3c79idYgpmfUcJ/TYT86S KdnkktbASInR4KDwG5JEnJP0XqKNp/+xl/0+zUr/J7htq2zAkS3o9PIUeMaMM0zqU7ox/3fZ qjA3GAhbmwAnpIUmS2Xkv5GgBhL2nsoL370QdFi/WbMVP6CxfMRVkRGLXs1bIwRseo9xlUfY JaLzIqqifgoyKZyUQ4NVES9yJj2PopTcj37bBWfQx/VUdbObTzTn5OtOfL6GeAW1b8E8UX34 GnTEle/bG7ayX+0B1b2YLsK1GbCbVRfoN3vKE8zTzK4HZS9MFvjd4Ym6F9+ias9gneAXYIFG R57dU4F7riZ7CcCx+56B3QE9H1ua++Nhyee6eDcbJcQq/piRCpuxapc5zwhxr1Z4TshJrQ9k TbOrtNov1Ctk/WegjthXh1Urz9XhYWN9Ux8MKTd/5NEVD7K5hUIpWmXDh0LoZNiBLiN8+hIz cPTkavoNDpY29fd/M9ZCsSNbczbazwuNh3mHDOSBwwADHaqOWzZm01BgaSS+3mS/f1Y4tDnn JsDTKMeVURgTKtLTBQ4WoZacNErBWBB8/bTlsMD6HugoQOEQcxbusqCTfeOGbD1Lz3fi7BYZ hwOyLe+LIIJN4S91VYxDzsy1InMBUfUWshA5yN7aQph6kBQ83VlTnEyxEv/a0Ws4X4PENa7m xc3jk11ZuFnp1KOqx8nY0HHoic9ihx7gdL+nTWYayL8No+1VIBSTif47g0/bsi9TAFyYgm/2 0djMX2XItAZx6slfmdthgjGvJJJEvMJVqxIbigbwvSPbukp21BRws1C7UBC7OrBT5BlkVlyG XZDh31F0gNnKtUyIP6JTEKo5l1Zh6bLsyPxk+5tm0kRIEEC9G7UcykN6hRgCw==
- Ironport-sdr: wYOXvLhGU3Eto6bBOOL4RgT/57DgGlL56ZcG+9qREcbWr2qN3WxeE8nY1I05hXRCA4rcZsxWiO zs/PfYrz9kTBaSxLprtSUK8Rgx22B9c3yTJKg4k0JJ6MOikgID33VKNByTBVkh0jE2swelXTEO XLXY1zT7QoUq+9WisWcbIVYsSgTG78AmL2xXdOfKVjbwDaAOdAQKjg1KWQZUSnsFqbybeizRjH rfW2LVVp7q1VmF3KKHvFT7+XMuybV2kvh2447C1bmLVQg5EQ/fmtrjj8ftfJ7Y5t+pf1X4gHNU I6Vyg7x9Kzd9BpzPbyqN4kRv
On Sun, May 1, 2022 at 3:51 AM Stefan Monnier <monnier AT iro.umontreal.ca>
wrote:
> That's why I referred to e-voting, which is different from formally
> verified voting machines.
>
> e-voting relies on a cryptographic communication protocol and doesn't
> make particular assumptions about the trustworthiness of the machines
> used by the remote voters.
>
> Formally verified EVMs on the other hand rely on correctness of the code
> running on the actual voting machine (and correctness of the hardware,
> etc...).
Formal verification of EVMs is nice to, or I would say must, have, but
elections
require independent verification/auditing of results. To achieve independent
verification in case of EVMs, we can use VVPAT [1]. Every voter can verify
that
machine captures their intention (individual verifiability), and
everyone can verify
that the final tally is produced based on cast ballots (universal
verifiability). This chain
of verification, individual and universal, eliminates the chances of fraud.
My rationale for verifying the EVMs is that India is not going back to
paper based
elections (in fact, I conjecture that most of the countries conducting
elections in some
electronic form are not going back to paper based elections).
Therefore, it is better to
make sure that these machines are verified, open sourced, etc. EVMs
used in India is
closed source, the source code for conducting election in Australian
Capital Territory (ACT)
Canberra, is closed source and proprietary [2] (you need to sign
confidentiality
agreement), and even sometimes, in a very rare event, you can be denied to
inspect the source code [3]. If you dig more, you find secrecy is widespread
phenomena, either it is EVMs (simple machines) or e-voting (general purpose
computers). The horrifying part is that many companies involved in
e-voting (general purpose computer voting) simply write the software
programs to conduct elections in C/C++/Java and establish
the correctness by testing! Ideally, I would like a voting-machine whose
hardware is formally verified and open sourced, the software running on
it is formally verified and open sourced. Moreover, it has gone through
some very challenging stress testing something like this [4] (Btw, this
system was running on SeL4, a formally verified operating system
developed in Data61, Australia, but unfortunately CSIRO, the parent
body of Data61, dismantled the formal verification group. This group
literally achieved impossible!). If DARPA can achieve the impossible [4]
using formal verification, there is a lot of hope for democracy as well.
Best,
Mukesh
[1] https://en.wikipedia.org/wiki/Voter-verified_paper_audit_trail
[2]
https://www.elections.act.gov.au/elections_and_voting/electronic_voting_and_counting
[3] https://www.aec.gov.au/information-access/foi/2014/files/ls4912-1.pdf
[4] https://www.311institute.com/hack-proof-code-defeats-darpa-hackers/
>
> They both involve computers and voting but they are quite different, AFAIK.
>
>
> Stefan
>
- Re: [Coq-Club] Electronic Voting Machines in French Elections, Stefan Monnier, 05/01/2022
- Re: [Coq-Club] Electronic Voting Machines in French Elections, mukesh tiwari, 05/01/2022
- <Possible follow-up(s)>
- Re: [Coq-Club] Electronic Voting Machines in French Elections, Ralf Jung, 05/01/2022
- Re: [Coq-Club] Electronic Voting Machines in French Elections, Abhishek Anand, 05/02/2022
- Re: [Coq-Club] Electronic Voting Machines in French Elections, Eddy Westbrook, 05/02/2022
- Re: [Coq-Club] Electronic Voting Machines in French Elections, Abhishek Anand, 05/02/2022
- Re: [Coq-Club] Electronic Voting Machines in French Elections, Clément Pit-Claudel, 05/02/2022
- Re: [Coq-Club] Electronic Voting Machines in French Elections, Xavier Leroy, 05/02/2022
- Re: [Coq-Club] Electronic Voting Machines in French Elections, Clément Pit-Claudel, 05/02/2022
Archive powered by MHonArc 2.6.19+.