Bayesian Authentication: Quantifying Security of the Hancke-Kuhn Protocol

Dusko Pavlovic, Catherine Meadows

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

8 Citations (Scopus)

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. In some cases, the proofs can be provided in the symbolic model. More often, various physical factors invalidate the perfect cryptography assumption, and the symbolic model does not apply. In such cases, the protocol cannot be secure in an absolute logical sense, but only with a high probability. But while probabilistic reasoning is thus necessary, the analysis in the full computational model may not be warranted, since the protocol security does not depend on any computational assumptions, or on attacker's computational power, but only on some guessing chances. We refine the Dolev-Yao 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 probabilistic reasoning to achieve its goals.
Original languageEnglish
Title of host publicationProceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2010)
EditorsM. Mislove, P. Selinger
Place of PublicationAmsterdam
PublisherElsevier
Pages97-122
Number of pages26
DOIs
Publication statusPublished - Sep 2010
Event26th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2010 - Ottawa, Canada
Duration: 6 May 201010 May 2010
Conference number: 26

Publication series

NameElectronic Notes in Theoretical Computer Science
PublisherElsevier
Volume265
ISSN (Print)1571-0661

Conference

Conference26th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2010
Abbreviated titleMFPS
CountryCanada
CityOttawa
Period6/05/1010/05/10

Fingerprint

Authentication
Cryptography
Mobile devices
Physical properties

Keywords

  • SCS-Cybersecurity
  • Security protocol
  • Pervasive authentication
  • Symbolic model
  • Bayesian reasoning
  • Distance bounding

Cite this

Pavlovic, D., & Meadows, C. (2010). Bayesian Authentication: Quantifying Security of the Hancke-Kuhn Protocol. In M. Mislove, & P. Selinger (Eds.), Proceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2010) (pp. 97-122). (Electronic Notes in Theoretical Computer Science; Vol. 265). Amsterdam: Elsevier. https://doi.org/10.1016/j.entcs.2010.08.007
Pavlovic, Dusko ; Meadows, Catherine. / Bayesian Authentication : Quantifying Security of the Hancke-Kuhn Protocol. Proceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2010). editor / M. Mislove ; P. Selinger. Amsterdam : Elsevier, 2010. pp. 97-122 (Electronic Notes in Theoretical Computer Science).
@inproceedings{22a7ed8a324f4eabaef498c4ac621194,
title = "Bayesian Authentication: Quantifying Security of the Hancke-Kuhn Protocol",
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. In some cases, the proofs can be provided in the symbolic model. More often, various physical factors invalidate the perfect cryptography assumption, and the symbolic model does not apply. In such cases, the protocol cannot be secure in an absolute logical sense, but only with a high probability. But while probabilistic reasoning is thus necessary, the analysis in the full computational model may not be warranted, since the protocol security does not depend on any computational assumptions, or on attacker's computational power, but only on some guessing chances. We refine the Dolev-Yao 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 probabilistic reasoning to achieve its goals.",
keywords = "SCS-Cybersecurity, Security protocol, Pervasive authentication, Symbolic model, Bayesian reasoning, Distance bounding",
author = "Dusko Pavlovic and Catherine Meadows",
year = "2010",
month = "9",
doi = "10.1016/j.entcs.2010.08.007",
language = "English",
series = "Electronic Notes in Theoretical Computer Science",
publisher = "Elsevier",
pages = "97--122",
editor = "M. Mislove and P. Selinger",
booktitle = "Proceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2010)",

}

Pavlovic, D & Meadows, C 2010, Bayesian Authentication: Quantifying Security of the Hancke-Kuhn Protocol. in M Mislove & P Selinger (eds), Proceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2010). Electronic Notes in Theoretical Computer Science, vol. 265, Elsevier, Amsterdam, pp. 97-122, 26th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2010, Ottawa, Canada, 6/05/10. https://doi.org/10.1016/j.entcs.2010.08.007

Bayesian Authentication : Quantifying Security of the Hancke-Kuhn Protocol. / Pavlovic, Dusko; Meadows, Catherine.

Proceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2010). ed. / M. Mislove; P. Selinger. Amsterdam : Elsevier, 2010. p. 97-122 (Electronic Notes in Theoretical Computer Science; Vol. 265).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Bayesian Authentication

T2 - Quantifying Security of the Hancke-Kuhn Protocol

AU - Pavlovic, Dusko

AU - Meadows, Catherine

PY - 2010/9

Y1 - 2010/9

N2 - 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. In some cases, the proofs can be provided in the symbolic model. More often, various physical factors invalidate the perfect cryptography assumption, and the symbolic model does not apply. In such cases, the protocol cannot be secure in an absolute logical sense, but only with a high probability. But while probabilistic reasoning is thus necessary, the analysis in the full computational model may not be warranted, since the protocol security does not depend on any computational assumptions, or on attacker's computational power, but only on some guessing chances. We refine the Dolev-Yao 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 probabilistic reasoning to achieve its goals.

AB - 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. In some cases, the proofs can be provided in the symbolic model. More often, various physical factors invalidate the perfect cryptography assumption, and the symbolic model does not apply. In such cases, the protocol cannot be secure in an absolute logical sense, but only with a high probability. But while probabilistic reasoning is thus necessary, the analysis in the full computational model may not be warranted, since the protocol security does not depend on any computational assumptions, or on attacker's computational power, but only on some guessing chances. We refine the Dolev-Yao 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 probabilistic reasoning to achieve its goals.

KW - SCS-Cybersecurity

KW - Security protocol

KW - Pervasive authentication

KW - Symbolic model

KW - Bayesian reasoning

KW - Distance bounding

U2 - 10.1016/j.entcs.2010.08.007

DO - 10.1016/j.entcs.2010.08.007

M3 - Conference contribution

T3 - Electronic Notes in Theoretical Computer Science

SP - 97

EP - 122

BT - Proceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2010)

A2 - Mislove, M.

A2 - Selinger, P.

PB - Elsevier

CY - Amsterdam

ER -

Pavlovic D, Meadows C. Bayesian Authentication: Quantifying Security of the Hancke-Kuhn Protocol. In Mislove M, Selinger P, editors, Proceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2010). Amsterdam: Elsevier. 2010. p. 97-122. (Electronic Notes in Theoretical Computer Science). https://doi.org/10.1016/j.entcs.2010.08.007