Visible to the public Biblio

Filters: Keyword is radiofrequency identification  [Clear All Filters]
2020-03-23
Bothe, Alexander, Bauer, Jan, Aschenbruck, Nils.  2019.  RFID-assisted Continuous User Authentication for IoT-based Smart Farming. 2019 IEEE International Conference on RFID Technology and Applications (RFID-TA). :505–510.
Smart Farming is driven by the emergence of precise positioning systems and Internet of Things technologies which have already enabled site-specific applications, sustainable resource management, and interconnected machinery. Nowadays, so-called Farm Management Information Systems (FMISs) enable farm-internal interconnection of agricultural machines and implements and, thereby, allow in-field data exchange and the orchestration of collaborative agricultural processes. Machine data is often directly logged during task execution. Moreover, interconnection of farms, agricultural contractors, and marketplaces ease the collaboration. However, current FMISs lack in security and particularly in user authentication. In this paper, we present a security architecture for a decentralized, manufacturer-independent, and open-source FMIS. Special attention is turned on the Radio Frequency Identification (RFID)-based continuous user authentication which greatly improves security and credibility of automated documentation, while at the same time preserves usability in practice.
2020-03-02
Hofnăr, Aurel-Dragoş, Joldoş, Marius.  2019.  Host Oriented Factor Normalizing Authentication Resource: More Secure Authentication for Legacy Systems. 2019 IEEE 15th International Conference on Intelligent Computer Communication and Processing (ICCP). :1–6.
Whenever one accesses a computer system there are three essential security issues involved: identification, authentication and authorization. The identification process enables recognition of an entity, which may be either a human, a machine, or another asset - e.g. software program. Two complementary mechanisms are used for determining who can access those systems: authentication and authorization. To address the authentication process, various solutions have been proposed in the literature, from a simple password to newer technologies based on biometrics or RFID (Radio Frequency Identification). This paper presents a novel scalable multi-factor authentication method, applicable to computer systems with no need of any hardware/software changes.
2020-02-10
Ramu, Gandu, Mishra, Zeesha, Acharya, B..  2019.  Hardware implementation of Piccolo Encryption Algorithm for constrained RFID application. 2019 9th Annual Information Technology, Electromechanical Engineering and Microelectronics Conference (IEMECON). :85–89.
The deployment of smart devices in IoT applications are increasing with tremendous pace causing severe security concerns, as it trade most of private information. To counter that security issues in low resource applications, lightweight cryptographic algorithms have been introduced in recent past. In this paper we propose efficient hardware architecture of piccolo lightweight algorithm uses 64 bits block size with variable key size of length 80 and 128 bits. This paper introduces novel hardware architecture of piccolo-80, to supports high speed RFID security applications. Different design strategies are there to optimize the hardware metrics trade-off for particular application. The algorithm is implemented on different family of FPGAs with different devices to analyze the performance of design in 4 input LUTs and 6 input LUTs implementations. In addition, the results of hardware design are evaluated and compared with the most relevant lightweight block ciphers, shows the proposed architecture finds its utilization in terms of speed and area optimization from the hardware resources. The increment in throughput with optimized area of this architecture suggests that piccolo can applicable to implement for ultra-lightweight applications also.
2020-01-20
Rasheed, Amar, Hashemi, Ray R., Bagabas, Ayman, Young, Jeffrey, Badri, Chanukya, Patel, Keyur.  2019.  Configurable Anonymous Authentication Schemes For The Internet of Things (IoT). 2019 IEEE International Conference on RFID (RFID). :1–8.
The Internet of Things (IoT) has revolutionized the way of how pervasive computing devices communicate and disseminate information over the global network. A plethora of user data is collected and logged daily into cloud-based servers. Such data can be analyzed by the IoT infrastructure to capture users' behaviors (e.g. users' location, tagging of smart home occupancy). This brings a new set of security challenges, specifically user anonymity. Existing access control and authentication technologies failed to support user anonymity. They relied on the surrendering of the device/user authentication parameters to the trusted server, which hence could be utilized by the IoT infrastructure to track users' behavioral patterns. This paper, presents two novel configurable privacy-preserving authentication schemes. User anonymity capabilities were incorporated into our proposed authentication schemes through the implementation of two crypto-based approaches (i) Zero Knowledge Proof (ZKP) and (ii) Verifiable Common Secret Encoding (VCSE). We consider a user-oriented approach when determining user anonymity. The proposed authentication schemes are dynamically capable of supporting various levels of user privacy based on the user preferences. To validate the two schemes, they were fully implemented and deployed on an IoT testbed. We have tested the performance of each proposed schemes in terms of power consumption and computation time. Based on our performance evaluation results, the proposed ZKP-based approach provides better performance compared to the VCSE-based approach.
2019-11-12
Dreier, Jannik, Hirschi, Lucca, Radomirovic, Sasa, Sasse, Ralf.  2018.  Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR. 2018 IEEE 31st Computer Security Foundations Symposium (CSF). :359-373.

