Name
Abstract | ||
|---|---|---|
Küsters and Truderung recently proposed an automatic verification method for security protocols with exclusive or (XOR). Their method reduces protocols with XOR to their XOR-free equivalents, enabling efficient verification by tools such as ProVerif. Although the proposed method works efficiently for verifying secrecy, verification of authentication properties is inefficient and sometimes impossible. In this paper, we improve the work by Küsters and Truderung in two ways. First, we extend their method for authentication verification to a richer class of XOR-protocols by automatically introducing bounded verification. Second, we improve the efficiency of their approach by developing a number of dedicated optimizations. We show the applicability of our work by implementing a prototype and applying it to both existing benchmarks and RFID protocols. The experiments show promising results and uncover a flaw in a recently proposed RFID protocol. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/978-3-642-10373-5_6 | ICFEM |
Keywords | Field | DocType |
authentication verification,efficient verification,dedicated optimizations,existing benchmarks,security protocols,bounded verification,rfid protocol,authentication property,xor-free equivalent,automatic verification method,improving automatic verification,security protocol | Functional verification,Authentication,Cryptographic protocol,Exclusive or,Cyclic redundancy check,Intelligent verification,Computer science,Cryptographic primitive,Theoretical computer science,High-level verification | Conference |
Volume | ISSN | Citations |
5885 | 0302-9743 | 2 |
PageRank | References | Authors |
0.37 | 19 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Xihui Chen | 1 | 92 | 7.22 |
| Ton Deursen | 2 | 2 | 0.37 |
| Jun Pang | 3 | 2 | 0.37 |