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 times- tamps: we relate a key to a crack time and combine it with timestamps in order to define a notion of recency. There- fore, 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 re- lation to model the causal relation between one primary protocol session and one of its following secondary proto- col session. Accordingly, we also revisit the definition of unsolicited authentication test. To demonstrate the power of this new theory, we model the Kerberos V protocol, and prove its secrecy and authentication goals. Our framework and the proofs of the example have been mechanized using Isabelle/HOL.