Journal Title
Title of Journal: Int J Inf Secur
|
Abbravation: International Journal of Information Security
|
Publisher
Springer-Verlag
|
|
|
|
|
|
Authors: Theodoros Balopoulos Stefanos Gritzalis Sokratis K Katsikas
Publish Date: 2008/05/28
Volume: 7, Issue: 6, Pages: 395-420
Abstract
Formal methods are an important tool for designing secure cryptographic protocols However the existing work on formal methods does not cover privacypreserving protocols as much as other types of protocols Furthermore privacyrelated properties such as unlinkability are not always easy or even possible to prove statically but need to be checked dynamically during the protocol’s execution In this paper we demonstrate how starting from an informal description of a privacypreserving protocol in natural language one may use a modified and extended version of the Typed MSR language to create a formal specification of this protocol typed in a linkabilityoriented type system and then use this specification to reach an implementation of this protocol in Jif in such a way that privacy vulnerabilities can be detected with a mixture of static and runtime checks
Keywords:
.
|
Other Papers In This Journal:
|