Delzanno, Giorgio; Ganty, Pierre Automatic verification of time sensitive cryptographic protocols. (English) Zbl 1126.68392 Jensen, Kurt (ed.) et al., Tools and algorithms for the construction and analysis of systems. 10th international conference, TACAS 2004, held as part of the joint conferences on theory and practice of software, ETAPS 2004, Barcelona, Spain, March 29 – April 2, 2004. Proceedings. Berlin: Springer (ISBN 3-540-21299-X/pbk). Lecture Notes in Computer Science 2988, 342-356 (2004). Summary: We investigate the applicability of symbolic exploration to the automatic verification of secrecy and authentication properties for time sensitive cryptographic protocols. Our formal specifications are given in multiset rewriting over first-order atomic formulas enriched with constraints so as to uniformly model fresh name generation and validity condition of time stamps. Our verification approach is based on data structures for symbolically representing sets of configurations of an arbitrary number of parallel protocol sessions. As a case study we discuss the verification of timed authentication for the Wide Mouth Frog protocol.For the entire collection see [Zbl 1046.68008]. Cited in 3 Documents MSC: 68P25 Data encryption (aspects in computer science) 68P05 Data structures 68Q60 Specification and verification (program logics, model checking, etc.) Software:TAPS; Casper PDFBibTeX XMLCite \textit{G. Delzanno} and \textit{P. Ganty}, Lect. Notes Comput. Sci. 2988, 342--356 (2004; Zbl 1126.68392) Full Text: DOI