A Calculus for the Analysis of Wireless Network Security Protocols

We propose a timed broadcasting calculus for wireless systems. The operational semantics of our calculus is given both in terms of a Reduction Semantics and in terms of a Labelled Transition Semantics. We prove that the two semantics coincide. The labelled transition system is used to derive a standard notion of (weak) bi-similarity which is proved to be a congruence. We use our simulation theory to adapt Gorrieri and Martinelli's tGNDC scheme to investigate, in our setting, the safety of non-trivial wireless network security protocols.

• Type: Journal
• Year: 2010
• Where: IFIP
• Authors: Francesco Ballardin, Massimo Merro
• Keywords: IFIP 2010, Labelled Transition, Labelled Transition Semantics, Programming Languages, Semantics