Post-Collusion Security and Distance Bounding
Autor: | Zach Smith, Jorge Toro-Pozo, Rolando Trujillo-Rasua, Sjouke Mauw |
---|---|
Rok vydání: | 2019 |
Předmět: |
021110 strategic
defence & security studies Computer science business.industry media_common.quotation_subject Data_MISCELLANEOUS 0211 other engineering and technologies 02 engineering and technology Gas meter prover Cryptographic protocol Modular design Payment Mathematical proof Computer security computer.software_genre Bounding overwatch 020204 information systems Collusion 0202 electrical engineering electronic engineering information engineering business Formal verification computer media_common |
Zdroj: | CCS |
DOI: | 10.1145/3319535.3345651 |
Popis: | Verification of cryptographic protocols is traditionally built upon the assumption that participants have not revealed their long-term keys. However, in some cases, participants might collude to defeat some security goals, without revealing their long-term secrets. We develop a model based on multiset rewriting to reason about collusion in security protocols. We introduce the notion of post-collusion security, which verifies security properties claimed in sessions initiated after the collusion occurred. We use post-collusion security to analyse terrorist fraud on protocols for securing physical proximity, known as distance-bounding protocols. In a terrorist fraud attack, agents collude to falsely prove proximity, whilst no further false proximity proof can be issued without further collusion. Our definitions and the Tamarin prover are used to develop a modular framework for verification of distance-bounding protocols that accounts for all types of attack from literature. We perform a survey of over 25 protocols, which include industrial protocols such as Mastercard's contactless payment PayPass and NXP's MIFARE Plus with proximity check. For the industrial protocols we confirm attacks, propose fixes, and deliver computer-verifiable security proofs of the repaired versions. |
Databáze: | OpenAIRE |
Externí odkaz: |