Ανάλυση Πρωτοκόλλων Ηλεκτρονικής Ψηφοφορίας με την ProVerif

Abstract

Σκοπός της παρούσας εργασίας είναι η μελέτη ιδιοτήτων ασφαλείας κρυπτογραφικών πρωτοκόλλων μέσω τυπικών μεθόδων και εργαλείων αυτόματης ανάλυσης. Πιο συγκεκριμένα, θα εξετάσουμε τον Εφαρμοσμένο π-Λογισμό και το εργαλείο αυτόματης ανάλυσης ProVerif που βασίζεται σε αυτόν, προκειμένου να μελετήσουμε ιδιότητες ασφαλείας των πρωτοκόλλων ηλεκτρονικής ψηφοφορίας. Επιλέξαμε ένα νέο πρωτόκολλο ηλεκτρονικής ψηφοφορίας που προτάθηκε πρόσφατα στη βιβλιογραφία και επιτυγχάνει ισχυρές ιδιότητες ασφαλείας. Κατασκευάσαμε σενάρια στην ProVerif που μοντελοποιούν το πρωτόκολλο, προκειμένου να αποδείξουμε αυτόματα τις ιδιότητες της ορθότητας και της μυστικότητας της ψήφου. Ελπίζουμε να καταδείξουμε τη χρησιμότητα τέτοιων εργαλείων στην ανάλυση πρωτοκόλλων καθώς και να σκιαγραφήσουμε τους τομείς που θα μπορούσαν κατά τη γνώμη μας να αποτελέσουν αντικείμενο περαιτέρω μελέτης.