Sciweavers

Share
APLAS
2007
ACM

Type-Based Verification of Correspondence Assertions for Communication Protocols

9 years 1 months ago
Type-Based Verification of Correspondence Assertions for Communication Protocols
Gordon and Jeffrey developed a type system for checking correspondence assertions. The correspondence assertions, proposed by Woo and Lam, state that when a certain event (called an "end" event) happens, the corresponding "begin" event must have occurred before. They can be used for checking authenticity in communication protocols. In this paper, we refine Gordon and Jeffrey's type system and develop a polynomial-time type inference algorithm, so that correspondence assertions can be verified fully automatically, without any type annotations. The main key idea that enables polynomial-time type inference is to introduce fractional effects; Without the fractional effects, the type inference problem is NP-hard.
Daisuke Kikuchi, Naoki Kobayashi
Added 12 Aug 2010
Updated 12 Aug 2010
Type Conference
Year 2007
Where APLAS
Authors Daisuke Kikuchi, Naoki Kobayashi
Comments (0)
books