Subscribe

Issue No.06 - Nov.-Dec. (2013 vol.10)

pp: 355-367

Marcin Poturalski , Swiss Fed. Inst. of Technol. in Lausanne, Lausanne, Switzerland

Panos Papadimitratos , R. Inst. of Technol., Stockholm, Sweden

Jean-Pierre Hubaux , Swiss Fed. Inst. of Technol. in Lausanne, Lausanne, Switzerland

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TDSC.2013.17

ABSTRACT

We develop a formal framework for the analysis of security protocols in wireless networks. The framework captures characteristics necessary to reason about neighbor discovery protocols, such as the neighbor relation, device location, and message propagation time. We use this framework to establish general results about the possibility of neighbor discovery. In particular, we show that time-based protocols cannot in general provide secure neighbor discovery. Given this insight, we also use the framework to prove the security of four concrete neighbor discovery protocols, including two novel time-and-location-based protocols. We mechanize the model and some proofs in the theorem prover Isabelle.

INDEX TERMS

Wireless networks, Formal verification, Knowledge discovery, Computer security, Security of data,distance bounding, Neighbor discovery, relay attack, formal verification

CITATION

Marcin Poturalski, Panos Papadimitratos, Jean-Pierre Hubaux, "Formal Analysis of Secure Neighbor Discovery in Wireless Networks",

*IEEE Transactions on Dependable and Secure Computing*, vol.10, no. 6, pp. 355-367, Nov.-Dec. 2013, doi:10.1109/TDSC.2013.17REFERENCES