Exclusive-or (XOR) operations are common in cryptographic protocols, in particular in RFID protocols and electronic payment protocols. Although there are numerous applications, due to the inherent complexity of faithful models of XOR, there is only limited tool support for the verification of cryptographic protocols using XOR. The Tamarin prover is a state-of-the-art verification tool for cryptographic protocols in the symbolic model. In this paper, we improve the underlying theory and the tool to deal with an equational theory modeling XOR operations. The XOR theory can be freely combined with all equational theories previously supported, including user-defined equational theories. This makes Tamarin the first tool to support simultaneously this large set of equational theories, protocols with global mutable state, an unbounded number of sessions, and complex security properties including observational equivalence. We demonstrate the effectiveness of our approach by analyzing several protocols that rely on XOR, in particular multiple RFID-protocols, where we can identify attacks as well as provide proofs.

2019-10-02
Alkadi, A., Chi, H., Prodanoff, Z. G., Kreidl, P..  2018.  Evaluation of Two RFID Traffic Models with Potential in Anomaly Detection. SoutheastCon 2018. :1–5.

The use of Knuth's Rule and Bayesian Blocks constant piecewise models for characterization of RFID traffic has been proposed already. This study presents an evaluation of the application of those two modeling techniques for various RFID traffic patterns. The data sets used in this study consist of time series of binned RFID command counts. More specifically., we compare the shape of several empirical plots of raw data sets we obtained from experimental RIFD readings., against the constant piecewise graphs produced as an output of the two modeling algorithms. One issue limiting the applicability of modeling techniques to RFID traffic is the fact that there are a large number of various RFID applications available. We consider this phenomenon to present the main motivation for this study. The general expectation is that the RFID traffic traces from different applications would be sequences with different histogram shapes. Therefore., no modeling technique could be considered universal for modeling the traffic from multiple RFID applications., without first evaluating its model performance for various traffic patterns. We postulate that differences in traffic patterns are present if the histograms of two different sets of RFID traces form visually different plot shapes.

Wang, S., Zhu, S., Zhang, Y..  2018.  Blockchain-Based Mutual Authentication Security Protocol for Distributed RFID Systems. 2018 IEEE Symposium on Computers and Communications (ISCC). :00074–00077.

Since radio frequency identification (RFID) technology has been used in various scenarios such as supply chain, access control system and credit card, tremendous efforts have been made to improve the authentication between tags and readers to prevent potential attacks. Though effective in certain circumstances, these existing methods usually require a server to maintain a database of identity related information for every tag, which makes the system vulnerable to the SQL injection attack and not suitable for distributed environment. To address these problems, we now propose a novel blockchain-based mutual authentication security protocol. In this new scheme, there is no need for the trusted third parties to provide security and privacy for the system. Authentication is executed as an unmodifiable transaction based on blockchain rather than database, which applies to distributed RFID systems with high security demand and relatively low real-time requirement. Analysis shows that our protocol is logically correct and can prevent multiple attacks.

Cherneva, V., Trahan, J..  2019.  A Secure and Efficient Parallel-Dependency RFID Grouping-Proof Protocol. 2019 IEEE International Conference on RFID (RFID). :1–8.

In this time of ubiquitous computing and the evolution of the Internet of Things (IoT), the deployment and development of Radio Frequency Identification (RFID) is becoming more extensive. Proving the simultaneous presence of a group of RFID tagged objects is a practical need in many application areas within the IoT domain. Security, privacy, and efficiency are central issues when designing such a grouping-proof protocol. This work is motivated by our serial-dependent and Sundaresan et al.'s grouping-proof protocols. In this paper, we propose a light, improved offline protocol: parallel-dependency grouping-proof protocol (PDGPP). The protocol focuses on security, privacy, and efficiency. PDGPP tackles the challenges of including robust privacy mechanisms and accommodates missing tags. It is scalable and complies with EPC C1G2.

