Abstract | ||
---|---|---|
We propose a method for engineering security protocols that are aware of timing aspects. We study a simplified version of the well-known Needham Schroeder protocol and the complete Yahalom protocol, where timing information allows the study of different attack scenarios. We model check the protocols using UPPAAL. Further, a taxonomy is obtained by studying and categorising protocols from the well known Clark Jacob library and the Security Protocol Open Repository (SPORE) library. Finally, we present some new challenges and threats that arise when considering time in the analysis, by providing a novel protocol that uses time challenges and exposing a timing attack over an implementation of an existing security protocol. |
Year | DOI | Venue |
---|---|---|
2005 | 10.3233/JCS-2007-15603 | Journal of Computer Security - Formal Methods in Security Engineering Workshop (FMSE 04) |
Keywords | DocType | Volume |
complete yahalom protocol,categorising protocol,novel protocol,timing aspect,model checking.,engineering security protocol,timing information,well-known needham schroeder protocol,timed analysis,clark jacob library,timed automata,timing attack,existing security protocol,security protocols,timing analysis,model checking,security protocol | Journal | 15 |
Issue | ISSN | Citations |
6 | 0926-227X | 9 |
PageRank | References | Authors |
0.54 | 26 | 4 |
Name | Order | Citations | PageRank |
---|---|---|---|
R. Corin | 1 | 87 | 4.58 |
S. Etalle | 2 | 116 | 6.19 |
P. H. Hartel | 3 | 40 | 3.16 |
Angelika Mader | 4 | 199 | 19.44 |