Automatic analysis of distance bounding protocols

Distance bounding protocols are used by nodes in wireless networks for the crucial purpose of estimating their distances to other nodes. Past efforts to analyze these protocols have only been manual. In this paper, we use the constraint solver tool to automatically analyze distance bounding protocols: We first formulate a new trace property called Secure Distance Bounding (SDB) that protocol executions must satisfy. We then classify the scenarios in which these protocols can operate considering the (dis)honesty of nodes and location of the attacker in the network. Finally, we extend the constraint solver tool so that it can be used to test protocols for violations of SDB in those scenarios and illustrate our technique on several examples. Keywords. Wireless networks, Sensor networks, Localization, Distance bounding, Formal methods, Constraint solving, Cryptographic protocols, Timed analysis.

• Type: Journal
• Year: 2010
• Where: CORR
• Authors: Sreekanth Malladi, Bezawada Bruhadeshwar, Kishore Kothapalli
• Keywords: Bounding, CORR 2010, Education, Solver Tool, Wireless Networks