History-Dependent Scheduling for Cryptographic Processes

Abstract. This paper presents history-dependent scheduling, a new technique for reducing the search space in the verification of cryptographic protocols. This technique allows the detection of some “non-minimal” interleavings during a depth-first search, and was implemented in TRUST, our cryptographic protocol verifier. We give some experimental results showing that our method can greatly increase the efficiency of the verification procedure.

• Type: Conference
• Year: 2004
• Where: VMCAI
• Authors: Vincent Vanackère
• Keywords: Cryptographic Protocol, Cryptographic Protocol Verifier, Search Space, Software Engineering, VMCAI 2004