We devise an abstraction of zero-knowledge protocols that is accessible to a fully mechanized analysis. The abstraction is formalized within the applied pi-calculus using a novel equational theory that abstractly characterizes the cryptographic semantics of zero-knowledge proofs. We present an encoding from the equational theory into a convergent rewriting system that is suitable for the automated protocol verifier ProVerif. The encoding is sound and fully automated. We successfully used ProVerif to obtain the first mechanized analysis of (a simplified variant of) the Direct Anonymous Attestation (DAA) protocol. This required us to devise novel abstractions of sophisticated cryptographic security definitions based on interactive games. The analysis reported a novel attack on DAA that was overlooked in its existing cryptographic security proof. We propose a revised variant of DAA that we successfully prove secure using ProVerif.
We proposed a new zero-knowledge proof of identity protocol based on Mandelbrot and Julia Fractal sets. The Fractal based zero-knowledge protocol was possible because of the intrinsic connection between the Mandelbrot and Julia Fractal sets. In the proposed protocol, the private key was used as an input parameter for Mandelbrot Fractal function to generate the corresponding public key. Julia Fractal function was then used to calculate the verified value based on the existing private key and the received public key. The proposed protocol was designed to be resistant against attacks. Fractal based zero-knowledge protocol was an attractive alternative to the traditional number theory zero-knowledge protocol.
Η διατριβή αυτή ασχολείται με την προδιαγραφή και υλοποίηση πρωτοκόλλων ασφάλειας με απαιτήσεις διασφάλισης ιδιωτικότητας, όπως για παράδειγμα τα πρωτόκολλα ηλεκτρονικών μετρητών, ηλεκτρονικής ψηφοφορίας και επιλεκτικής αποκάλυψης δεδομένων. Ο στόχος, όσον αφορά την προδιαγραφή τους, είναι αυτή να γίνει με τυπική μέθοδο (formal method), και, όσον αφορά την υλοποίησή τους, να βασίζεται στην προδιαγραφή τους και να διασφαλίζει τις περί ιδιωτικότητας απαιτήσεις. Το υπάρχον ερευνητικό έργο στη διεθνή βιβλιογραφία σε τυπικές μεθόδους δεν καλύπτει επαρκώς τα πρωτόκολλα ασφάλειας με απαιτήσεις διασφάλισης ιδιωτικότητας όσο άλλων ειδών πρωτόκολλα ασφάλειας, όπως τα πρωτόκολλα αυθεντικοποίησης. Στην παρούσα διατριβή υποστηρίζεται ότι οι λόγοι για αυτή την ανεπάρκεια μελέτης είναι οι εξής: Πρώτον, ότι τα πρωτόκολλα με απαιτήσεις διασφάλισης ιδιωτικότητας βασίζονται σε πιο εξειδικευμένη κρυπτογραφία, όπως η δέσμευση (commitment), η τυφλή υπογραφή (blind signature), η απόδειξη μηδενικής γνώσης (zero-knowledge proof), η ομομορφική κρυπτογραφία (homomorphic encryption), το mix του Chaum και το onion routing. Δεύτερον, ότι είναι απαραίτητη η διαφοροποίηση στη μοντελοποίηση της κλασικής κρυπτογραφίας (συμμετρική και ασύμμετρη κρυπτογράφηση και ψηφιακές υπογραφές) που τα πρωτόκολλα αυτά χρησιμοποιούν από κοινού με τα υπόλοιπα πρωτόκολλα. Η διατριβή αυτή χρησιμοποιεί ως βάση τη γλώσσα προδιαγραφής πρωτοκόλλων Typed MSR [14, 15], καθώς και την προηγούμενη εργασία μας στην ίδια [10, 7, 9, 8, 6] ερευνητική κατεύθυνση και στοχεύει με τροποποιήσεις και προσθήκες να την μετατρέψει σε κατάλληλη, αφενός για την προδιαγραφή πρωτοκόλλων με απαιτήσεις διασφάλισης ιδιωτικότητας, αφετέρου για την προδιαγραφή ενός κατά Dolev-Yao επιτιθέμενου [19] σχεδιασμένου για επίθεση σε πρωτόκολλα τέτοιου είδους. Επιπλέον, χρησιμοποιεί ως βάση τη γλώσσα Jif [30, 31, 29], καθώς και την προηγούμενη εργασία μας [6] στην ίδια ερευνητική κατεύθυνση και στοχεύει να επιδείξει πως η γλώσσα αυτή, που διαθέτει σύστημα τύπων για απαιτήσεις ασφάλειας, μπορεί να χρησιμοποιηθεί με τέτοιον τρόπο ώστε οι αδυναμίες στην υλοποίηση πρωτοκόλλων ασφαλείας όσον αφορά τη συνδεσιμότητα (linkability) να μπορούν να ανιχνευτούν με ένα συνδυασμό στατικών και δυναμικών (runtime) ελέγχων. Τα βασικά συμπεράσματα της διατριβής αυτής είναι τα ακόλουθα: 1. Προκειμένου η Typed MSR να είναι κατάλληλη για την προδιαγραφή πρωτοκόλλων ασφάλειας με απαιτήσεις ιδιωτικότητας, δεν θα πρέπει να μοντελοποιεί τη συμμετρική και την ασύμμετρη κρυπτογράφηση ως αιτιοκρατική. Μια τέτοια απλούστευση μπορεί να μη δημιουργεί προβλήματα στη μοντελοποίηση άλλων πρωτοκόλλων, αλλά οδηγεί σε ανύπαρκτες αδυναμίες διασύνδεσης στα πρωτόκολλα που μελετούμε στην παρούσα διατριβή. 2. Μπορούμε να κατασκευάσουμε υψηλού επιπέδου μοντελοποιήσεις για κρυπτογραφία πιο σύνθετη από την κλασική, όπως είναι η δέσμευση, η τυφλή υπογραφή, η απόδειξη μηδενικής γνώσης και η ομομορφική κρυπτογραφία. 3. Η χρήση μη διαδραστικών μοντελοποιήσεων για τις αποδείξεις μηδενικής γνώσης οδηγεί στην απλοποίηση τόσο της προδιαγραφής των πρωτοκόλλων, όσο και της μετατροπής αυτής σε υλοποίησή τους. 4. Με βάση τις προαναφερθείσες αλλαγές και προσθήκες, η Typed MSR γίνεται κατάλληλη για την προδιαγραφή πρωτοκόλλων ασφάλειας με απαιτήσεις ιδιωτικότητας, όπως δείχνει η προδιαγραφή των δύο πρωτοκόλλων ηλεκτρονικής ψηφοφορίας που περιέχονται στην παρούσα διατριβή. 5. Ένα απλό σύστημα τύπων, που χρησιμοποιείται παράλληλα με το σύστημα τύπων της Typed MSR, αποτρέπει συγκεκριμένες εσφαλμένες χρήσεις της κρυπτογραφίας που μπορεί να οδηγήσουν σε αδυναμίες συνδεσιμότητας, καθώς και να παρακολουθήσει την απειλή συνδεσιμότητας που προκύπτει από κάθε πιθανή χρήση της κρυπτογραφίας. 6. Είναι απαραίτητη η ενημέρωση του εκφρασμένου σε Typed MSR μοντέλου του κατά Dolev-Yao επιτιθέμενου με βάση τα παραπάνω, ώστε να μπορεί πλέον να επιτεθεί στα πρωτόκολλα τα οποία μελετάμε. 7. Η ενημερωμένη αυτή έκδοση του κατά Dolev-Yao επιτιθέμενου δημιουργεί ένα τυπικό (formal) περιβάλλον, στο οποίο μπορούν να εκφραστούν αδυναμίες διασύνδεσης των πρωτοκόλλων. 8. Τα παραπάνω μπορούν να αποτελέσουν τη βάση για τη χρήση της γλώσσας Jif με τέτοιο τρόπο, ώστε οι αδυναμίες στην υλοποίηση πρωτοκόλλων ασφαλείας όσον αφορά τη συνδεσιμότητα να μπορούν να ανιχνευτούν με ένα συνδυασμό στατικών και δυναμικών ελέγχων. 9. Η συνδεσιμότητα δεν είναι δυνατό να ελεγχθεί στατικά στη γενική περίπτωση, αλλά μπορεί να ελέγχεται δυναμικά κατά την εκτέλεση των πρωτοκόλλων. 10. Οι κανόνες της Typed MSR με τους οποίους παράγονται τα καινούρια μηνύματα τα οποία μπορεί να σχηματίσει ο κατά Dolev-Yao επιτιθέμενος από ένα σύνολο γνωστών μηνυμάτων χωρίζονται σε δύο κατηγορίες, ανάλογα με το αν χρησιμοποιούνται στη φάση αποδόμησης των γνωστών μηνυμάτων ή στη φάση κατασκευής των καινούριων. Συγκεκριμένα μηνύματα που βασίζονται στην κρυπτογραφία της διατριβής αυτής δεν μπορούν όμως να χωριστούν σε μία από τις δύο κατηγορίες, καθώς είναι ωφέλιμη η χρήση τους και στις δύο αυτές φάσεις.
Nowadays it is widely accepted to formulate the security of a protocol carrying out a given task via the “trusted-party paradigm,” where the protocol execution is compared with an ideal process where the outputs are computed by a trusted party that sees all the inputs. A protocol is said to securely carry out a given task if running the protocol with a realistic adversary amounts to “emulating” the ideal process with the appropriate trusted party. In the Universal Composability (UC) framework the program run by the trusted party is called an ideal functionality. While this simulation-based security formulation provides strong security guarantees, its usefulness is contingent on the properties and correct specification of the ideal functionality, which, as demonstrated in recent years by the coexistence of complex, multiple functionalities for the same task as well as by their “unstable” nature, does not seem to be an easy task. In this paper we address this problem, by introducing a general methodology for the sound specification of ideal functionalities. First, we introduce the class of canonical ideal functionalities for a cryptographic task, which unifies the syntactic specification of a large class of cryptographic tasks under the same basic template functionality. Furthermore, this representation enables the isolation of the individual properties of a cryptographic task as separate members of the corresponding class. By endowing the class of canonical functionalities with an algebraic structure we are able to combine basic functionalities to a single final canonical functionality for a given task. Effectively, this puts forth a bottom-up approach for the specification of ideal functionalities: first one defines a set of basic constituent functionalities for the task at hand, and then combines them into a single ideal functionality taking advantage of the algebraic structure. In our framework, the constituent functionalities of a task can be derived either directly or, following a translation strategy we introduce, from existing game-based definitions; such definitions have in many cases captured desired individual properties of cryptographic tasks, albeit in less adversarial settings. Our translation methodology entails a sequence of steps that systematically derive a corresponding canonical functionality given a game-based definition, effectively “lifting” the game-based definition to its composition-safe version. We showcase our methodology by applying it to a variety of basic cryptographic tasks, including commitments, digital signatures, zero-knowledge proofs, and oblivious transfer. While in some cases our derived canonical functionalities are equivalent to existing formulations, thus attesting to the validity of our approach, in others they differ, enabling us to “debug” previous definitions and pinpoint their shortcomings.
Based on USB key and zero-knowledge proof,a mutual authentication scheme is proposed in this paper,which has realized to user’s authentication,moreover has realized to user’s public key authentication.The analysis indicates that the scheme is secure and the computation complexity is low.
The abstraction of cryptographic operations by term algebras, called Dolev–Yao models, is essential in almost all tool-supported methods for proving security protocols. Recently significant progress was made in proving that Dolev–Yao models offering the core cryptographic operations such as encrypt ion and digital signatures can be sound with respect to actual cryptographic realizations and security definitions. Recent work, however, has started to extend Dolev–Yao models to more sophisticated operations with unique security features. Zero-knowledge proofs arguably constitute the most amazing such extension. In this paper, we first identify which additional properties a cryptographic (non-interactive) zero-knowledge proof needs to fulfill in order to serve as a computationally sound implementation of symbolic (Dolev–Yao style) zero-knowledge proofs; this leads to the novel definition of a symbolically-sound zero-knowledge proof system. We prove that even in the presence of arbitrary active adversaries, such proof systems constitute computationally sound implementations of symbolic zero-knowledge proofs. This yields the first computational soundness result for symbolic zero-knowledge proofs and the first such result against fully active adversaries of Dolev–Yao models that go beyond the core cryptographic operations.
The development of mobile telecommunication is emerging as a means of payment by replacing cash and credit cards. Information exchange is regarded as the most important communication system in conforming valid users. The most efficient means of securing information applies cryptography, which relies on small size information and demands its strict management. It is crucial to distribute key to cryptographic communication receiver without exposing key to the third party. The suggested protocol takes authentication and key distribution, which allows session key distribution after user authentication through an authentication center. However, the paper suggests an authentication and key distribution protocol which can be available to smartcard-suing personal communication system. This protocol takes ID-based key distribution method by means of Zero-Knowledge authentication proof which does not reveal secret information to the authentication center.
We propose a cryptographic protocol for biometrics authentication without revealing personal biometrical data against malicious verifier. Our protocol uses a neural network and zero-knowledge interactive proof. In this paper, we developed a sample implementation system of our proposed protocol and we evaluate the performance and the accuracy of the proposed protocol. Especially, we study several algorithms for feature extraction of minutiae of fingerprint which is appropriate to our protocol. We examine false acceptance rates and rejection rates
Biometric Identification and Security
User Authentication and Security Systems
Advanced Steganography and Watermarking Techniques
Abhilasha Bhargav-Spantzel, Anna Squicciarini, Elisa Bertino
An emerging approach to the problem of reducing the identity theft is represented by the adoption of biometric authentication systems. Such systems however present however several challenges, related to privacy, reliability, security of the biometric data. Inter-operability is also required among the devices used for the authentication. Moreover, very often biometric authentication in itself is not sufficient as a conclusive proof of identity and has to be complemented with multiple other proofs of identity like passwords, SSN, or other user identifiers. Multi-factor authentication mechanisms are thus required to enforce strong authentication based on the biometric and identifiers of other nature.In this paper we provide a two-phase authentication mechanism for federated identity management systems. The first phase consists of a two-factor biometric authentication based on zero knowledge proofs. We employ techniques from vector-space model to generate cryptographic biometric keys. These keys are kept secret, thus preserving the confidentiality of the biometric data, and at the same time exploit the advantages of a biometric authentication. The second authentication combines several authentication factors in conjunction with the biometric to provide a strong authentication. A key advantage of our approach is that any unanticipated combination of factors can be used. Such authentication system leverages the information of the user that are available from the federated identity management system.
Biometric Identification and Security
User Authentication and Security Systems
Advanced Steganography and Watermarking Techniques
Fingerprinting schemes are technical means to discourage people from illegally redistributing the digital data they have legally purchased. These schemes enable the original merchant to identify the original users of the digital data. Anonymous fingerprinting schemes allow a seller to fingerprint information sold to a user without knowing the identity of the user and without the seller seeing the fingerprinted copy. Finding a (redistributed) fingerprinted copy enables the seller to find out and prove to third party whose copy it was. In this paper, we propose a new scheme of anonymous fingerprinting by using electronic wallet, in which, the user doesn't need making a computationally expensive zero-knowledge proof on finding a fingerprinted copy, the seller can directly determine the redistributor by a simple computation without the help of a registration authority and without making a search for the redistributor's public key in purchase record. In addition, our scheme can prevent the collusion of merchant and registration center to make false-accusation to honest users. By using electronic wallet, our scheme can be integrated with electronic payment system
2 source records
Advanced Steganography and Watermarking Techniques
Traditional design of authenticated key exchange protocol considers communication security, but seldom takes into account the security threat of server compromises. Whenever an authentication server is captured, the intruder can immediately masquerade as legitimate users to successfully log into the system. Although some zero-knowledge-proof methods were designed to relieve this threat, their computation is relatively high due to computationally heavy modular exponentiations employed. A dynamic-verifier based authenticated key exchange protocol is proposed, where the server stores a dynamically changing password-verifier and no password leakage would occur even when the server’s verifier database is stolen. DV-AKE is especially useful for applications where lightweight client is required or lower server computational load is preferred.
In line with the recent call for technology on Image Based Authentication (IBA) in JPEG committee [1], we present a novel graphical password design in this paper. It rests on the human cognitive ability of association-based memorization to make the authentication more user-friendly, comparing with traditional textual password. Based on the principle of zero-knowledge proof protocol, we further improve our primary design to overcome the shoulder-surfing attack issue without adding any extra complexity into the authentication procedure. System performance analysis and comparisons are presented to support our proposals.
User Authentication and Security Systems
Advanced Steganography and Watermarking Techniques
Esoteric protocols, such as electronic cash, electronic voting and selective disclosure protocols, use special message constructors that are not widely used in other types of protocols (for example, in authentication protocols). These message constructors include blind signatures, commitments and zero-knowledge proofs. Furthermore, a standard formalization of the Dolev-Yao intruder [6] does not take into account these message constructors, nor does it consider some types of attacks (such as privacy attacks, brute-force dictionary attacks and known-plaintext attacks) that esoteric as well as other types of protocols are designed to protect against. This paper aims to present an extension of typed MSR [3, 4] in order to formally specify the needed message constructors, as well as the capabilities of a Dolev-Yao intruder designed to attack esoteric protocols.
J. Hammell, André Weimerskirch, J. Girão, Dirk Westhoff
This paper formally defines recognition as a new security principle closely related to authentication. Low-power sensor networks with no pre-deployment information require the less authoritative security of recognition. We give general properties of recognition protocols based on the method of key disclosure. We examine previously proposed low-power protocols according to the environment and security model presented. Finally, we give measurements from an implementation of a recognition protocol called zero common-knowledge and discuss how well this proof-of-concept satisfies the properties of the environment.
Recently, two generic watermarking protocols were proposed, based on a popular zero-knowledge identification protocol. In this paper, we show that both protocols are flawed and therefore fail to achieve their purpose of allowing a prover to prove to a verifier of his ownership of a watermarked image. We also give some suggestions to fix these flaws.
2 source records
Advanced Steganography and Watermarking Techniques
Gustavo A. Santana Torrellas, Andrés Tamayo Domínguez
Businesses are deploying Public Key Infrastructures (PKIs) to support internal business processes, implement virtual private networks, and secure corporate assets. The ability to establish business relations inside the company as well as with other companies in a secure way is important for the operability of business in today's world; corporate PKIs may implement different architectures, security policies, and cryptographic suites in order to accomplish this goal. But communication beyond the PKI is established with other companies based on a trust relationship (B2B), which brings vulnerability provided by PKIs from different companies. A flexible mechanism is needed to link these corporate PKIs and translate corporate relationships with security mechanisms and policies. This is accomplished through a Password Authentication Protocol (PAK), which provides means to authenticate or validate users across Bridge Certification Authorities (BCA), where certificates authorities (CA) are limited and cannot reach over to the other side of the BCA. In such a way, PAK can guarantee authentication of end points without modifying the original PKI structure of companies and offer flexibility in the process of implementation. Additional to this, there are several other issues that must be solved; such as the ability to connect different company PKI without compromising any sensible information that might cause a conflict of commercial interests and still guarantee a certain level of security through an accreditation and validation of the parties in order to be certain with whom we are doing business. In order to achieve accreditation and validation of PKIs and not expose any sensible information that could compromise either parties, we also based our work on a zero-knowledge security protocol, letting each PKI continue with their security policies without having to adjust to specific needs, achieving a better security level of commercial transactions through such hardening process.
A new framework is proposed for the analysis of communication protocols that require accountability, such as those for electronic commerce. Informal arguments are presented to show that a heretofore un-explored property "provability" is pertinent to examine the potential use of communication protocols in the context of litigation, and in the context of audit. A set of postulates which are applicable to the analysis of proofs in general (e.g., zero knowledge proofs), and the proofs of accountability in particular, are proposed. The proposed approach is more natural for the analysis of accountability then the existing belief logics that have been used in the past for the analysis of key distribution protocols. Some recently proposed protocols for electronic commerce and public-key delegation are analyzed to illustrate the use of the new analysis framework in detecting (and suggesting remedies for eliminating) their lack of accountability, and in detecting and eliminating redundancies.>
We suggest a systematic way to design secure password-based authentication protocols, which is the password verifier model. The method makes use of zero-knowledge interactive proof (ZKIP), which has been known not to be useful for the protection of passwords. For the proper usage of ZKIP, we introduce a specialized form of ZKIP, which has a secret coin tossing stage.
We consider the problem of designing an efficient oblivious transfer (OT) protocol that is provably secure in a concurrent setting, i.e., where many OT sessions may be running concurrently with their messages interleaved arbitrarily. Known OT protocols use zero-knowledge proofs, and no concurrent zero-knowledge proofs are known that use less than a poly-logarithmic number of rounds (at least without requiring a pre-processing phase, a public random string, an auxiliary string, timing constraints, or pre-distributed public keys). We introduce a model for proving security of concurrent OT protocols, and present a protocol that is proven secure in this model based on the decisional Diffie-Hellman problem. The protocol is efficient, requiring only a slightly non-constant number of rounds.