Sharma, V., Vithalkar, A., Hashmi, M..  2018.  Lightweight Security Protocol for Chipless RFID in Internet of Things (IoT) Applications. 2018 10th International Conference on Communication Systems Networks (COMSNETS). :468–471.

The RFID based communication between objects within the framework of IoT is potentially very efficient in terms of power requirements and system complexity. The new design incorporating the emerging chipless RFID tags has the potential to make the system more efficient and simple. However, these systems are prone to privacy and security risks and these challenges associated with such systems have not been addressed appropriately in the broader IoT framework. In this context, a lightweight collision free algorithm based on n-bit pseudo random number generator, X-OR hash function, and rotations for chipless RFID system is presented. The algorithm has been implemented on an 8-bit open-loop resonator based chipless RFID tag based system and is validated using BASYS 2 FPGA board based platform. The proposed scheme has been shown to possess security against various attacks such as Denial of Service (DoS), tag/reader anonymity, and tag impersonation.

Sharma, V., Malhotra, S., Hashmi, M..  2018.  An Emerging Application Centric RFID Framework Based on New Web Technology. 2018 IEEE International Conference on RFID Technology Application (RFID-TA). :1–6.

In the context of emerging applications such as IoT, an RFID framework that can dynamically incorporate, identify, and seamlessly regulate the RFID tags is considered exciting. Earlier RFID frameworks developed using the older web technologies were limited in their ability to provide complete information about the RFID tags and their respective locations. However, the new and emerging web technologies have transformed this scenario and now framework can be developed to include all the required flexibility and security for seamless applications such as monitoring of RFID tags. This paper revisits and proposes a generic scenario of an RFID framework built using latest web technology and demonstrates its ability to customize using an application for tracking of personal user objects. This has been shown that the framework based on newer web technologies can be indeed robust, uniform, unified, and integrated.

Damghani, H., Hosseinian, H., Damghani, L..  2019.  Investigating Attacks to Improve Security and Privacy in RFID Systems Using the Security Bit Method. 2019 5th Conference on Knowledge Based Engineering and Innovation (KBEI). :833–838.

The RFID technology is now widely used and combined with everyday life. RFID Tag is a wireless device used to identify individuals and objects, in fact, it is a combination of the chip and antenna that sends the necessary information to an RFID Reader. On the other hand, an RFID Reader converts received radio waves into digital information and then provides facilities such as sending data to the computer and processing them. Radio frequency identification is a comprehensive processing technology that has led to a revolution in industry and medicine as an alternative to commercial barcodes. RFID Tag is used to tracking commodities and personal assets in the chain stores and even the human body and medical science. However, security and privacy problems have not yet been solved satisfactorily. There are many technical and economic challenges in this direction. In this paper, some of the latest technical research on privacy and security problems has been investigated in radio-frequency identification and security bit method, and it has been shown that in order to achieve this level of individual security, multiple technologies of RFID security development should combine with each other. These solutions should be cheap, efficient, reliable, flexible and long-term.

2019-05-20
Chu, G., Lisitsa, A..  2018.  Penetration Testing for Internet of Things and Its Automation. 2018 IEEE 20th International Conference on High Performance Computing and Communications; IEEE 16th International Conference on Smart City; IEEE 4th International Conference on Data Science and Systems (HPCC/SmartCity/DSS). :1479–1484.

The Internet of Things (IoT) is an emerging technology, an extension of the traditional Internet which make everything is connected each other based on Radio Frequency Identification (RFID), Sensor, GPS or Machine to Machine technologies, etc. The security issues surrounding IoT have been of detrimental impact to its development and has consequently attracted research interest. However, there are very few approaches which assess the security of IoT from the perspective of an attacker. Penetration testing is widely used to evaluate traditional internet or systems security to date and it normally spends numerous cost and time. In this paper, we analyze the security problems of IoT and propose a penetration testing approach and its automation based on belief-desire-intention (BDI) model to evaluate the security of the IoT.

2019-02-08
Clark, G., Doran, M., Glisson, W..  2018.  A Malicious Attack on the Machine Learning Policy of a Robotic System. 2018 17th IEEE International Conference On Trust, Security And Privacy In Computing And Communications/ 12th IEEE International Conference On Big Data Science And Engineering (TrustCom/BigDataSE). :516-521.

