2009/06/05 by Yannick Chevalier, Chevalier, Yannick, Mounira Kourjieh +2
Computer Science · #Advanced Authentication Protocols Security #Cryptography and Data Security #Cryptography and Security (cs.CR) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #User Authentication and Security Systems #cs.CR #cs.LO
paper · pdf · doi:10.48550/arxiv.0906.1199
arxiv created 2009/06/05 · openalex publication_date 2009/06/05 · arxiv updated 2009/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Analysis of cryptographic protocols in a symbolic model is relative to a deduction system that models the possible actions of an attacker regarding an execution of this protocol. We present in this paper a transformation algorithm for such deduction systems provided the equational theory has the finite variant property. the termination of this transformation entails the decidability of the ground reachability problems. We prove that it is necessary to add one other condition to obtain the decidability of non-ground problems, and provide one new such criterion.