- [1] Nokia Instant Community Project, http://research.nokia.com/news9391, 2013.
- [2] D. Basin, S. Čapkun, P. Schaller, and B. Schmidt, "Let's Get Physical: Models and Methods for Real-World Security Protocols,"
Proc. 22nd Int'l Conf. Theorem Proving in Higher Order Logics (TPHOLs), 2009.- [3] S. Brands and D. Chaum, "Distance-Bounding Protocols,"
Proc. Advances in Cryptology, Workshop Theory and Application of Cryptographic Techniques (EUROCRYPT), 1994.- [4] I. Cervesato, C. Meadows, and D. Pavlovic, "An Encapsulated Authentication Logic for Reasoning about Key Distribution Protocols,"
Proc. IEEE 18th Workshop Computer Security Foundations, 2005.- [5] J. Chiang, J. Haas, Y.-C. Hu, P. Kumar, and J. Choi, "Fundamental Limits on Secure Clock Synchronization and Man-in-the-Middle Detection in Fixed Wireless Networks,"
Proc. IEEE INFOCOM, 2009.- [6] J. Clulow, G.P. Hancke, M.G. Kuhn, and T. Moore, "So Near and Yet So Far: Distance-Bounding Attacks in Wireless Networks,"
Proc. Third European Workshop Security and Privacy in Ad Hoc and Sensor Networks (ESAS), 2006.- [7] C. Cremers, K.B. Rasmussen, and S. Capkun, "Distance Hijacking Attacks on Distance Bounding Protocols,"
Proc. 2012 IEEE Symposium on Security and Privacy, 2012.- [8] A. Datta, A. Derek, J. Mitchell, and D. Pavlovic, "A Derivation System and Compositional Logic for Security Protocols,"
J. Computer Security, vol. 13, pp. 423-482, 2005.- [9] J. Eriksson, S.V. Krishnamurthy, and M. Faloutsos, "TrueLink: A Practical Countermeasure to the Wormhole Attack in Wireless Networks,"
Proc. IEEE 14th Int'l Conf. Network Protocols (ICNP), 2006.- [10] A. Francillon, B. Danev, and S. Čapkun, "Relay Attacks on Passive Keyless Entry and Start Systems in Modern Cars,"
Proc. 18th Ann. Network and Distributed System Security Symp. (NDSS), 2011.- [11] G. Hancke and M. Kuhn, "An RFID Distance Bounding Protocol,"
Proc. First Int'l Conf. Security and Privacy for Emerging Areas in Comm. Networks (SecureComm), 2005.- [12] G.P. Hancke, "Practical Attacks on Proximity Identification Systems,"
Proc. IEEE Symp. Security and Privacy, 2006.- [13] G.P. Hancke and M.G. Kuhn, "Attacks on Time-of-Flight Distance Bounding Channels,"
Proc. First ACM Conf. Wireless Network Security (WiSec), 2008.- [14] L. Hu and D. Evans, "Using Directional Antennas to Prevent Wormhole Attacks,"
Proc. 11th Ann. Symp. Network and Distributed Systems Security (NDSS), 2004.- [15] Y.-C. Hu, A. Perrig, and D.B. Johnson, "Packet Leashes: A Defense against Wormhole Attacks in Wireless Networks,"
Proc. IEEE INFOCOM, 2003.- [16] S. Malladi, B. Bezawada, and K. Kothapalli, "Automatic Analysis of Distance Bounding Protocols,"
Proc. Workshop Foundations of Computer Security, 2009.- [17] C. Meadows, R. Poovendran, D. Pavlovic, L.-W. Chang, and P. Syverson, "Distance Bounding Protocols: Authentication Logic Analysis and Collusion Attacks,"
Secure Localization and Time Synchronization for Wireless Sensor and Ad Hoc Networks. Springer, 2007.- [18] J. Millen and V. Shmatikov, "Constraint Solving for Bounded Process Cryptographic Protocol Analysis,"
Proc. Eighth ACM Conf. Computer and Comm. Security (CCS), 2001.- [19] T. Nipkow, L.C. Paulson, and M. Wenzel,
A Proof Assistant for Higher Order Logic. Springer, 2008.- [20] P. Papadimitratos, M. Poturalski, P. Schaller, P. Lafourcade, D. Basin, S. Čapkun, and J.-P. Hubaux, "Secure Neighborhood Discovery: A Fundamental Element for Mobile Ad Hoc Networking,"
IEEE Comm. Magazine, vol. 46, no. 2, pp. 132-139, Feb. 2008.- [21] P. Papadimitratos and Z.J. Haas, "Secure Message Transmission in Mobile Ad Hoc Networks,"
Ad Hoc Networks J., vol. 1, no. 1, pp. 193-209, 2003.- [22] L.C. Paulson, "The Inductive Approach to Verifying Cryptographic Protocols,"
J. Computer Security, vol. 6, no. 1/2, pp. 85-128, 1998.- [23] D. Pavlovic and C. Meadows, "Deriving Secrecy Properties in Key Establishment Protocols,"
Proc. 11th European Symp. Research in Computer Security (ESORICS), 2006.- [24] D. Pavlovic and C. Meadows, "Bayesian Authentication: Quantifying Security of the Hancke-Kuhn Protocol,"
Proc. 26th Conf. Math. Foundations of Programming Semantics (MFPS), 2010.- [25] M. Poturalski, M. Flury, P. Papadimitratos, J.-P. Hubaux, and J.-Y. Le Boudec, "Distance Bounding with IEEE 802.15.4a: Attacks and Countermeasures,"
IEEE Trans. Wireless Comm., vol. 10, no. 4, pp. 1334-1344, Apr. 2011.- [26] M. Poturalski, P. Papadimitratos, and J.-P. Hubaux, "Formal Analysis of Secure Neighbor Discovery in Wireless Networks," http://www.ee.kth.se/~papadim/publications/ fulltextTECH_ REPORT_SND_V2.pdf, technical report, 2012.
- [27] M. Poturalski, P. Papadimitratos, and J.-P. Hubaux, "Secure Neighbor Discovery in Wireless Networks: Formal Investigation of Possibility,"
Proc. Third ACM Symp. Information, Computer and Comm. Security (ASIACCS), 2008.- [28] M. Poturalski, P. Papadimitratos, and J.-P. Hubaux, "Towards Provable Secure Neighbor Discovery in Wireless Networks,"
Proc. Sixth ACM Workshop Formal Methods in Security Eng., 2008.- [29] K.B. Rasmussen and S. Čapkun, "Implications of Radio Fingerprinting on the Security of Sensor Networks,"
Proc. IEEE Third Conf. Security and Privacy in Comm. Networks (SecureComm), 2007.- [30] R. Robles, J. Haas, J. Chiang, Y.-C. Hu, and P. Kumar, "Secure Topology Discovery through Network-Wide Clock Synchronization,"
Proc. Third Int'l Conf. Signal Processing and Comm. (SPCOM), 2010.- [31] P. Schaller, B. Schmidt, D. Basin, and S. Čapkun, "Modeling and Verifying Physical Properties of Security Protocols for Wireless Networks,"
Proc. IEEE 22nd Computer Security Foundations Symp. (CSF), 2009.- [32] F.J. Thayer, J.C. Herzog, and J.D. Guttman, "Strand Spaces: Why Is a Security Protocol Correct?"
Proc. IEEE Symp. Security and Privacy, 1998.- [33] F.J. Thayer, V. Swarup, and J.D. Guttman, "Metric Strand Spaces for Locale Authentication Protocols,"
Proc. Fourth IFIP Int'l Conf. Trust Management, 2010. |