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

Περίληψη

Στις μέρες μας το δίκτυα υπολογιστών και οι διαδικτυακές επικοινωνίες αναπτύσσονται ταχύτατα, με αποτέλεσμα να αυξάνεται ολοένα και περισσότερο η ανάγκη για ποιότητα των προσφερόμενων υπηρεσιών, αλλά πρωτίστως για την ασφάλειά τους. Η παρούσα διδακτορική διατριβή ασχολείται με την μελέτη και τον έλεγχο πρωτοκόλλων ασφαλείας με χρήση των τυπικών μεθόδων ανάλυσης συστημάτων. Ειδικότερα η ερευνά που παρουσιάζεται, αφορά τις ιδιότητες ασφαλείας που εγγυώνται σύγχρονα πρωτόκολλα ασφαλείας προς τις συμμετέχουσες οντότητες. Με τη χρήση αυτοματοποιημένων τυπικών μεθόδων επαλήθευσης, διεξήχθη μια ενδελεχής έρευνα προς την ανάπτυξη εξειδικευμένων θεωριών δημιουργίας εισβολέων. Με την βοήθεια αυτών ελέχθησαν εξαντλητικά για λάθη, σύγχρονα πρωτόκολλα ασφαλείας, προσπαθώντας με αυτό τον τρόπο να συμπεριληφθούν στον έλεγχο και εχθρικές ενέργειες που μπορεί να εξαπολύσει ένας κακόβουλος χρήστης. Οι εισβολείς αυτοί σχεδιάστηκαν και υλοποιήθηκαν μέσα σε περιβάλλοντα μοντελοποίησης σε αυτοματοποιημένα ...
περισσότερα

Περίληψη σε άλλη γλώσσα

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 ...
περισσότερα
Πρέπει να είστε εγγεγραμένος χρήστης για έχετε πρόσβαση σε όλες τις υπηρεσίες του ΕΑΔΔ  Είσοδος /Εγγραφή

Όλα τα τεκμήρια στο ΕΑΔΔ προστατεύονται από πνευματικά δικαιώματα.

DOI
10.12681/eadd/19375
Διεύθυνση Handle
http://hdl.handle.net/10442/hedi/19375
Εναλλακτικός τίτλος
Developing formal methods for security protocols validation
Συγγραφέας
Μπασαγιάννης, Στυλιανός Δημήτριος
Ημερομηνία
2009
Ίδρυμα
Αριστοτέλειο Πανεπιστήμιο Θεσσαλονίκης (ΑΠΘ). Σχολή Θετικών Επιστημών. Τμήμα Πληροφορικής
Εξεταστική επιτροπή
Πομπόρτσης Ανδρέας
Παπαδημητρίου Γεώργιος
Κατσαρός Παναγιώτης
Πάγκαλος Γεώργιος
Καρατζά Ελένη
Καρανίκας Κωνσταντίνος
Κάτος Βασίλειος
Επιστημονικό πεδίο
Φυσικές Επιστήμες
Επιστήμες Ηλεκτρονικών Υπολογιστών & Πληροφορικής
Λέξεις-κλειδιά
Τυπικές μέθοδοι ανάλυσης συστημάτων; Πρωτόκολλα ασφαλείας; Μοντέλα εισβολέων; Έκρηξη χώρου καταστάσεων
Χώρα
Ελλάδα
Γλώσσα
Ελληνικά
Άλλα στοιχεία
xi, 217 σ., εικ.