SPECIFICATION OF CRYPTOGRAPHIC PROTOCOLS USING INTERVAL TEMPOTAL LOGIC

Abstract

In this paper Interval Temporal Logic (ITL) [1] is used to specify cryptographic protocols. We choose Kerberos as a case strudy because of its apparent terporal characteristics. Using ITL, the communication protocol of Kerberos is specified formally. Inference rules of timed belief are presented. Therefore the temporal properties of Kerberos can be specified and verified.