@inproceedings{wsan07,
	author={Model Checking Wireless Sensor Network Security Protocols: TinySec + LEAP},
	title={Llanos Tobarra, Diego Cazorla, Fernando Cuartero, Gregorio D{\'i}az, and Emilia
		Cambronero},
	abstract={In this paper, a formal analysis of security protocols in the field of
		wireless sensor networks is presented. Two complementary protocols, TinySec
		and LEAP, are modelled using the high-level formal language HLPSL, and
		verified using the model checking tool Avispa, where two main security
		properties are checked: authenticity and confidentiality of messages.
		As a result of this analysis, two attacks have been found: 
a man-in-the-middle- 	attack and a type flaw attack. In both cases confidentiality
is compromised 	and an intruder may obtain confidential data from a node in the network.
		Two solutions to these attacks are proposed in the paper.},
	booktitle={First IFIP International Conference on Wireless Sensor and Actor Networks
		(WSAN 2007)},
	year={2007},
	month={September}
}