×

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].

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
Full Text: DOI