Specifying and implementing privacy-preserving cryptographic protocols

Abstract

Formal methods are an important tool for designing and implementing secure cryptographic protocols. However, the existing work on formal methods does not cover privacy-preserving protocols as much as other types of protocols (for example, authentication protocols). Furthermore, privacy-related properties are not always easy or even possible to prove statically, but need to be checked dynamically during the protocol’s execution. This thesis: (i) proposes abstractions for some (relatively) complex cryptographic primitives used in privacy-preserving protocols, and uses these abstractions to develop suitable message constructors and a linkability-oriented type system for Typed MSR (a strongly typed specification language for security protocols), and (ii) demonstrates how these typed message constructors can be implemented in Jif (a security-oriented extension of a subset of the Java programming language dealing with information flow) in such a way that linkability vulnerabilities can be detected with a mixture of static and runtime checks.

Η διατριβή αυτή ασχολείται με την προδιαγραφή και υλοποίηση πρωτοκόλλων ασφάλειας με απαιτήσεις διασφάλισης ιδιωτικότητας, όπως για παράδειγμα τα πρωτόκολλα ηλεκτρονικών μετρητών, ηλεκτρονικής ψηφοφορίας και επιλεκτικής αποκάλυψης δεδομένων. Ο στόχος, όσον αφορά την προδιαγραφή τους, είναι αυτή να γίνει με τυπική μέθοδο (formal method), και, όσον αφορά την υλοποίησή τους, να βασίζεται στην προδιαγραφή τους και να διασφαλίζει τις περί ιδιωτικότητας απαιτήσεις. Το υπάρχον ερευνητικό έργο στη διεθνή βιβλιογραφία σε τυπικές μεθόδους δεν καλύπτει επαρκώς τα πρωτόκολλα ασφάλειας με απαιτήσεις διασφάλισης ιδιωτικότητας όσο άλλων ειδών πρωτόκολλα ασφάλειας, όπως τα πρωτόκολλα αυθεντικοποίησης. Στην παρούσα διατριβή υποστηρίζεται ότι οι λόγοι για αυτή την ανεπάρκεια μελέτης είναι οι εξής: Πρώτον, ότι τα πρωτόκολλα με απαιτήσεις διασφάλισης ιδιωτικότητας βασίζονται σε πιο εξειδικευμένη κρυπτογραφία, όπως η δέσμευση (commitment), η τυφλή υπογραφή (blind signature), η απόδειξη μηδενικής γνώσης (zero-knowledge proof), η ομομορφική κρυπτογραφία (homomorphic encryption), το mix του Chaum και το onion routing. Δεύτερον, ότι είναι απαραίτητη η διαφοροποίηση στη μοντελοποίηση της κλασικής κρυπτογραφίας (συμμετρική και ασύμμετρη κρυπτογράφηση και ψηφιακές υπογραφές) που τα πρωτόκολλα αυτά χρησιμοποιούν από κοινού με τα υπόλοιπα πρωτόκολλα. Η διατριβή αυτή χρησιμοποιεί ως βάση τη γλώσσα προδιαγραφής πρωτοκόλλων Typed MSR [14, 15], καθώς και την προηγούμενη εργασία μας στην ίδια [10, 7, 9, 8, 6] ερευνητική κατεύθυνση και στοχεύει με τροποποιήσεις και προσθήκες να την μετατρέψει σε κατάλληλη, αφενός για την προδιαγραφή πρωτοκόλλων με απαιτήσεις διασφάλισης ιδιωτικότητας, αφετέρου για την προδιαγραφή ενός κατά Dolev-Yao επιτιθέμενου [19] σχεδιασμένου για επίθεση σε πρωτόκολλα τέτοιου είδους. Επιπλέον, χρησιμοποιεί ως βάση τη γλώσσα Jif [30, 31, 29], καθώς και την προηγούμενη εργασία μας [6] στην ίδια ερευνητική κατεύθυνση και στοχεύει να επιδείξει πως η γλώσσα αυτή, που διαθέτει σύστημα τύπων για απαιτήσεις ασφάλειας, μπορεί να χρησιμοποιηθεί με τέτοιον τρόπο ώστε οι αδυναμίες στην υλοποίηση πρωτοκόλλων ασφαλείας όσον αφορά τη συνδεσιμότητα (linkability) να μπορούν να ανιχνευτούν με ένα συνδυασμό στατικών και δυναμικών (runtime) ελέγχων. Τα βασικά συμπεράσματα της διατριβής αυτής είναι τα ακόλουθα: 1. Προκειμένου η Typed MSR να είναι κατάλληλη για την προδιαγραφή πρωτοκόλλων ασφάλειας με απαιτήσεις ιδιωτικότητας, δεν θα πρέπει να μοντελοποιεί τη συμμετρική και την ασύμμετρη κρυπτογράφηση ως αιτιοκρατική. Μια τέτοια απλούστευση μπορεί να μη δημιουργεί προβλήματα στη μοντελοποίηση άλλων πρωτοκόλλων, αλλά οδηγεί σε ανύπαρκτες αδυναμίες διασύνδεσης στα πρωτόκολλα που μελετούμε στην παρούσα διατριβή. 2. Μπορούμε να κατασκευάσουμε υψηλού επιπέδου μοντελοποιήσεις για κρυπτογραφία πιο σύνθετη από την κλασική, όπως είναι η δέσμευση, η τυφλή υπογραφή, η απόδειξη μηδενικής γνώσης και η ομομορφική κρυπτογραφία. 3. Η χρήση μη διαδραστικών μοντελοποιήσεων για τις αποδείξεις μηδενικής γνώσης οδηγεί στην απλοποίηση τόσο της προδιαγραφής των πρωτοκόλλων, όσο και της μετατροπής αυτής σε υλοποίησή τους. 4. Με βάση τις προαναφερθείσες αλλαγές και προσθήκες, η Typed MSR γίνεται κατάλληλη για την προδιαγραφή πρωτοκόλλων ασφάλειας με απαιτήσεις ιδιωτικότητας, όπως δείχνει η προδιαγραφή των δύο πρωτοκόλλων ηλεκτρονικής ψηφοφορίας που περιέχονται στην παρούσα διατριβή. 5. Ένα απλό σύστημα τύπων, που χρησιμοποιείται παράλληλα με το σύστημα τύπων της Typed MSR, αποτρέπει συγκεκριμένες εσφαλμένες χρήσεις της κρυπτογραφίας που μπορεί να οδηγήσουν σε αδυναμίες συνδεσιμότητας, καθώς και να παρακολουθήσει την απειλή συνδεσιμότητας που προκύπτει από κάθε πιθανή χρήση της κρυπτογραφίας. 6. Είναι απαραίτητη η ενημέρωση του εκφρασμένου σε Typed MSR μοντέλου του κατά Dolev-Yao επιτιθέμενου με βάση τα παραπάνω, ώστε να μπορεί πλέον να επιτεθεί στα πρωτόκολλα τα οποία μελετάμε. 7. Η ενημερωμένη αυτή έκδοση του κατά Dolev-Yao επιτιθέμενου δημιουργεί ένα τυπικό (formal) περιβάλλον, στο οποίο μπορούν να εκφραστούν αδυναμίες διασύνδεσης των πρωτοκόλλων. 8. Τα παραπάνω μπορούν να αποτελέσουν τη βάση για τη χρήση της γλώσσας Jif με τέτοιο τρόπο, ώστε οι αδυναμίες στην υλοποίηση πρωτοκόλλων ασφαλείας όσον αφορά τη συνδεσιμότητα να μπορούν να ανιχνευτούν με ένα συνδυασμό στατικών και δυναμικών ελέγχων. 9. Η συνδεσιμότητα δεν είναι δυνατό να ελεγχθεί στατικά στη γενική περίπτωση, αλλά μπορεί να ελέγχεται δυναμικά κατά την εκτέλεση των πρωτοκόλλων. 10. Οι κανόνες της Typed MSR με τους οποίους παράγονται τα καινούρια μηνύματα τα οποία μπορεί να σχηματίσει ο κατά Dolev-Yao επιτιθέμενος από ένα σύνολο γνωστών μηνυμάτων χωρίζονται σε δύο κατηγορίες, ανάλογα με το αν χρησιμοποιούνται στη φάση αποδόμησης των γνωστών μηνυμάτων ή στη φάση κατασκευής των καινούριων. Συγκεκριμένα μηνύματα που βασίζονται στην κρυπτογραφία της διατριβής αυτής δεν μπορούν όμως να χωριστούν σε μία από τις δύο κατηγορίες, καθώς είναι ωφέλιμη η χρήση τους και στις δύο αυτές φάσεις.