The field of robotics has matured using artificial intelligence and machine learning such that intelligent robots are being developed in the form of autonomous vehicles. The anticipated widespread use of intelligent robots and their potential to do harm has raised interest in their security. This research evaluates a cyberattack on the machine learning policy of an autonomous vehicle by designing and attacking a robotic vehicle operating in a dynamic environment. The primary contribution of this research is an initial assessment of effective manipulation through an indirect attack on a robotic vehicle using the Q learning algorithm for real-time routing control. Secondly, the research highlights the effectiveness of this attack along with relevant artifact issues.

2019-01-31
Tewari, A., Gupta, B. B..  2018.  A Robust Anonymity Preserving Authentication Protocol for IoT Devices. 2018 IEEE International Conference on Consumer Electronics (ICCE). :1–5.

In spite of being a promising technology which will make our lives a lot easier we cannot be oblivious to the fact IoT is not safe from online threat and attacks. Thus, along with the growth of IoT we also need to work on its aspects. Taking into account the limited resources that these devices have it is important that the security mechanisms should also be less complex and do not hinder the actual functionality of the device. In this paper, we propose an ECC based lightweight authentication for IoT devices which deploy RFID tags at the physical layer. ECC is a very efficient public key cryptography mechanism as it provides privacy and security with lesser computation overhead. We also present a security and performance analysis to verify the strength of our proposed approach.

Mahboubi, A., Camtepe, S., Morarji, H..  2018.  Reducing USB Attack Surface: A Lightweight Authentication and Delegation Protocol. 2018 International Conference on Smart Computing and Electronic Enterprise (ICSCEE). :1–7.

A privately owned smart device connected to a corporate network using a USB connection creates a potential channel for malware infection and its subsequent spread. For example, air-gapped (a.k.a. isolated) systems are considered to be the most secure and safest places for storing critical datasets. However, unlike network communications, USB connection streams have no authentication and filtering. Consequently, intentional or unintentional piggybacking of a malware infected USB storage or a mobile device through the air-gap is sufficient to spread infection into such systems. Our findings show that the contact rate has an exceptional impact on malware spread and destabilizing free malware equilibrium. This work proposes a USB authentication and delegation protocol based on radiofrequency identification (RFID) in order to stabilize the free malware equilibrium in air-gapped networks. The proposed protocol is modelled using Coloured Petri nets (CPN) and the model is verified and validated through CPN tools.

2018-05-30
Su, C., Santoso, B., Li, Y., Deng, R. H., Huang, X..  2017.  Universally Composable RFID Mutual Authentication. IEEE Transactions on Dependable and Secure Computing. 14:83–94.

Universally Composable (UC) framework provides the strongest security notion for designing fully trusted cryptographic protocols, and it is very challenging on applying UC security in the design of RFID mutual authentication protocols. In this paper, we formulate the necessary conditions for achieving UC secure RFID mutual authentication protocols which can be fully trusted in arbitrary environment, and indicate the inadequacy of some existing schemes under the UC framework. We define the ideal functionality for RFID mutual authentication and propose the first UC secure RFID mutual authentication protocol based on public key encryption and certain trusted third parties which can be modeled as functionalities. We prove the security of our protocol under the strongest adversary model assuming both the tags' and readers' corruptions. We also present two (public) key update protocols for the cases of multiple readers: one uses Message Authentication Code (MAC) and the other uses trusted certificates in Public Key Infrastructure (PKI). Furthermore, we address the relations between our UC framework and the zero-knowledge privacy model proposed by Deng et al. [1].

