Name
Abstract | ||
|---|---|---|
Many decision problems on security protocols can be reduced to solving deduction constraints expressing whether an instance of a given message pattern can be constructed by the intruder. Most constraint solving procedures for protocol security rely on two properties of constraint systems called monotonicity and variable-origination. In this work we relax these restrictions by giving a decision procedure for solving general intruder constraints (that do not have these properties) that stays in NP. The result is also valid modulo an associative, commutative and idempotent theory. The procedure can be applied to verify security protocols in presence of multiple intruders. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1109/CRISIS.2010.5764919 | Risks and Security of Internet and Systems |
Keywords | Field | DocType |
computability,computational complexity,cryptographic protocols,Dolev Yao model,NP decision procedure,general intruder constraint satisfiability,monotonicity properties,nonatomic keys,security protocols,set constructor,variable-origination properties,ACI,Dolev-Yao intruder,Security,constraint solving,general constraints | Decision problem,Dolev–Yao model,Cryptographic protocol,Commutative property,Computer science,Satisfiability,Theoretical computer science,Computability,Public-key cryptography,Computational complexity theory | Conference |
Volume | ISBN | Citations |
80 | 978-1-4244-8642-7 | 4 |
PageRank | References | Authors |
0.41 | 34 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Tigran Avanesov | 1 | 72 | 5.32 |
| Yannick Chevalier | 2 | 910 | 44.46 |
| Michael Rusinowitch | 3 | 390 | 33.33 |
| Mathieu Turuani | 4 | 698 | 31.32 |