LEAP Key Management Protocol: Modeling and Analysis

This publication discusses the LEAP key management protocol for wireless sensor networks, emphasizing formal verification for protocol security. It covers the motivation, key management techniques, LEAP protocol overview, key types, and authentication mechanisms used in the protocol.

• Key Management
• Protocol Analysis
• Wireless Sensor Networks
• Formal Verification

jenning Follow

Uploaded on Feb 23, 2025 | 0 Views

Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.

Presentation Transcript

1. Modeling and Analysis of the LEAP Key Management Protocol* (Why you should also formally verify your favorite protocols) Rakesh Verma Computer Science Department University of Houston *Joint work with Bailey Basile Verma - MWSN 2013 1

2. Motivation 1978: Needham Schroeder Protocol in CACM 1981: Replay attack, Denning & Sacco, CACM, Timestamps or nonces added to fix attack 1995: Man-in-the-middle attack with an insider attacker, Gavin Lowe using the formal verification system, FDR, a model checker for CSP Verma - MWSN 2013 2

3. Key Management for WSN Random key predistribution schemes, e.g., Eschenauer & Gligor Du, Deng, Han and Varshney LEAP SHELL Verma - MWSN 2013 3

4. Outline Key management techniques LEAP Protocol AVISPA Scenarios Tried Attacks Found Conclusions and Future Work Verma - MWSN 2013 4

5. LEAP LEAP: key management protocol intended for large- scale wireless sensor networks Goal: authentication and confidentiality; intruder may eavesdrop, inject packets, and replay messages Desire a robust protocol: that will survive in the face of security attacks Effects of any attacks are minimized (to a node's neighbors only, for example). Supports in-network processing necessary for most applications of these networks Four types of keys: individual keys, pairwise shared keys, cluster keys and group keys Verma - MWSN 2013 5

6. LEAP: Keys Individual keys: symmetric keys shared between the base station and each of the nodes. For example, a node might use the individual key to notify the base station of a suspicious neighbor. Pairwise shared keys: symmetric keys shared between a node and each of its neighbors. Used to establish cluster keys. Cluster keys: symmetric keys shared between a node and all of its neighbors. Used for locally broadcast messages & for updating the group key. Group key: symmetric key shared between the base station and all nodes Allows encrypted and authenticated messages to broadcast through the whole network Verma - MWSN 2013 6

7. LEAP Uses authentication mechanism, -TESLA, for authentication of the sink node (base station) Ensures that the packets sent to the group are from the sink node only Uses a pre-distribution key to help establish the four types of keys. Steps: (1) Individual key established using a function of a seed and the ID of node (2) Nodes broadcast their IDs. Receiving node uses a function, seeded with an initial key, to calculate the shared key between it and each neighbor (3) Cluster key distributed by the cluster head using pairwise communication secured with pairwise shared key (4) For distributing group key, sink node broadcasts it in a multihop cluster- by-cluster manner starting with closest cluster Verma - MWSN 2013 7

8. AVISPA AVISPA = Automated Validation of Internet Security Protocols and Applications Set of applications for building formal models of security protocols & formally analyzing their security properties. Provides: High Level Protocol Specification Language (HLPSL) for specifying protocols and their security properties. Provides: Formal verification tools Verma - MWSN 2013 8

9. Architecture of AVISPA Security Protocol HLPSL Script IF OFMC SATMC CL-AtSe TA4SP Error Traces or Security Proof Verma - MWSN 2013 9

10. AVISPA Each of the back-ends has a different set of options. OFMC and CL-AtSe most useful for us: reliable, allow untyped models, and include the xor function Weak authentication, which does not provide replay protection, can be specified in cases where the protocol is not meant to prevent replay attacks. AVISPA requires extensive experimentation with the many parameters Verma - MWSN 2013 10

11. Scenarios Tried Single Hop Pairwise Shared Key (2 nodes) Single Hop Pairwise Shared Key (3 nodes) Multi-hop Pairwise Shared Key (2 proxies) Cluster Key -TESLA Verma - MWSN 2013 11

12. Attacks Found Replay attacks some simple and some subtle Authentication attacks some can be fixed, but a couple of serious attacks were found Secrecy attack only with an insider attacker Attack due to inconsistent use of -TESLA: LEAP violated recommendation of authors of -TESLA Verma - MWSN 2013 12

13. Other Problems DoS attack LEAP assumes that the time to set up the keys is less than the time it takes an intruder to compromise a node However, an intruder can jam during key set up time and prevent the network from deploying Solution: R-LEAP+: Blackshear and Verma [ACM-SAC 2010, Security track] Verma - MWSN 2013 13

14. Conclusions & Future Work Verify your protocol manually and formally Formal analysis of other protocols: R-LEAP+, Verma - MWSN 2013 14

15. Thank You! Questions/Comments Verma - MWSN 2013 15