Timed Calculus of Cryptographic Communication

摘要

We extend the (core) Calculus of Cryptographic Communication (C{sup}3) with real time, e.g., time stamps and timed keys. We illustrate how to use this extended calculus (tC{sup}3) on a specification and verification case study, namely the failure of the Wide-Mouthed-Frog protocol in its original, i.e., timed, version.