Securing statically-verified communications protocols against timing attacks |
Mikael Buchholtz, Stephen Gilmore, Jane Hillston, Flemming Nielson
|
| Abstract | We present a federated analysis of communication protocols which considers both security properties and timing. These are not entirely independent observations of a protocol; by using timing observations of an executing protocol it is possible to deduce derived information about the nature of the communication even in the presence of unbreakable encryption. Our analysis is based on expressing the protocol as a process algebra model and deriving from this process models analysable by the Imperial PEPA Compiler and the LySatool. |
| Type | Conference paper [With referee] |
| Conference | Proceedings of First International Workshop on Practical Applications of Stochastic Modelling (PASM 04) |
| Year | 2004 |
| Series | Electronic Notes in Computer Science |
| Note | To appear. |
| Electronic version(s) | [pdf] |
| BibTeX data | [bibtex] |
| IMM Group(s) | Computer Science & Engineering |