2008 Third International Conference on Availability, Reliability and Security Soundness Conditions for Message Encoding Abstractions in Formal Security Protocol Models March 04-March 07 ISBN: 978-0-7695-3102-1
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ARES.2008.30
In formal methods, security protocols are usually modeled with a high level of abstraction. In particular, marshalling/unmarshalling operations on transmitted messages are generally abstracted away. However, in real applications, errors in this protocol component could be exploited to break protocol security. In order to solve this issue, this paper formally shows that, under some constraints checkable on sequential code, if an abstract protocol model is secure, then a refined model, which takes into account a wide class of possible implementations of the marshalling/unmarshalling operations, is implied to be secure too. The paper also indicates possible exploitations of this result.
Citation:
Alfredo Pironti, Riccardo Sisto, "Soundness Conditions for Message Encoding Abstractions in Formal Security Protocol Models," ares, pp.72-79, 2008 Third International Conference on Availability, Reliability and Security, 2008 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb