4 papers
Automated Synthesis of a Finite Complexity Ordering for Saturation
Yannick Chevalier, Mounira Kourjieh
We present in this paper a new procedure to saturate a set of clauses with respect to a well-founded ordering on ground atoms such that A < B implies Var(A) {\subseteq} Var(B) for…
On the Decidability of (ground) Reachability Problems for Cryptographic Protocols (extended version)
Yannick Chevalier, Kourjieh Mounira
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. W…
Key Substitution in the Symbolic Analysis of Cryptographic Protocols (extended version)
Yannick Chevalier, Mounira Kourjieh
Key substitution vulnerable signature schemes are signature schemes that permit an intruder, given a public verification key and a signed message, to compute a pair of signature an…
A Symbolic Intruder Model for Hash-Collision Attacks
Yannick Chevalier, Mounira Kourjieh
In the recent years, several practical methods have been published to compute collisions on some commonly used hash functions. In this paper we present a method to take into accoun…