CONCUR 2004 START ConferenceManager    

A symbolic decision procedure for cryptographic protocols with time stamps

L. Bozga, C. Ene and Y. Lakhnech

Presented at Fifteenth International Conference on Concurrency Theory (CONCUR 2004), London, England, 31 August - 3 September, 2004


We present a symbolic decision procedure for time-sensitive cryptographic protocols with time-stamps. We consider protocols described in a process algebra-like notation that includes clocks, time-stamps and time variables. While the values of all clocks increase with rate one when time passes, time variables are simply variables that range over the time domain and can be used to remember time-stamps, i.e. time values. Our symbolic decision procedure deals with secrecy, authentication and any property that can be described as a safety property. Our approach is based on a logic representation of sets of configurations that combines a decidable logic with time constraints.

START Conference Manager (V2.47.4)