Name
Abstract | ||
|---|---|---|
Security protocols flaws are notoriously difficult to detect. Comparatively little attention has been given to logics of knowledge, although such logics have been proven to be very useful in the specifications of protocols for communication systems. We address ourselves to the analysis of security protocols under the Dolev-Yao model by using a logic of algorithmic knowledge, and propose a general method to describe formally the data structures used in the verification, such as messages, traces, intruders, and so on. We explore the use of our methodology for the verification of security protocols. The Horng-Hsu attack to Helsinki protocol has been found successfully in this setting by using SPIN. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1109/GRC.2006.1635866 | GrC |
Keywords | Field | DocType |
algorithmic knowledge,cryptographic protocols,intruder model,security,data structure,algorithm design and analysis,communication system,logic,protocols,indexing terms,cryptographic protocol,data structures,data security,mathematical model,cryptography,security protocol | Data structure,Data security,Algorithm design,Cryptographic protocol,Computer science,Computer security,Cryptography,Communications system,Content-addressable storage | Conference |
ISBN | Citations | PageRank |
1-4244-0134-8 | 0 | 0.34 |
References | Authors | |
6 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Xiao Mei-hua | 1 | 1 | 1.39 |
| Jinyun Xue | 2 | 127 | 24.47 |