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. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Kikuchi, D., & Kobayashi, N. (2007). Type-based verification of correspondence assertions for communication protocols. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4807 LNCS, pp. 191–205). Springer Verlag. https://doi.org/10.1007/978-3-540-76637-7_13
Mendeley helps you to discover research relevant for your work.