Extending the Strand Space Method to Verify Kerberos V

摘要

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