Article citationsMore>>

L. Bozga, C. Ene and Y. Lakhnech, “A Symbolic Decision Procedure for Cryptographic Protocols with Time Stamps,” Journal of Logic and Algebraic Programming, Vol. 65, No. 1, 2005, pp. 1-35.

has been cited by the following article:

• TITLE: Extending the Strand Space Method with Timestamps: Part I the Theory

  AUTHORS: Yongjian Li, Jun Pang

  KEYWORDS: Strand Space, Kerberos V, Theorem Proving, Verification, Isabelle/HOL

  JOURNAL NAME: Journal of Information Security, Vol.1 No.2, October 29, 2010

  ABSTRACT: In this paper, we present two extensions of the strand space method to model Kerberos V. First, we include time and timestamps to model security protocols with timestamps: we relate a key to a crack time and combine it with timestamps in order to define a notion of recency. Therefore, we can check replay attacks in this new framework. Second, we extend the classic strand space theory to model protocol mixture. The main idea is to introduce a new relation to model the causal relation between one primary protocol session and one of its following secondary protocol session. Accordingly, we also extend the definition of unsolicited authentication test.