Ανάπτυξη τυπικών μεθόδων για τον έλεγχο πρωτοκόλλων ασφαλείας

Abstract

Nowadays, the spread of computer networks and internet communications increases rapidly, causing an even strong need for quality of services, but mostly, the security of them. The present doctorate thesis involves with the verification of security protocols with the use of formal methods. The research been conducted, studies the security guaranties that most of the modern security protocols, tend to offer to the participant entities. Related work has shown that in order to successfully verify a security protocol, it is a necessity to check the protocol correctness while operating with a strong intruder entity. Using automatic model checking tools, we have developed discrete formal method techniques that combined with the proposed intruder theories can be useful for the correctness and the exhaustive verification of a series of security properties. Using these intruder theories, we verify security protocols’ tolerance against common attack policies that can be applied today by dishonest protocol users. One of the major problems found today in the research area of formal methods is the known problem of the State Space explosion. When modeling a system using model checking, the produced state space may increase dramatically due to the complexity of the processed involved in the model or for example the mechanisms that are embedded into (e.g. random generator number machine, cryptographic functions). Furthermore, the combination of a powerful intruder model into the security system may lead to an enormous state space, resulting in a difficult and time-consuming security analysis. In the present thesis, three distinct intruder theories and models have been developed in order to guide the analysts into a much easier analysis of their security protocols. While the analyst today may find a wide area of security properties that target towards verification of them, the described intruder theories provide a selection for the appropriate intruder model -depending on the properties- to be applied, providing a successful verification mean, into revealing potential security flaws. We formally describe these three intruder theories and verify their success over a series of security protocols. As a result, the proposed intruders have not only dramatically decreased the produces state space during model checking but also they have been proved capable of revealing unknown to us security flaws in the tested protocol systems. To conclude, the contribution of this thesis lies in the successful verification of the security guaranties of security protocols, with the help of specific intruder models, which are independent from the used mean of communication by the protocols’ participants. Using the developed powerful intruder creation methodologies, the analyst may exhaustively check its protocol for security flaws, using formal methods techniques, without producing a large state space that could lead its analysis impossible to be conducted.

Στις μέρες μας το δίκτυα υπολογιστών και οι διαδικτυακές επικοινωνίες αναπτύσσονται ταχύτατα, με αποτέλεσμα να αυξάνεται ολοένα και περισσότερο η ανάγκη για ποιότητα των προσφερόμενων υπηρεσιών, αλλά πρωτίστως για την ασφάλειά τους. Η παρούσα διδακτορική διατριβή ασχολείται με την μελέτη και τον έλεγχο πρωτοκόλλων ασφαλείας με χρήση των τυπικών μεθόδων ανάλυσης συστημάτων. Ειδικότερα η ερευνά που παρουσιάζεται, αφορά τις ιδιότητες ασφαλείας που εγγυώνται σύγχρονα πρωτόκολλα ασφαλείας προς τις συμμετέχουσες οντότητες. Με τη χρήση αυτοματοποιημένων τυπικών μεθόδων επαλήθευσης, διεξήχθη μια ενδελεχής έρευνα προς την ανάπτυξη εξειδικευμένων θεωριών δημιουργίας εισβολέων. Με την βοήθεια αυτών ελέχθησαν εξαντλητικά για λάθη, σύγχρονα πρωτόκολλα ασφαλείας, προσπαθώντας με αυτό τον τρόπο να συμπεριληφθούν στον έλεγχο και εχθρικές ενέργειες που μπορεί να εξαπολύσει ένας κακόβουλος χρήστης. Οι εισβολείς αυτοί σχεδιάστηκαν και υλοποιήθηκαν μέσα σε περιβάλλοντα μοντελοποίησης σε αυτοματοποιημένα εργαλεία ελέγχου μοντέλων, που ανήκουν στην οικογένεια των Τυπικών Μεθόδων (Formal Methods) Ανάλυσης Συστημάτων. Ένα από τα κύρια προβλήματα που παρουσιάζεται στην ερευνητική περιοχή του ελέγχου ασφαλείας με χρήση των τυπικών μεθόδων, είναι και αυτό της Έκρηξης του Χώρου Καταστάσεων, ΕΧΚ (state explosion problem). Πρόκειται για τον παραγόμενο χώρο των καταστάσεων της αναπαράστασης του συστήματος, ο οποίος εξαιτίας της πολυπλοκότητας των μηχανισμών που έγκειται σε όλα σχεδόν τα σύγχρονα πρωτόκολλα ασφαλείας (λ.χ. κρυπτογραφικών μηχανισμών, μηχανών παραγωγής τυχαίων αριθμών) μπορεί να οδηγήσει σε ΕΧΚ. Στην ίδια κατεύθυνση οδηγούμαστε και με την χρήση των υπαρκτών μεθοδολογιών κατασκευής εισβολέων, οι οποίες και στην πλειοψηφία τους βασίζονται στο διάσημο μοντέλο εισβολέα των Dolev και Yao. Πιο συγκεκριμένα, στην διατριβή αυτή, περιγράφεται η δημιουργία τριών καινούργιων θεωριών κατασκευής εισβολέων, οι οποίοι προσπαθούν με βάση τον σχεδιασμό τους, να προσπεράσουν το πρόβλημα της ΕΚΧ, αλλά παράλληλα να καταφέρουν να αναπαριστούν πιστά επιθέσεις που μπορούν να ανιχνευθούν σήμερα σε πρωτόκολλα ασφαλείας. Παρουσιάζεται η μαθηματική ορολογία στην οποία βασίστηκε ο κάθε εισβολέας, η αποτελεσματικότητά αυτών απέναντι σε μια σειρά από πρωτόκολλα ασφαλείας που εξετάσθηκαν και παράλληλα, η ικανότητα που προσφέρουν, για την αποφυγή της ΕΧΚ. Ως αποτέλεσμα της χρήσης των εισβολέων αυτών, ανακαλύφθηκαν παραβιάσεις ασφαλείας σε υπό εξέταση πρωτόκολλα, οι οποίες ήταν άγνωστες μέχρι σήμερα. Συνοψίζοντας, η συνεισφορά της παρούσας διατριβής εντοπίζεται κατά κύριο λόγο στον έλεγχο εγγυήσεων των πρωτοκόλλων ασφαλείας, ανεξάρτητα του μέσου επικοινωνίας που υλοποιείται το υπό εξέταση πρωτόκολλο. Με τη βοήθεια εξειδικευμένων εισβολέων επιτυγχάνεται, όχι μόνο ο εξαντλητικός έλεγχος για λάθη ασφαλείας των πρωτοκόλλων αυτών, αλλά επιπρόσθετα, αποφεύγεται η έκρηξη του χώρου των καταστάσεων, επιτρέποντας τη γρήγορη και αποτελεσματική ανάλυση του εκάστοτε συστήματος ασφαλείας.