International Association for Cryptologic Research

International Association
for Cryptologic Research

IACR News item: 18 January 2013

Ta Vinh Thong, Amit Dvir
ePrint Report ePrint Report
In this paper, we address the problem of formal and automated security verification of WSN transport

protocols that may perform cryptographic operations. The verification of this class of protocols is difficult

because they typically consist of complex behavioral characteristics, such as real-time, probabilistic, and

cryptographic operations. To solve this problem, we propose a

probabilistic timed calculus for cryptographic protocols, and demonstrate how to use this formal language

for proving security or vulnerability of protocols. The main advantage of the proposed language is that it

supports an expressive syntax and semantics, including bisimilarities that supports real-time, probabilistic,

and cryptographic issues at the same time. Hence, it can be used to verify the systems that involve these three

property in a more convenient way. In addition, we propose an automatic verification method, based on the

well-known PAT process analysis toolkit, for this class of protocols.

For demonstration purposes, we apply the proposed manual and automatic proof methods for verifying the security of

DTSN and SDTP, which are two of the recently proposed WSN tranport protocols.

Expand

Additional news items may be found on the IACR news page.