Quantifying pervasive authentication: the case of the Hancke-Kuhn protocol

TL;DR

This paper refines a formal analysis method to provide a security proof for the Hancke-Kuhn proximity authentication protocol, addressing the challenges of hybrid protocols in pervasive, heterogeneous networks.

Contribution

It introduces a probabilistic extension to the Dolev-Yao model for analyzing hybrid security protocols, enabling formal proofs of protocols like Hancke-Kuhn's.

Findings

Provides a formal security proof for the Hancke-Kuhn protocol

Extends protocol analysis methods with probabilistic reasoning

Addresses security analysis in hybrid, pervasive networks

Abstract

As mobile devices pervade physical space, the familiar authentication patterns are becoming insufficient: besides entity authentication, many applications require, e.g., location authentication. Many interesting protocols have been proposed and implemented to provide such strengthened forms of authentication, but there are very few proofs that such protocols satisfy the required security properties. The logical formalisms, devised for reasoning about security protocols on standard computer networks, turn out to be difficult to adapt for reasoning about hybrid protocols, used in pervasive and heterogenous networks. <p> We refine the Dolev-Yao-style algebraic method for protocol analysis by a probabilistic model of guessing, needed to analyze protocols that mix weak cryptography with physical properties of nonstandard communication channels. Applying this model, we provide a precise security proof for a proximity authentication protocol, due to Hancke and Kuhn, that uses a subtle form of probabilistic reasoning to achieve its goals.