2018-05-01
Fraj, R. Ben, Beroulle, V., Fourty, N., Meddeb, A..  2017.  A Global Approach for the Improvement of UHF RFID Safety and Security. 2017 12th International Conference on Design Technology of Integrated Systems In Nanoscale Era (DTIS). :1–2.
Radio Frequency Identification (RFID) devices are widely used in many domains such as tracking, marking and management of goods, smart houses (IoT), supply chains, etc. However, there is a big number of challenges which must still be overcome to ensure RFID security and privacy. In addition, due to the low cost and low consumption power of UHF RFID tags, communications between tags and readers are not robust. In this paper, we present our approach to evaluate at the same time the security and the safety of UHF RFID systems in order to improve them. First, this approach allows validating UHF RFID systems by simulation of the system behavior in presence of faults in a real environment. Secondly, evaluating the system robustness and the security of the used protocols, this approach will enable us to propose the development of new more reliable and secure protocols. Finally, it leads us to develop and validate new low cost and secure tag hardware architectures.
Woo, S., Ha, J., Byun, J., Kwon, K., Tolcha, Y., Kang, D., Nguyen, H. M., Kim, M., Kim, D..  2017.  Secure-EPCIS: Addressing Security Issues in EPCIS for IoT Applications. 2017 IEEE World Congress on Services (SERVICES). :40–43.
In the EPCglobal standards for RFID architecture frameworks and interfaces, the Electronic Product Code Information System (EPCIS) acts as a standard repository storing event and master data that are well suited to Supply Chain Management (SCM) applications. Oliot-EPCIS broadens its scope to a wider range of IoT applications in a scalable and flexible way to store a large amount of heterogeneous data from a variety of sources. However, this expansion poses data security challenge for IoT applications including patients' ownership of events generated in mobile healthcare services. Thus, in this paper we propose Secure-EPCIS to deal with security issues of EPCIS for IoT applications. We have analyzed the requirements for Secure-EPCIS based on real-world scenarios and designed access control model accordingly. Moreover, we have conducted extensive performance comparisons between EPCIS and Secure-EPCIS in terms of response time and throughput, and provide the solution for performance degradation problem in Secure-EPCIS.
2018-02-21
Ristov, P., Mišković, T., Mrvica, A., Markić, Z..  2017.  Reliability, availability and security of computer systems supported by RFID technology. 2017 40th International Convention on Information and Communication Technology, Electronics and Microelectronics (MIPRO). :1459–1464.

The implementation of RFID technology in computer systems gives access to quality information on the location or object tracking in real time, thereby improving workflow and lead to safer, faster and better business decisions. This paper discusses the quantitative indicators of the quality of the computer system supported by RFID technology applied in monitoring facilities (pallets, packages and people) marked with RFID tag. Results of analysis of quantitative indicators of quality compute system supported by RFID technology are presented in tables.

2018-02-02
Anderson, E. C., Okafor, K. C., Nkwachukwu, O., Dike, D. O..  2017.  Real time car parking system: A novel taxonomy for integrated vehicular computing. 2017 International Conference on Computing Networking and Informatics (ICCNI). :1–9.
Automation of real time car parking system (RTCPS) using mobile cloud computing (MCC) and vehicular networking (VN) has given rise to a novel concept of integrated communication-computing platforms (ICCP). The aim of ICCP is to evolve an effective means of addressing challenges such as improper parking management scheme, traffic congestion in parking lots, insecurity of vehicles (safety applications), and other Infrastructure-to-Vehicle (I2V) services for providing data dissemination and content delivery services to connected Vehicular Clients (VCs). Edge (parking lot based) Fog computing (EFC) through road side sensor based monitoring is proposed to achieve ICCP. A real-time cloud to vehicular clients (VCs) in the context of smart car parking system (SCPS) which satisfies deterministic and non-deterministic constraints is introduced. Vehicular cloud computing (VCC) and intra-Edge-Fog node architecture is presented for ICCP. This is targeted at distributed mini-sized self-energized Fog nodes/data centers, placed between distributed remote cloud and VCs. The architecture processes data-disseminated real-time services to the connected VCs. The work built a prototype testbed comprising a black box PSU, Arduino IoT Duo, GH-311RT ultrasonic distance sensor and SHARP 2Y0A21 passive infrared sensor for vehicle detection; LinkSprite 2MP UART JPEG camera module, SD card module, RFID card reader, RDS3115 metal gear servo motors, FPM384 fingerprint scanner, GSM Module and a VCC web portal. The testbed functions at the edge of the vehicular network and is connected to the served VCs through Infrastructure-to-Vehicular (I2V) TCP/IP-based single-hop mobile links. This research seeks to facilitate urban renewal strategies and highlight the significance of ICCP prototype testbed. Open challenges and future research directions are discussed for an efficient VCC model which runs on networked fog centers (NetFCs).
2018-01-23
Ulz, T., Pieber, T., Steger, C., Lesjak, C., Bock, H., Matischek, R..  2017.  SECURECONFIG: NFC and QR-code based hybrid approach for smart sensor configuration. 2017 IEEE International Conference on RFID (RFID). :41–46.

