Multidevice Authentication with Strong Privacy Protection

Research Article Multidevice Authentication with Strong Privacy Protection Jan Hajny , Petr Dzurenda, and Lukas Malina Brno University of Technology, Czech Republic Correspondence should be addressed to Jan Hajny; [email protected] Received 12 April 2018; Revised 20 June 2018; Accepted 3 July 2018; Published 29 July 2018 Academic Editor: Kim-Kwang Raymond Choo Copyright © 2018 Jan Hajny et al. This is an open access article distributed under the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited. Card-based physical access control systems are used by most people on a daily basis, for example, at work, in public transportation, or at hotels. Yet these systems have often very poor cryptographic protection. User identifiers and keys can be easily eavesdropped on and counterfeited. The privacy-preserving features are almost missing in these systems. To improve this state, we propose a novel cryptographic scheme based on efficient zero-knowledge proofs and Boneh-Boyen signatures. The proposed scheme is provably secure and provides the full set of privacy-enhancing features, that is, the anonymity, untraceability, and unlinkability of users. Furthermore, our scheme supports distributed multidevice authentication with multiple RFID (Radio-Frequency IDentification) user devices. This feature is particularly important in applications for controlling access to dangerous sites where the presence of protective equipment is checked during each access control session. Besides the full cryptographic specification, we also show the results of our implementation on devices commonly used in access control applications, particularly the smart cards and embedded verification terminals. By avoiding costly operations on user devices, such as bilinear pairings, we were able to achieve times comparable to existing systems (around 500 ms), while providing significantly higher security, privacy protection, and features for RFID multidevice authentication. 1. Introduction Privacy-enhancing technologies constitute a significant part of contemporary cryptography. Modern cryptographic protocols allow privacy-enhanced storing of sensitive data and its processing by cloud services, private information retrieval, or, for example, authentication based on personal attributes, instead of user identifiers. The increasing intensity of research into privacy is supported by national programs and strategies, in particular in USA [1] and EU [2]. While most of the novel schemes are aimed at electronic services, the domain of physical access control is rather neglected. We still use traditional locks, tourniquets, and classical cardbased access control mechanisms to manage physical access to our premises. But with the increasing computational power of the programmable smart cards, massive expansion of various personal electronic devices, and the capabilities in RFID communication of our smart phones, we can expect penetration of privacy-enhancing technologies also to the area of physical access control. In particular, in mass applications like public transportation, e-ticketing, e-passports, and eIDs, the benefits of controlling physical access using electronic devices with advanced cryptographic protocols are very appealing. In this paper, we propose and experimentally evaluate a novel cryptographic scheme that particularly addresses two phenomenons of contemporary cyberspace: lack of user privacy and ubiquitous presence of many personal devices (phones, smart cards, RFID tags, bluetooth dongles, smart watch, etc.) that can be leveraged for stronger authentication and more reliable access control. In particular, we focus on safety applications in which the users wear multiple safety equipment, such as helmets, harnesses, boots, and protective suits, each with attached programmable RFID tag capable of wireless communication. A user is granted access to (potentially dangerous) premises only if all his equipment is present. In existing systems, the presence of the protective equipment is checked simply by scanning the identifiers using RFID readers. Such an approach is neither secure (identifiers can be counterfeited), nor privacy friendly (identifiers can be traced, behavioral profiles can be created, etc.). Hindawi Wireless Communications and Mobile Computing Volume 2018, Article ID 3295148, 12 pages https://doi.org/10.1155/2018/3295148 2 Wireless Communications and Mobile Computing We propose a novel cryptographic scheme for multidevice authentication that is tailored for physical access control systemswheretheusermustprovenotonlyhisownidentifier, but also many other auxiliary identifiers stored on separate devices. In addition, the authentication sessions must support all the key privacy-enhancing features; i.e., the access control process must be anonymous (i.e., a user must prove that he belongs to a group of authorized users, but without releasing his concrete identity), unlinkable (all the sessions of a single user cannot be linkable to a profile), and untraceable (system administrators must be unable to trace honest users in the system). On the other side, the scheme must provide efficient means for revocation and identification of malicious users. In our cryptographic system, we provide all the required features that are often contradictory and completely unavailable in existing schemes (in particular, the presence of many identifiers versus anonymity; the untraceability and strong cryptographic security versus efficiency on RFID tags and stickers). In our scheme, users can be granted access to premises upon proving the presence of particular devices in their proximity (e.g., the safety equipment) or personal attributes (age, membership, citizenship, etc.). The access control process may (the extent of privacy-enhancing features can be initially set by the administrator; if required, identification or user tracing may be enforced by the access control system) proceed in a fully private manner, without disclosing user identity or being traceable in the system. 2. Related Work Most of the existing practical physical access control systems arebasedonthefollowingtechnologies:NXP’sMifareand DESfire; HID’s Prox and iClass; and Legic Prime and Advant. NXP’s Mifare Classic, introduced in 1994, is a very popular technology used in physical access control systems. Although very old and insecure, the technology is still used in many applications, even those security sensitive. The authentication protocol is based on a unique 4B card identifier UID. In some implementations, the card just reveals UID to the terminal without any authentication protocol. In that case, UID can be easily eavesdropped on and used by an attacker for impersonation. In other implementations, a simple authentication protocol is used but is considered insecure due to many existing practical attacks [3–5] on the encryption algorithm CRYPTO1. The insufficient security of the CRYPTO1 algorithm used in the Mifare Classic made NXP improve the cryptographic protection and release Mifare DESFire. The old encryption algorithm was replaced by 3DES algorithm. The authentication protocol was further improved in Mifare DESFire EV1 which supports the AES encryption algorithm [6]. The protocol itself remained without any major changes. However, even Mifare DESFire was successfully attacked, althoughtheattacks[7,8]wereaimedontheimplementation, not cryptographic weaknesses. The HID Prox technology contains no cryptographic protection. HID iClass employs an authentication protocol based on the 3DES algorithm, but attacks on this protocol are available [9]. Legic Prime has weak proprietary cryptographic protection [10]. Legic Advant is protected by symmetric block algorithms (DES [11], 3DES,andAES).Noneofthemajorcommercialtechnologies provide any protection of privacy. With the introduction of the first attribute-based credential schemes, such as the Idemix [12], U-Prove [13], and HM12 [14], the variants for physical access control systems also started to appear. The U-Prove scheme was implemented on Multos smart cards [15]. The user is able to prove his attribute in less than 1 s using this implementation. However, the unlinkability property cannot be provided by the cryptographic design of the protocol. The Idemix was also implemented on the Multos smart card platform, with cca 1 s needed to generate the attribute proof. The pilot implementation of the HM12 scheme using Multos ML3 smart cards [16] required around 2.4 s in total to generate and verify the proof, including the communication overhead. No testing was done on multiple devices because the distributed proof is not supported by these schemes. Many types of personal and wearable devices forming the so-called Internet of Things (IoT) have appeared recently. Authentication issues have been solved by different techniques on these devises. Xu and Weitao propose biometric authentication using wearables with face recognition using smart-glass and gait recognition using smart watch. Riva et al. [17] combine multiple sources of authentication data, which is close to our approach. However, all these schemes are using mainly biometric authentication factors. Cha et al. [18] present a simple model for two-device authentication for micropayment systems using mobile and wearable devices. Nevertheless, their proposal lacks details and concrete cryptographic functions. Butun et al. [19] address multilevel authentication issue in cloud computing. Gonzalez-Manzano et al. [20] present an access control mechanism for cloudbased storage service access by using a set of devices. However, their scheme is based on symmetric cryptography andthusdoesnotprovidenonrepudiation.Hajnyetal.[21] use many wearable and IoT devices to do the authentication process. However, the scheme misses privacy-enhancing properties, because each user is uniquely represented by his/her public key. In summary, there are several authentication solutions that involve IoT devices. However, there are only very few papers focusing on multidevice authentication. Currently, none of the proposals is provably secure and supports the privacy-enhancing features. Furthermore, most of the schemes remain only theoretic. 2.1. Our Contribution. The cryptographic scheme presented in this paper takes a novel approach for the access control based on rather the presence of multiple devices in user’s proximity than the direct verification of user identifiers. The novel approach has two key benefits: it significantly improves the privacy protection of users and allows the authentication based on the presence of many low-performance devices. Our scheme is the first practical proposal with implementation results that combines strong security, all standard privacyenhancing features, and efficiency. Wireless Communications and Mobile Computing 3 Figure 1: Schnorr’s proof of knowledge of discrete logarithm PK {𝑤 : 𝑐 = 𝑔𝑤}in Z∗ 𝑝. (i) Provable security:allalgorithmsareprovablysecure, based on primitives with rigorous formal proofs. (ii) Multidevice authentication: the scheme allows user authentication based on the presence of many personal devices. (iii) Anonymity: the scheme allows authentication based on anonymous proofs of knowledge of private user and/or device identifiers. (iv) Unlinkability: the scheme prevents creating user behavior profiles based on the authentication sessions linking. (v) Untraceability: the scheme prevents any entity from tracing users (or their devices). (vi) Efficiency: the authentication protocol is fast on constrained user devices (i.e., smart cards) and embedded verification terminals. (vii) Revocation and identification: the proposed scheme is compatible with major revocation and identification schemes [22–24] for attribute-based credentials. We not only provide the cryptographic description and securityproofsofourscheme,butalsoprovidepractical implementation results based on benchmarks on RFID devices and an embedded hardware terminal. These results prove that the scheme can be practically implemented on existing off-the-shelf devices. 3. Preliminaries 3.1. Notation. We describe proof of knowledge protocols (PK) using the efficient notation introduced by Camenisch andStadler[25].Theprotocolforprovingtheknowledgeof discrete logarithm of 𝑐with respect to 𝑔is denoted as PK{𝛼 : 𝑐=𝑔 𝛼}. The symbol “:” means “such that” and “|𝑥|”isthebit length of 𝑥.Wewrite𝑎$ ←󳨀𝐴when 𝑎is sampled uniformly at random from 𝐴. A secure hash function is denoted as H. 3.2. Proofs of Knowledge. The statements about discrete logarithms in prime order groups can be easily proven using the Σ-protocols [26]. A simple yet very useful protocol for proving the discrete logarithm knowledge is based on the Schnorr signature scheme [27]. Using this protocol, the prover proves his knowledge of a discrete logarithm with respect to public parameters 𝑐,𝑔,𝑝,𝑞; i.e., he proves the knowledge of 𝑤:𝑐= 𝑔𝑤mod 𝑝,where𝑝is prime modulus, 𝑞is group order, and 𝑔 is Z∗ 𝑝generator. The protocol is depicted in Figure 1. The proof of discrete logarithm knowledge is a simple 3way protocol where the prover commits to a random number 𝑟in the first step, receives a challenge 𝑒in the second step, and responds by 𝑧to the challenge in the third step. The protocol is Honest Verifier Zero-Knowledge (HVZK). Note that the verifier does not have to know the private input 𝑤 oftheprovertobeabletoverifyitsknowledge.Werecallthe properties of the protocol below. Proof. Completeness:proverwhoknows𝑤is always accepted: 𝑐=𝑔 𝑧𝑐𝑒=𝑔 𝑟−𝑒𝑤𝑔𝑒𝑤 =𝑔 𝑟𝑔−𝑒𝑤𝑔𝑒𝑤 =𝑔 𝑟= 𝑐. Proof. Soundness: let us assume a cheating prover is ready to answer at least 2 random challenges 𝑒,𝑒󸀠after committing to 𝑟without knowing 𝑤.Then,hisresponses𝑧,𝑧󸀠must be accepted in verifier’s checks: 𝑐=𝑔 𝑧𝑐𝑒,(1) 𝑐=𝑔 𝑧󸀠𝑐𝑒󸀠,(2) we divide (1) and (2) and get 𝑐 𝑐=𝑔𝑧𝑐𝑒 𝑔𝑧󸀠𝑐𝑒󸀠⇐⇒ 1=𝑔 𝑧−𝑧󸀠𝑐𝑒−𝑒󸀠, (3) after multiplying both sides of (3) by 𝑔−(𝑧−𝑧󸀠)and raising to the power of (𝑒− 𝑒󸀠)−1,weget 𝑔(𝑧󸀠−𝑧)(𝑒−𝑒󸀠)−1 =𝑐 (4) andwegetthediscretelogarithm𝑤=(𝑧 󸀠−𝑧)(𝑒−𝑒 󸀠)−1 that is easy to efficiently compute for the dishonest prover; thus we reached the contradiction because the cheating prover unaware of 𝑤was assumed. Proof. Honest Verifier Zero-Knowledge: the ZK property is proven by proving the existence of the following ZK simulator 𝑀∗ 𝑉: 4 Wireless Communications and Mobile Computing (1) the simulator randomly chooses the response 𝑧󸀠$ ←󳨀 Z𝑞. (2) the simulator randomly chooses 𝑒󸀠$ ←󳨀 Z𝑞. (3) the simulator computes 𝑐󸀠=𝑔 𝑧󸀠𝑐𝑒󸀠. The 𝑀∗ 𝑉’s output 𝑐󸀠,𝑒󸀠,𝑧󸀠is computationally indistinguishable from the real protocol output 𝑐,𝑒,𝑧. The protocol for proving the knowledge of a discrete logarithm described above can be extended to the discrete logarithm representation proof and discrete logarithm equivalence proof [25]. The principles and security proofs remain the same. 3.3. Bilinear Pairing. Let G1,G2,andG𝑇be groups of prime order 𝑞.Abilinearmape:G1×G2󳨀→ G𝑇is a map which satisfies bilinearity, i.e., e(𝑔𝑥 1,𝑔𝑦 2)=e(𝑔1,𝑔2)𝑥𝑦 for all 𝑥,𝑦 ∈ Z𝑞; nondegeneracy, i.e., for all generators 𝑔1∈G1and 𝑔2∈ G2,e(𝑔1,𝑔2)generates G𝑇; and efficiency, i.e., there exists an efficient algorithm G(1𝑘)that outputs the bilinear group (𝑞,G1,G2,G𝑇,e,𝑔1,𝑔2). The pairing is a bilinear map and it is symmetric if G1=G2.Therearemanytypesofpairings; however only Weil, Tate, Ate, and Eta parings are mainly used in cryptography due to their efficient computation. Our scheme makes use of the Tate pairing [28], since it is the fastest among them. Most of the known parings uses Millers algorithm[29]todocomputationsonellipticcurves. 3.4. Weak Boneh-Boyen Signature. The weak Boneh-Boyen (wBB) signature scheme [30] can be used to efficiently sign (blocks of) messages. Furthermore, the signature scheme canbeeasilyintegratedwiththezero-knowledgeproofs so that the knowledge of signed messages (and signatures themselves) can be proven anonymously, unlinkably, and untraceably.Werecallthesigningandverificationalgorithms below; the efficient proofs of knowledge are described, e.g., in [24]. Setup:Oninputsecurityparameter𝑘, generate a bilinear group (𝑞,G1,G2,G𝑇,e,𝑔1,𝑔2)←󳨀G(1𝑘).Take𝑠𝑘 $ ←󳨀 Z𝑞, compute 𝑝𝑘=𝑔 𝑠𝑘 2,andoutput𝑠𝑘 as private key and 𝑝𝑘 = (𝑞,G1,G2,G𝑇,𝑔1,𝑔2,e,𝑝𝑘)as public key. Sign:Oninputmessage𝑚∈Z𝑞and secret key 𝑠𝑘,output 𝜎=𝑔 1/(𝑠𝑘+𝑚) 1. Verify:Oninputthesignature𝜎,message𝑚,andpublic key 𝑝𝑘,output1iffe(𝜎,𝑝𝑘) ⋅e(𝜎𝑚,𝑔2)=e(𝑔1,𝑔2)holds. Showing the constant signature 𝜎multiple times would make the authentication protocol linkable. All user sessions wouldbelinkabletoasingleprofile,whichwouldmakethe resulting scheme very privacy unfriendly. To avoid linkability of signatures, users can only prove the knowledge of a valid signature by using the proof defined in [24]. In this proof, the user chooses a random value 𝑟$ ←󳨀 Z𝑞and computes randomized auxiliary values 𝜎󸀠=𝜎 𝑟and 𝜎=𝜎 󸀠−𝑚𝑔𝑟 1.Then, the knowledge of a signature is proven by constructing the zero-knowledge proof 𝜋 = 𝑃𝐾{(𝑚,𝑟) : 𝜎=𝜎 󸀠−𝑚𝑔𝑟 1}and verifying e(𝜎,𝑔2)=e(𝜎󸀠,𝑝𝑘). The verifier is convinced that the user indeed knows a valid signature on a known message, although the proof does not release any of these values. That construction is perfect for our scheme, because the users want to convince verifiers that they know (device) identifiers signed by registrars, in an anonymous, untraceable, and unlinkable manner. The wBB signatures were proven existentially unforgeable against a weak (nonadaptive) chosen message attack under the 𝑞-SDH assumption [30]. 4. Multidevice Authentication with Privacy Protection First, we define the formal requirements on the authentication scheme. Next, we define the algorithms and entities in the scheme. Finally, we present the concrete instantiation of the privacy-enhanced multidevice authentication scheme based on the wBB signatures described in the previous section. 4.1. Requirements. We require the scheme to be secure, private, and efficient. Security Requirements Completeness: registered users must be accepted by the Authenticate protocol. Soundness: unregistered users must be rejected by the Authenticate protocol. Zero-Knowledge:theAuthenticate protocol transcript must be simulatable without the knowledge of identifiers, thus provably releasing no sensitive information. Privacy Requirements Anonymity: users must be able to prove the knowledge of their identifiers anonymously, without disclosing them. Untraceability: user authentication sessions must be untraceable by all system entities, including registrars. Unlinkability: all single user’s authentication sessions must be mutually unlinkable. Efficiency Requirements Readiness for RFID devices: the scheme must be fast on constrained devices, in particular smart cards. No operations, that are unavailable on RFID devices (such as bilinear pairings), can be used in user’s algorithms. 4.2. Definition of Algorithms. We define the algorithms and protocols of our scheme in this section. The communication pattern is depicted in Figure 2 and employs the registrar (i.e., a central server that manages users and their equipment), users (i.e., user devices such as smart cards or smart phones), terminals (i.e., embedded devices with RFID readers typically attached next to doors), and tags (i.e., devices that need to be present during authentication and access control, typically Wireless Communications and Mobile Computing 5 Registrar User Terminal Device i Device i Tag i Register Register AuthenticateAuthenticate Setup Keygen 0/1 Figure 2: Architecture of multidevice authentication with privacy protection. safetyequipmentwithprogrammableRFIDsticks,suchasthe helmet, respirator, or harness). (𝑝𝑎𝑟) ←󳨀 Setup(1𝑘,𝑛): the algorithm is run by the registrar. It inputs the security parameter 𝑘and the maximum number of tag classes (i.e., helmets, harnesses, boots, etc.). The algorithm outputs the public system parameters 𝑝𝑎𝑟. (𝑠𝑘𝑟,𝑝𝑘𝑟)←󳨀Keygen(𝑝𝑎𝑟):thealgorithmisrunby the registrar. On the input of public system parameters 𝑝𝑎𝑟, it generates its private key 𝑠𝑘𝑟and public key 𝑝𝑘𝑟. The registrar distributes the public key to all other entities.(⟨𝐼𝐷𝑖,𝜎𝑖⟩𝑛 𝑖=1,𝐼𝐷𝑢,𝜎𝑢)←󳨀Register(𝑝𝑎𝑟,𝑠𝑘𝑟,𝑝𝑘𝑟):the algorithm is run by the registrar. On the input of system parameters and its keypair, the registrar generates the tags’ identifiers 𝐼𝐷𝑖with corresponding signatures 𝜎𝑖and user’s identifier 𝐼𝐷𝑢with a corresponding signature 𝜎𝑢.Thetag identifiers and signatures are securely delivered to tags and the user identifier and signature are delivered securely to the user device. (0/1) ←󳨀 Authenticate(𝑝𝑎𝑟,⟨𝐼𝐷𝑖,𝜎𝑖⟩𝑛 𝑖=1,𝐼𝐷𝑢,𝜎𝑢, 𝑝𝑘𝑟): the cryptographic protocol is run jointly by the user device, tags, and the terminal. It inputs system parameters, registrar’s public key, private identifiers, and corresponding signatures and returns 1 iff signatures and IDs are valid, or 0 otherwise. 4.3. Instantiation Using wBB Signatures. In this section, we present the concrete instantiations of cryptographic algorithmsdefinedinSection4.2.WeusethewBBsignature scheme to certify the identifiers of tags and users in the Register algorithm and interactive proofs of knowledge to prove the knowledge of respective signatures and identifiers in the Authenticate protocol.WeusetheCamenischStadlernotation[25]todescribetheproofofknowledge protocols. Setup. The algorithm inputs the security parameter 𝑘and the maximum number of tag classes 𝑛. It generates the bilinear group with parameters 𝑝𝑎𝑟 = (𝑞,G1,G2,G𝑇, e,𝑔1,...,𝑔𝑛,𝑔𝑢∈G1,𝑔2∈G2)satisfying |𝑞| = 𝑘. Keygen. The algorithm inputs the public parameters 𝑝𝑎𝑟, selects random registrar’s private keys 𝑠𝑘𝑟=(𝑠𝑘 0,𝑠𝑘1, ...,𝑠𝑘𝑛,𝑠𝑘𝑢)$ ←󳨀 Z∗ 𝑞,andcomputesthepublickeys𝑝𝑘𝑟= (𝑝𝑘0=𝑔 𝑠𝑘0 2,𝑝𝑘1=𝑔 𝑠𝑘1 2,...,𝑝𝑘𝑛=𝑔 𝑠𝑘𝑛 2,𝑝𝑘𝑢=𝑔 𝑠𝑘𝑢 2).It outputs the private keys as registrar’s private output and the public key as the public output. Register. The algorithm inputs the registrar’s keys and public parameters, randomly selects tag and user identifiers (𝐼𝐷1,...,𝐼𝐷𝑛,𝐼𝐷𝑢)$ ←󳨀 Z𝑞, and computes the wBB signatures (𝜎1,...,𝜎𝑛)on tag identifiers (𝐼𝐷1,...,𝐼𝐷𝑛)andtheaggregated user signature 𝜎𝑢and auxiliary values ⟨𝜎𝑢𝑖,𝜎−𝐼𝐷𝑖 𝑢𝑖⟩𝑛 𝑖=1, 𝜎𝑢𝑢,𝜎−𝐼𝐷𝑢 𝑢𝑢that allow the construction of efficient proofs of knowledge in the Authenticate protocol.Thealgorithm outputs the tag identifiers and corresponding signatures as a private output to tags. The user identifier, the aggregated signature, and auxiliary values are outputted to the user as a private output. Both tags and the user receive the initial 𝑠𝑒𝑒𝑑 required for the synchronization of the zero-knowledge proofs as a private input. The algorithm is depicted in Figure 3. Authenticate.Authenticate is an algorithm distributed among the user, terminal, and tags that inputs the identifiers and respective signatures and outputs 1 iff (1) all signatures are valid and created by the registrar and (2) all identifiers of the user are present and signed. Otherwise it outputs 0. The protocol is a distributed proof of knowledge of wBB signatures where the tags prove that they know their identifiers and corresponding signatures (without actually revealing them) and, at the same time, the user proves that hehasanaggregatedsignatureonallhistagidentifiers, plus his own identifier. As the user does not know the tag identifiers, all tags must be present and participate on the proof construction. As a result, the user is able to anonymously, untraceably, and unlinkably prove his valid registration by the registrar and the presence of all his tags,i.e.,thesafetyequipment.Theprotocolisdepictedin abstract CS notation in Figure 4. We also provide the full description in Figure 5 in Section 6 focused on implementation. 5. Security Analysis The registrar issues the wBB signatures to tags and users in the Register algorithm. Then, the user and tags prove 6 Wireless Communications and Mobile Computing Figure 3: Register protocol. Figure 4: Authenticate protocol in CS notation. Wireless Communications and Mobile Computing 7 Figure 5: Authenticate protocol in full notation for 𝑖𝑡ℎ tag. Tag i RFID Tag 1 RFID Tag 2 RFID Tag n RFID Terminal PC Raspberry Pi NFC/BLE User Device Smartphone Smart Card Smart watch . . . Figure 6: Tested scenario. the knowledge of such signatures to the terminal using the distributed zero-knowledge proofs in the Authenticate protocol. Lemma 1. The weak Boneh-Boyen signatures are unforgeable against a weak chosen message attack under the 𝑞-Static DiffieHellman assumption [30]. Lemma 1 is proven in [30]. Lemma 2. The protocol presented in Figure 5 is complete, sound, and zero-knowledge. We construct the proof for a tag 𝑖using the standard proving technique for zero-knowledge protocols. For other 8 Wireless Communications and Mobile Computing devices and the user, the proof is constructed analogically. Proof. Completeness: honest users pass the terminal’s check. 𝑡𝑖=𝑔 𝑠𝑟𝑖 𝑖𝜎󸀠𝑠𝐼𝐷𝑖 𝑖𝜎𝑖−𝑐 (5) =𝑔 𝜌𝑟𝑖 𝑖𝑔𝑐𝑟𝑖 𝑖𝜎𝑟𝑖𝑠𝐼𝐷𝑖 𝑖𝜎󸀠𝐼𝐷𝑖𝑐 𝑖𝑔−𝑐𝑟𝑖 𝑖(6) =𝑔 𝜌𝑟𝑖 𝑖𝑔𝑐𝑟𝑖 𝑖𝜎𝑟𝑖𝜌𝐼𝐷𝑖 𝑖𝜎−𝑟𝑖𝑐𝐼𝐷𝑖 𝑖𝜎𝑟𝑖𝐼𝐷𝑖𝑐 𝑖𝑔−𝑐𝑟𝑖 𝑖(7) =𝑔 𝜌𝑟𝑖 𝑖𝜎󸀠𝜌𝐼𝐷𝑖 𝑖(8) e(𝜎𝑖,𝑔2)=e(𝜎󸀠 𝑖,𝑝𝑘0)(9) e(𝜎−𝐼𝐷𝑖𝑟𝑖 𝑖𝑔𝑟𝑖 𝑖,𝑔2)=e(𝜎󸀠 𝑖,𝑔𝑠𝑘0 2)(10) e(𝑔(−𝐼𝐷𝑖𝑟𝑖+𝑟𝑖(𝑠𝑘𝑜+𝐼𝐷𝑖))/(𝑠𝑘0+𝐼𝐷𝑖) 𝑖,𝑔2)=e(𝜎󸀠 𝑖,𝑔𝑠𝑘0 2)(11) e(𝑔𝑟𝑖𝑠𝑘𝑜/(𝑠𝑘0+𝐼𝐷𝑖) 𝑖,𝑔2)=e(𝜎󸀠 𝑖,𝑔𝑠𝑘0 2)(12) e(𝜎󸀠𝑠𝑘0 𝑖,𝑔2)=e(𝜎󸀠 𝑖,𝑔𝑠𝑘0 2)(13) Error Probability. If implemented correctly, the user will be always accepted. Proof. Soundness: only registered users pass terminal’s check. Assume a user who is not registered (i.e., does not know the identifier 𝐼𝐷𝑖) and passes the terminal’s check for two different challenges 𝑐and 𝑐󸀠with two different responses 𝑠 and 𝑠󸀠: 𝑡𝑖=𝑔 𝑠𝑟𝑖 𝑖𝜎󸀠𝑠𝐼𝐷𝑖 𝑖𝜎𝑖−𝑐 (14) 𝑡𝑖=𝑔 𝑠󸀠 𝑟𝑖 𝑖𝜎󸀠𝑠󸀠 𝐼𝐷𝑖 𝑖𝜎𝑖−𝑐󸀠(15) and we get 𝜎𝑖𝑐−𝑐󸀠=𝑔 𝑠𝑟𝑖−𝑠󸀠 𝑟𝑖 𝑖𝜎󸀠𝑠𝐼𝐷𝑖−𝑠󸀠 𝐼𝐷𝑖 𝑖(16) and therefore 𝜎𝑖=𝑔 (𝑠𝑟𝑖−𝑠󸀠 𝑟𝑖)/(𝑐−𝑐󸀠) 𝑖𝜎󸀠(𝑠𝐼𝐷𝑖−𝑠󸀠 𝐼𝐷𝑖)/(𝑐−𝑐󸀠) 𝑖(17) Thus the user can efficiently compute both the randomizer 𝑟𝑖=(𝑠 𝑟𝑖−𝑠 󸀠 𝑟𝑖)/(𝑐 − 𝑐󸀠)and the identifier 𝐼𝐷𝑖=(𝑠 𝐼𝐷𝑖 − 𝑠󸀠 𝐼𝐷𝑖)/(𝑐−𝑐󸀠)andwereachedthecontradictiontoouroriginal assumption. Error Probability. The attacker will pass the verification check if he can predict the challenge 𝑐. The probability of soundness error is thus 𝑃=2 −|𝑐| =2 −𝑞 =2 −224, which is negligible. With an expected rate of 100 ms per challenge, the expected time of breach is 4×1058 years. Proof. Zero-Knowledge: the protocol releases no private information, i.e., there exists a zero-knowledge simulator 𝑀∗ 𝑉. Using the public parameters and the public key (𝑔,𝑔𝑥)(we follow the proof presented in [24] that allows the simulator to input an auxiliary public key (𝑔,𝑔𝑥):𝑔$ ←󳨀 Z𝑞from the registrar), the simulator chooses randomly and uniformly (𝑠𝑟𝑖,𝑠𝐼𝐷𝑖,𝑟,𝑐) $ ←󳨀 Z𝑞,computes𝜎󸀠 𝑖= 𝑔𝑟,𝜎𝑖=(𝑔𝑥)𝑟,𝑡𝑖= 𝑔𝑠𝑟𝑖 𝑖𝜎󸀠𝑠𝐼𝐷𝑖 𝑖𝜎𝑖−𝑐,andoutputstheproof𝜋=(𝜎𝑖,𝜎󸀠 𝑖,𝑡𝑖,H(𝑟),𝑐, (𝑠𝑟𝑖,𝑠𝐼𝐷𝑖)). The simulated transcript is computationally indistinguishable from the real run of the protocol. Error Probability. The attacker can try to guess the randomizers 𝑟𝑖,𝜌 𝑟𝑖,𝑟𝑢,𝜌 𝑟𝑢andbreakthediscretelogarithmassumption. The probability is 𝑃=2 −𝑞 =2 −224 for each device, which is negligible. With an expected rate of 10 ms per computing the guess (the exponentiation), the expected time of breach is 4×1057 years. As a result of the zero-knowledge property and randomization of all signatures, the protocol is also anonymous, untraceable, and unlinkable. 6. Implementation Aspects The Authenticate protocol has been implemented as a standard 3-way interactive zero-knowledge proof of knowledge protocol described in Section 3.2. We use a parallel composition with one challenge and one response for all tags of a user to construct an AND proof for both tag and user signatures. The Authenticate protocol for 𝑖𝑡ℎ tag is fully specified in Figure 5. To keep user devices synchronized, we use a counter that is initialized by a seed generated by the registrar. In the beginning of each session, the counter increments. To avoid losing synchronization, the hashed counter is broadcasted by the terminal so that the devices can compare it with their actual counter value (and with, e.g., 10 next precomputed values) and sync in case their counter is behind. The hashed counter also serves as the session identifier and thus is present in all three steps of the protocol. In the first step of the protocol, the tag generates randomizers 𝑟𝑖,𝜌 𝑟𝑖,𝜌 𝐼𝐷𝑖,computesrandomizedsignatures𝜎󸀠 𝑖,𝜎𝑖,and computes the commitment to randomizers 𝑡𝑖.Therandomized signatures, commitment to randomizers, and hashed randomizers are sent to the terminal. In the second step, the terminal randomly selects its challenge 𝑐and sends it to all tags and devices, together with the obtained hash. In the third step, the tag computes their answers 𝑠𝑟𝑖,𝑠𝐼𝐷𝑖 of the zero-knowledge protocol. After receiving the answers, the terminal is able to verify thatthetagknowsavalidsignatureandacorrespondingtag identifier with respect to registrar’s public key 𝑝𝑘,without actually learning any useror tag-identifying values. The proof construction for the user is the same with the exception that the answers containing tag IDs are omitted, because the terminal makes use of the values received by Wireless Communications and Mobile Computing 9 12345 # of tags [-] MULTOS Card HUAWEI P9 Lite 2017 HUAWEI Watch 2 0 0,5 1 1,5 2 2,5 3 3,5 time [s] Figure 7: Dependence of the proof construction time on the number of user device. the devices. Instead of proving tag IDs, the user proves the knowledge of his own user ID. 6.1. Performance Analysis. The scheme was designed to be practical and fast on constrained RFID devices, such as smart cards and programmable RFID tags. Therefore, the bilinear pairings, which are the most computationally complex operations in our algorithm, are only computed in the terminal which normally has more resources than user device. The second most complex operation is the exponentiation (implemented as scalar multiplication of an elliptic-curve point) and itisreducedtoaminimum.Theuserdeviceneeds(5 + 2𝑑) exponentiations to construct a “user proof” with 𝑑personal tags. Each tag must compute 5exponentiations to generate a“tagproof”.However,ourimplementationusesonly4 exponentiations, since the value (𝜎𝑖−𝐼𝐷𝑖𝑔𝑖)is precomputed within a Register protocolandisusedfortherandomized signature 𝜎𝑖=𝜎 󸀠−𝐼𝐷𝑖 𝑖𝑔𝑟𝑖 𝑖=(𝜎 𝑖−𝐼𝐷𝑖𝑔𝑖)𝑟𝑖construction. The complexity of the other operations (random number generation, addition, and multiplication) are only minor, compared to pairings and exponentiations. In order to verify the proof, the terminal must compute (4+4𝑑)bilinear pairings and (4+3𝑑) exponentiations. We provide performance measurement of crucial operationsoncommondevices,whicharewidelyusedintheaccess control applications, i.e., a smart card, smart phone, smart watch (as user devices), and a custom-built RFID terminal with ARM or Intel CPU and programmable RFID tags (as RFID tags attached to safety equipment). The hardware and software specification of all the devices is presented in Table 1. The testing scenario is depicted in Figure 6. The user needstoholdawearabledevice,suchasasmartphone (HUAWEIP9Lite2017),asmartcard(MultosCard),orsmart watch (HUAWEI Watch 2) and some safety equipment, such as helmets, harnesses, boots, and protective suits, each of them with a programmable RFID tag attached. The tag is equipped with a programmable chip SC23Z018 with Multos 4.2 operation system. The proofs are collected and verified by a terminal. We use Raspberry Pi 3 to represent the terminal. In another scenario, PC (Intel i7-7700 CPU, 16 GB RAM) acts as a central authentication server representing the case of a centralized access control system. The system uses RFID communication between tags and a terminal, and NFC or BLE communication between a terminal and a user device. The performance of critical operations and the estimation of the running time of the Authenticate protocol with one RFID tag and one user device are presented in Table 2. In addition, we provide measurement of the selected devices where we consider different elliptic curves types, in particular type A and D. Both curves satisfy the NIST key recommendationfor80-bitsecuritystrength[31].Theperformanceis measured in milliseconds (the measurement of clock cycles is unavailable on the smart card platform) and the values are an average of 10 measurements, excluding communication overhead. For the implementation of EC operations, the PBC library was used [32] on the terminal and jPBC [33] library on Android devices. Native assembler code was used to perform operations on the Multos smart card. Theproposedauthenticationschemecanbeusedinmany types of access control scenarios and for different types of devices. Therefore, we provide the results of each protocol using one RFID tag. Furthermore, we present the crucial EC operations’ benchmarks on a wide range of devices in Table 3. The time is measured in milliseconds and the values are an average of 10 measurements, as in the previous case. All measurements were performed by using the elliptic curve d159 from the PBC library. We did not consider Android devices as a terminal device, since the pairing operation requires too much time and therefore it is not usable in practice. Figure 7 depicts the time required for a proof construction on different devices (Multos smart card, Android smart