Sequence-Indexed Linear-Time Temporal Logic: Proof System and Application

In this paper, we propose a proof system for reasoning on certain specifications of secure authentication systems. For this purpose, a new logic, sequence-indexed linear-time temporal logic (SLTL), is obtained semantically from standard linear-time temporal logic (LTL) by adding a sequence modal operator that represents a sequence of symbols. By this sequence modal operator, we can appropriately express message flows between clients and servers and states of servers in temporal reasoning. A Gentzen-type sequent calculus for SLTL is introduced, and the completeness and cut-elimination theorems for it are proved. SLTL is also shown to be PSPACE-complete and embeddable into LTL.

• Type: Journal
• Year: 2010
• Where: AAI
• Authors: Ken Kaneiwa, Norihiro Kamide
• Keywords: AAI 2010, Algorithms, Linear-time Temporal Logic, Secure Authentication Systems, Sequence Modal Operator