Πιθανοκρατικός αυτόματος έλεγχος μοντέλου του μηχανισμού ασφαλείας oblivious transfer:
Creators: name: Αλεξίου, Νικόλαος Στυλιανού
Publisher: name: Aristotle University of Thessaloniki
Year: 2010
Subjects: Πιθανοκρατικός
Αυτόματος έλεγχος
Ασφάλεια υπολογιστικών συστημάτων
Oblivious transfer
Probabilistic model checking
Cryptographic protocols

description: Ο αυτόματος έλεγχος μοντέλων (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 &lt; n). Τα δύο μέρη του πρωτοκόλλου συμφωνούν σε έναν αλγόριθμο δημοσίου κλειδιού όπως τον RSA και έναν αλγόριθμο ιδιωτικού κλειδιού όπως τον AES, με τους οποίους κρυπτογραφούνται τα μηνύματα που ανταλλάσσονται. Η ποσοτική ανάλυση βασίζεται στα διαφορετικά μήκη κλειδιών που μπορεί να χρησιμοποιηθούν για τον RSA αλγόριθμο, όπως για παράδειγμα 128 bit, 512 bit, 1024 bit και 2048 bit, που βέβαια προσφέρουν διαφορετικά επίπεδα ασφάλειας επιφέροντας ένα αντίστοιχο κόστος αποδοτικότητας εκτέλεσης.
description: Probabilistic model checking of security protocols is a formal verification technique and an innovative method that can offer many benefits in order to exploit weaknesses and security threats of protocols showing non-deterministic behavior. Formal verification offers a strong mathematical base to verify security properties of systems, security mechanisms and security protocols. Results of formal verification can be the avoidance of disastrous effects occurring from misbehavior of security protocols and therefore prevent any malicious intruder to subvert a protocol’s guarantees [234]. Most of these approaches adopt the basic assumptions of the general Dolev and Yao model [9] that are summarized as follows: (i) the encryption method used is unbreakable, (ii) the intruder can prevent any message from reaching its destination and (iii) the intruder can create messages of his own. However the existing formal approaches focus mainly on secrecy and authentication guarantees. On the other hand, quantitative analysis of security protocols can be applied to obtain interesting results such as the efficiency of a security scheme or protocol and therefore compare workloads and computation efforts of the protocols’ participants. The term efficiency refers to the computational cost, number of modular exponentiations, encryptions and decryptions performed by the participants of the protocol [31, 132, 133]. The Oblivious transfer mechanism [556, 555, 36, 7] proposed by Michael O. Rabin, is a ubiquitous cryptographic primitive that can be used to implement a wide variety of other cryptographic protocols such as secret key exchange, contract signing [556], blind signatures schemes and secure function evaluation [557, 558, 559]. Oblivious Transfer is a two-party protocol between a sender and receiver. In its general form the receiver accepts or rejects secrets sent by the sender who remains oblivious about the receiver’s choice. In this paper we introduce probabilistic model checking as an efficient tool based approach for quantification analysis of an m-out-of-n Oblivious Transfer scheme, using the PRISM probabilistic model checker tool with the DTMC model type. Oblivious Transfer security properties are formally verified and a quantitative analysis is performed in order to analyze the mechanism in terms of efficiency. In this scheme the receiver obtains exactly m messages out of the n (n&gt;m) owned by the sender. The participants agree on a public key exchange algorithm, such as RSA and a private key algorithm such as AES. The former two cryptographic algorithms are chosen for this analysis and the quantitative analysis of the participants is based on the different lengths of RSA encryption keys.