An overview of the EAP-based handover

procedures of the IEEE 802.16e standard is introduced and their

security vulnerabilities are analyzed. Possible solutions for secure

handover in IEEE 802.16e networks that guarantee a backward

and forward secrecy are described and formally verified using

Scyther, a specialized model checker for security protocols. These

solutions showed a few drawbacks in the verified procedure and

some modifications are proposed for a more secure and efficient

handover protocol.