Visible to the public Automated Analysis of PUF-based Protocols

TitleAutomated Analysis of PUF-based Protocols
Publication TypeConference Paper
Year of Publication2020
AuthorsFocardi, R., Luccio, F. L.
Conference Name2020 IEEE 33rd Computer Security Foundations Symposium (CSF)
Date PublishedJune 2020
ISBN Number978-1-7281-6572-1
KeywordsAnalytical models, API, APIs, application programming interface, compositionality, cryptographic protocols, cryptography, Data models, error correction data, fingerprint identification, formal methods and verification, Hardware, hardware-based security, integrated circuit, integrated circuits, mutual authentication protocol, physical unclonable functions, Protocols, pubcrawl, PUF API, PUF-based protocols, pufs, resilience, Resiliency, security properties, security protocols, Tamarin prover

Physical Unclonable Functions (PUFs) are a promising technology to secure low-cost devices. A PUF is a function whose values depend on the physical characteristics of the underlying hardware: the same PUF implemented on two identical integrated circuits will return different values. Thus, a PUF can be used as a unique fingerprint identifying one specific physical device among (apparently) identical copies that run the same firmware on the same hardware. PUFs, however, are tricky to implement, and a number of attacks have been reported in the literature, often due to wrong assumptions about the provided security guarantees and/or the attacker model. In this paper, we present the first mechanized symbolic model for PUFs that allows for precisely reasoning about their security with respect to a variegate set of attackers. We consider mutual authentication protocols based on different kinds of PUFs and model attackers that are able to access PUF values stored on servers, abuse the PUF APIs, model the PUF behavior and exploit error correction data to reproduce the PUF values. We prove security properties and we formally specify the capabilities required by the attacker to break them. Our analysis points out various subtleties, and allows for a systematic comparison between different PUF-based protocols. The mechanized models are easily extensible and can be automatically checked with the Tamarin prover.

Citation Keyfocardi_automated_2020