In smart factories and smart homes, devices such as smart sensors are connected to the Internet. Independent of the context in which such a smart sensor is deployed, the possibility to change its configuration parameters in a secure way is essential. Existing solutions do provide only minimal security or do not allow to transfer arbitrary configuration data. In this paper, we present an NFC- and QR-code based configuration interface for smart sensors which improves the security and practicability of the configuration altering process while introducing as little overhead as possible. We present a protocol for configuration as well as a hardware extension including a dedicated security controller (SC) for smart sensors. For customers, no additional hardware other than a commercially available smartphone will be necessary which makes the proposed approach highly applicable for smart factory and smart home contexts alike.

2017-12-20
Maleki, H., Rahaeimehr, R., Jin, C., Dijk, M. van.  2017.  New clone-detection approach for RFID-based supply chains. 2017 IEEE International Symposium on Hardware Oriented Security and Trust (HOST). :122–127.

Radio-Frequency Identification (RFID) tags have been widely used as a low-cost wireless method for detection of counterfeit product injection in supply chains. In order to adequately perform authentication, current RFID monitoring schemes need to either have a persistent online connection between supply chain partners and the back-end database or have a local database on each partner site. A persistent online connection is not guaranteed and local databases on each partner site impose extra cost and security issues. We solve this problem by introducing a new scheme in which a small Non-Volatile Memory (NVM) embedded in RFID tag is used to function as a tiny “encoded local database”. In addition our scheme resists “tag tracing” so that each partner's operation remains private. Our scheme can be implemented in less than 1200 gates satisfying current RFID technology requirements.

Zhou, X., Yao, X., Li, H., Ma, J..  2017.  A bisectional multivariate quadratic equation system for RFID anti-counterfeiting. 2017 IEEE 15th International Conference on Software Engineering Research, Management and Applications (SERA). :19–23.

This paper proposes a novel scheme for RFID anti-counterfeiting by applying bisectional multivariate quadratic equations (BMQE) system into an RF tag data encryption. In the key generation process, arbitrarily choose two matrix sets (denoted as A and B) and a base Rab such that [AB] = λRABT, and generate 2n BMQ polynomials (denoted as p) over finite field Fq. Therefore, (Fq, p) is taken as a public key and (A, B, λ) as a private key. In the encryption process, the EPC code is hashed into a message digest dm. Then dm is padded to d'm which is a non-zero 2n×2n matrix over Fq. With (A, B, λ) and d'm, Sm is formed as an n-vector over F2. Unlike the existing anti-counterfeit scheme, the one we proposed is based on quantum cryptography, thus it is robust enough to resist the existing attacks and has high security.

Sun, D. Z., Xu, G. Q..  2017.  One-Round Provably Secure Yoking-Proof for RFID Applications. 2017 IEEE Trustcom/BigDataSE/ICESS. :315–322.

Under the Internet of Things (IoT), the coexistence proof of multiple RFID tagged objects becomes a very useful mechanism in many application areas such as health care, evidences in court, and stores. The yoking-proof scheme addresses this issue. However, all existing yoking-proof schemes require two or more rounds communication to generate the yoking-proof. In this paper, we investigate the design of one-round yoking-proof schemes. Our contributions are threefold: (1) to confirm the coexistence of the RFID tag pair, we propose a one-round offline yoking-proof scheme with privacy protection. (2) We define a privacy model of the yoking-proof scheme and enhance Moriyama's security model for the yoking-proof scheme. The security and the privacy of the proposed scheme are proved under our models. (3) We further extend the yoking-proof scheme for the coexistence of m RFID tags, where m\textbackslashtextgreater2. The extended scheme maintains one-round. In addition, the proposed technique has efficiency advantage, compared with previous work.

Comon, H., Koutsos, A..  2017.  Formal Computational Unlinkability Proofs of RFID Protocols. 2017 IEEE 30th Computer Security Foundations Symposium (CSF). :100–114.

We set up a framework for the formal proofs of RFID protocols in the computational model. We rely on the so-called computationally complete symbolic attacker model. Our contributions are: 1) to design (and prove sound) axioms reflecting the properties of hash functions (Collision-Resistance, PRF). 2) to formalize computational unlinkability in the model. 3) to illustrate the method, providing the first formal proofs of unlinkability of RFID protocols, in the omputational model.