Ο αυτόματος έλεγχος μοντέλων (model checking) πρωτοκόλλων ασφαλείας και η εφαρμογή τυπικών μεθόδων επαλήθευσης στον τομέα της ασφάλειας είναι μια καινοτόμος μέθοδος, που μπορεί να προσφέρει πολλά πλεονεκτήματα προς την κατεύθυνση εύρεσης κενών ασφαλείας και απειλών. Έτσι καθίσταται δυνατή η επαλήθευση της ασφάλειας επικοινωνίας μέσα από την ανάπτυξη σαφώς ορισμένων μοντέλων που χρησιμεύουν ως ένα ισχυρό μαθηματικό εργαλείο ανάλυσης της συμπεριφοράς των πρωτοκόλλων. Με τις τυπικές μεθόδους επαλήθευσης είναι δυνατό να εντοπιστούν κενά ασφαλείας τα οποία πιθανότατα θα αποτελέσουν αιτία παραβίασης των εγγυήσεων που υποτίθεται ότι προσφέρει ένα κρυπτογραφικό πρωτόκολλο. Τα αποτελέσματα της οποιασδήποτε δυσλειτουργίας πρωτοκόλλων ασφαλείας μπορεί να οικονομικές συνέπειες ή να θέτουν σε κίνδυνο τα συμφέροντα των συμμετεχόντων. Ωστόσο οι περισσότερες τυπικές μέθοδοι ανάλυσης εστιάζουν κυρίως στον έλεγχο βασικών ιδιοτήτων ασφαλείας, όπως η απόκρυψη (secrecy) και η αυθεντικοποίηση (authentication). Εφαρμόζοντας ποσοτική ανάλυση σε πρωτόκολλα ασφαλείας είναι δυνατό να εξαχθούν χρήσιμα συμπεράσματα, όπως η αποδοτικότητα του πρωτοκόλλου. Ο όρος αποδοτικότητα αναφέρεται στο υπολογιστικό κόστος των συμμετεχόντων, δηλαδή το κόστος κρυπτογραφήσεων και αποκρυπτογραφήσεων και το κόστος εκθετικών πράξεων. Ο μηχανισμός Oblivious Transfer [7, 11, 17, 18] που προτάθηκε από τον Michael O. Rabin είναι ένα πρωταρχικό κρυπτογραφικό πρωτόκολλο, που μπορεί να χρησιμοποιηθεί στον πυρήνα άλλων κρυπτογραφικών μηχανισμών με λειτουργίες όπως ανταλλαγή μυστικού κλειδιού, ηλεκτρονική υπογραφή σύμβασης [18], σχήματα κεκαλυμμένων υπογραφών [19, 20, 21]. Στο πρωτόκολλο Oblivious Transfer συμμετέχουν δύο μέρη, ένας αποστολέας και ένας παραλήπτης. Στη γενική του μορφή ο παραλήπτης επιλέγει κάποια από τα μυστικά που στέλνει ο αποστολέας αγνοώντας αυτά που δεν επιλέγει, ενώ ο αποστολέας δεν έχει τρόπο να γνωρίζει σχετικά με τις επιλογές του παραλήπτη.Στην παρούσα εργασία γίνεται η ανάλυση του μηχανισμού ασφαλείας m-out-of-n Oblivious Transfer με το εργαλείο πιθανοκρατικού αυτόματου ελέγχου μοντέλων PRISM. Η ανάλυση έχει ως στόχο την επαλήθευση των βασικών ιδιοτήτων ασφαλείας του μηχανισμού, αλλά και την ποσοτική – συγκριτική ανάλυση των συμμετεχόντων μερών υπό το πρίσμα της αποδοτικότητας εκτέλεσης. Η ανάλυση του μοντέλου του Oblivious Transfer γίνεται μοντελοποιώντας την αλληλεπίδραση των δύο μερών του πρωτοκόλλου με μία Μαρκοβιανή Αλυσίδα Διακριτού Χρόνου (Discrete Time Markov Chain). Σto σχήμα m-out-of-n ο παραλήπτης λαμβάνει ακριβώς m από τα n μηνύματα που στέλνει ο αποστολέας (m < n). Τα δύο μέρη του πρωτοκόλλου συμφωνούν σε έναν αλγόριθμο δημοσίου κλειδιού όπως τον RSA και έναν αλγόριθμο ιδιωτικού κλειδιού όπως τον AES, με τους οποίους κρυπτογραφούνται τα μηνύματα που ανταλλάσσονται. Η ποσοτική ανάλυση βασίζεται στα διαφορετικά μήκη κλειδιών που μπορεί να χρησιμοποιηθούν για τον RSA αλγόριθμο, όπως για παράδειγμα 128 bit, 512 bit, 1024 bit και 2048 bit, που βέβαια προσφέρουν διαφορετικά επίπεδα ασφάλειας επιφέροντας ένα αντίστοιχο κόστος αποδοτικότητας εκτέλεσης.