Protocol Analysis with Time: Experimental Output
Damián Aparicio-Sánchez1, Santiago Escobar1, Catherine Meadows2, José Meseguer3 and Julia Sapiña1
1 DSIC-ELP, Universitat Politècnica de València, Spain.
2 Naval Research Laboratory, Washington DC, USA.
3 University of Illinois at Urbana-Champaign, USA.
In this web page we present a suite of experiments analyzing a set of distance-bounding protocols, demonstrating that adding time to Maude-NPA works well in practice.
Find all the material in a ZIP file
here
Table of results
We present the different distance-bounding protocols that we have analyzed, where ✓ means we are able to prove the protocol secure, × means the protocol is not secure. We have analyzed two properties for each protocol: Mafia fraud attack (i.e., an attacker tries to convince the verifier that an honest prover is close to him whereas he is far away), and Distance hijacking fraud attack (i.e., a dishonest prover located far away succeeds in convincing a verifier that they are actually close, and he may only exploit the presence of honest participants in the neighborhood to achieve his goal). The column PreProc gives the time it takes Maude-NPA to perform some preprocessing on the specification that eliminates searches for some provably unreachable state and the column tm(sec) give the times in seconds that it took for a search to complete.
| Protocol | PreProc(sec) | Mafia | time(sec) | Hijacking | time(sec) |
|---|---|---|---|---|---|
| Brands and Chaum[3] | 3.0 | ✓ | 4.3 | × | 11.4 |
| Meadows et al (nV ⊗ nP,P)[18] | 3.7 | ✓ | 1.3 | ✓ | 22.5 |
| Meadows et al (nV,nP ⊗ P)[18] | 3.5 | ✓ | 1.1 | × | 1.5 |
| Hancke and Kuhn[13] | 1.2 | ✓ | 12.5 | ✓ | 0.7 |
| MAD[4] | 5.1 | ✓ | 110.5 | × | 318.8 |
| Swiss-Knife[14] | 3.1 | ✓ | 4.8 | ✓ | 24.5 |
| Munilla et al.[20] | 1.7 | ✓ | 107.1 | ✓ | 4.5 |
| CRCS[27] | 3.0 | ✓ | 450.1 | × | 68.6 |
| TREAD[1] | 2.4 | ✓ | 4.7 | × | 4.2 |
References
1. Gildas Avoine, Xavier Bultel, Sébastien Gambs, David Gérault, Pascal Lafourcade, Cristina Onete, and Jean-Marc Robert. A terrorist-fraud resistant and extractor-free anonymous distance-bounding protocol. In Ramesh Karri, Ozgur Sinanoglu, Ahmad-Reza Sadeghi, and Xun Yi, editors, Proceedings of the 2017 ACM on Asia Conference on Computer and Communications Security, AsiaCCS 2017, Abu Dhabi, United Arab Emirates, April 2-6, 2017, pages 800–814. ACM, 2017.
3. Stefan Brands and David Chaum. Distance-bounding protocols (extended abstract). In Tor Helleseth, editor, Advances in Cryptology - EUROCRYPT’93, Workshop on the Theory and Application of of Cryptographic Techniques, Lofthus, Norway, May 23-27, 1993, Proceedings, volume 765 of Lecture Notes in Computer Science, pages 344–359. Springer, 1993.
4. Srdjan Capkun, Levente Buttyán, and Jean-Pierre Hubaux. SECTOR: secure tracking of node encounters in multi-hop wireless networks. In Sanjeev Setia and Vipin Swarup, editors, Proceedings of the 1st ACM Workshop on Security of ad hoc and Sensor Networks, SASN 2003, Fairfax, Virginia, USA, 2003, pages 21–32. ACM, 2003.
13. Gerhard P. Hancke and Markus G. Kuhn. An RFID distance bounding protocol. In First International Conference on Security and Privacy for Emerging Areas in Communications Networks, SecureComm 2005, Athens, Greece, 5-9 September, 2005, pages 67–73. IEEE, 2005.
14. Chong Hee Kim, Gildas Avoine, François Koeune, François-Xavier Standaert, and Olivier Pereira. The swiss-knife RFID distance bounding protocol. In Pil Joong Lee and Jung Hee Cheon, editors, Information Security and Cryptology-ICISC 2008, 11th International Conference, Seoul, Korea, December 3-5, 2008, Revised Selected Papers, volume 5461 of Lecture Notes in Computer Science, pages 98–115. Springer, 2008.
18. C. Meadows, R. Poovendran, D. Pavlovic, L. W. Chang, and P. Syverson. Distance Bounding Protocols: Authentication Logic Analysis and Collusion Attacks. In R. Poovendran, S. Roy, and C. Wang, editors, Secure Localization and Time Synchronization for Wireless Sensor and Ad Hoc Networks. Advances in Information Security, volume 30, pages 279–298. Springer, 2007.
20. Jorge Munilla and Alberto Peinado. Distance bounding protocols for RFID enhanced by using void-challenges and analysis in noisy channels. Wireless Communications and Mobile Computing, 8(9):1227–1232, 2008.
27. Kasper Bonne Rasmussen and Srdjan Capkun. Realization of RF distance bounding. In 19th USENIX Security Symposium, Washington, DC, USA, August 11-13, 2010, Proceedings, pages 389–402. USENIX Association, 2010.