Name
Abstract | ||
|---|---|---|
We address the insecurity problem for cryptographic protocols, for an active intruder and a bounded number of sessions. The protocol steps are modeled as rigid Horn clauses, and the intruder abilities as an equational theory. The problem of active intrusion -- such as whether a secret term can be derived, possibly via interaction with the honest participants of the protocol -- is then formulated as a Cap Unification problem. Cap Unification is an extension of Equational 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 employed in a simple manner to detect attacks exploiting some properties of block ciphers. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1145/1755688.1755713 | ASIACCS |
Keywords | Field | DocType |
protocol security modulo homomorphic,cap unification,insecurity problem,active intruder,intruder capability,cap unification problem,intruder ability,homomorphic encryption theory,active intrusion,equational unification,equational theory,homomorphic encryption,protocol,cryptographic protocol,block cipher,rewriting,unification | Homomorphic encryption,Horn clause,Cryptographic protocol,Block cipher,Computer science,Modulo,Unification,Computer security,Theoretical computer science,Rewriting,Bounded function | Conference |
Citations | PageRank | References |
4 | 0.44 | 17 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Siva Anantharaman | 1 | 104 | 10.87 |
| Hai Lin | 2 | 23 | 2.96 |
| Christopher Lynch | 3 | 27 | 3.62 |
| Paliath Narendran | 4 | 1100 | 114.99 |
| Michael Rusinowitch | 5 | 390 | 33.33 |