Cap Unification: Application to Protocol Security modulo Homomorphic Encryption
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.
Rewriting Unification Protocol Secrecy Analysis
Siva Anantharaman Hai Lin Christopher Lynch Paliath Narendran Michael Rusinowitch
LIFO, Université dOrleans Orléans, France Clarkson University Potsdam, NY, USA University at Albany-SUNY Albany, NY, USA Loria-INRIA Grand Est Nancy, France
国际会议
北京
英文
192-203
2010-04-13（万方平台首次上网日期，不代表论文的发表时间）