We address the insecurity problem for cryptographic proto cols, for an active intruder and a bounded number of ses sions. The protocol steps are modeled as rigid Horn clauses, and the intruder abilities as an equational theory. The prob lem of active intrusion - such as whether a secret term can be derived, possibly via interaction with the honest partic ipants of the protocol - is then formulated as a Cap Uni fication problem. Cap Unification is an extension of Equa tional Unification: look for a cap to be placed on a given set of terms, so as to unify it with a given term modulo the equational theory. We give a decision procedure for Cap Unification, when the intruder capabilities are modeled as homomorphic encryption theory. Our procedure can be em ployed in a simple manner to detect attacks exploiting some properties of block ciphers.
展开▼
