Paper Info
Title
Soundness Conditions for Message Encoding Abstractions in Formal Security Protocol Models
Abstract
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.
Year
DOI
Venue
2008
10.1109/ARES.2008.30
Barcelona
Keywords
Field
DocType
formal security protocol models,formal method,abstract protocol model,unmarshalling operation,message encoding abstractions,protocol security,possible implementation,constraints checkable,security protocol,refined model,possible exploitation,soundness conditions,protocol component,cryptographic protocols,availability,decoding,encoding,cryptography,protocols,computer languages,data mining,concrete,data security
Cryptographic protocol,Computer security,Computer science,Marshalling,Security service,Implementation,Soundness,Formal methods,Computer security model,Distributed computing,Universal composability
Conference
ISBN
Citations 
PageRank 
978-0-7695-3102-1
3
0.39
References 
Authors
11
2
Name
Order
Citations
PageRank
Alfredo Pironti133027.47
Riccardo Sisto255656.79