Μοντελοποίηση του Πρωτοκόλλου Εξουσιοδότησης OAuth 2.0 με την Γλώσσα Maude

Abstract

Το πρωτόκολλο OAuth 2.0 είναι το πρωτόκολλο εξουσιοδότησης που χρησιμοποιείται ευρέως στην βιομηχανία, για περιπτώσεις όπου ο χρήστης επιθυμεί να παραχωρήσει άδεια σε μια εφαρμογή για να χρησιμοποιήσει δεδομένα τα οποία είναι αποθηκευμένα σε ένα API. Η γλώσσα προγραμματισμού Maude αποτελεί ένα δυνατό εργαλείο, στο οποίο δυναμικά συστήματα σαν το OAuth 2.0 τυποποιούνται ως θεωρίες της λογικής επαναγραφής. Σε αυτήν, οι εξισώσεις και οι κανόνες επαναγραφής της λογικής αποτυπώνουν την εξέλιξη του συστήματος από την μία κατάσταση στην επόμενη. Ο αντικειμενοστραφής προγραμματισμός που υποστηρίζεται από τις τελευταίες εκδόσεις της γλώσσας είναι κατάλληλος για την μοντελοποίηση πρωτοκόλλων που περιλαμβάνουν αποστολή μηνυμάτων. Η εργασία περιλαμβάνει μία σύντομη εισαγωγή στην Maude, στις δυνατότητες της ως προς την μοντελοποίηση πρωτοκόλλων και τον έλεγχο της εγκυρότητας ή της ασφάλειας των μοντέλων. Ακολουθεί μια περιγραφή της χρήσης του πρωτοκόλλου για διάφορους τύπους εφαρμογών. Παρουσιάζονται οι δύο βασικές ροές εξουσιοδότησης και τα αναγνωριστικά τα οποία λαμβάνουν οι εφαρμογές για να αποκτήσουν πρόσβαση στα δεδομένα του χρήστη. Η μοντελοποίηση του πρωτοκόλλου βρίσκεται στο Κεφάλαιο 3. Γίνεται περιγραφή των κανόνων επαναγραφής της μοντελοποίησης και αναλύεται η αντιστοιχία τους με την πραγματική ανταλλαγή μηνυμάτων στο πρωτόκολλο. Στο τελευταίο μέρος, προσδιορίζεται ένα σύστημα πολλαπλών διακομιστών και επιβεβαιώνεται η έγκυρη λειτουργία του. Γίνεται εισαγωγή ενός Attacker (κακόβουλου πράκτορα) στην μοντελοποίηση και γίνεται έλεγχος προδιαγραφών του πρωτοκόλλου με τον ενσωματωμένο LTL Model Checker της γλώσσας Maude.