کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
433963 | 1441693 | 2014 | 26 صفحه PDF | دانلود رایگان |
Gorrieri and Martinelli’s timed Generalized Non-Deducibility on Compositions (tGNDC) schema is a well-known general framework for the formal verification of security protocols in a concurrent scenario. We generalise the tGNDC schema to verify wireless network security protocols. Our generalisation relies on a simple timed broadcasting process calculus whose operational semantics is given in terms of a labelled transition system which is used to derive a standard simulation theory . We apply our tGNDC framework to perform a security analysis of three well-known key management protocols for wireless sensor networks: μTESLA, LEAP+ and LiSP.
► We generalise Gorrieri and Martinelli’s tGNDC security framework.
► Our generalisation relies on a simple timed broadcasting process calculus.
► Our generalisation relies on a standard simulation theory.
► We apply our generalisation to verify real-world wireless networks key management protocols.
Journal: Science of Computer Programming - Volume 81, 15 February 2014, Pages 53–78