Biblio

Cryptographic protocols are utilized for establishing a secure session between “honest” agents which communicate strictly according to the protocol rules as well as for ensuring the authenticated and confidential transmission of messages. The specification of a cryptographic protocol is usually presented as a set of requirements for the sequences of transmitted messages including the format of such messages. Note that protocol can describe several execution scenarios. All these requirements lead to a huge formal specification for a real cryptographic protocol and therefore, it is difficult to verify the security of the whole cryptographic protocol at once. In this paper, to overcome this problem, we suggest verifying the protocol security for its fragments. Namely, we verify the security properties for a special set of so-called traces of the cryptographic protocol. Intuitively, a trace of the cryptographic protocol is a sequence of computations, value checks, and transmissions on the sides of “honest” agents permitted by the protocol. In order to choose such set of traces, we introduce an Adversary model and the notion of a similarity relation for traces. We then verify the security properties of selected traces with Tamarin Prover. Experimental results for the EAP and Noise protocols clearly show that this approach can be promising for automatic verification of large protocols.

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.

Direct Anonymous Attestation (DAA) is a cryptographic scheme that provides Trusted Platform Module TPM-backed anonymous credentials. We develop Tamarin modelling of the ECC-based version of the protocol as it is standardised and provide the first mechanised analysis of this standard. Our analysis confirms that the scheme is secure when all TPMs are assumed honest, but reveals a break in the protocol's expected authentication and secrecy properties for all TPMs even if only one is compromised. We propose and formally verify a minimal fix to the standard. In addition to developing the first formal analysis of ECC-DAA, the paper contributes to the growing body of work demonstrating the use of formal tools in supporting standardisation processes for cryptographic protocols.

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.