会议专题

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

国际会议

5th International Symposium on ACM Symposium on Information,Computer and Communications Security(ACM信息、计算机和通信安全国际会议 ASIACCS 2010)

北京

英文

192-203

2010-04-13(万方平台首次上网日期,不代表论文的发表时间)