[{"type":"thesis","title":"Towards Applying Cryptographic Security Models to Real-World Systems","issued":{"date-parts":[["2020","4","27"]]},"DOI":"10.5445\/IR\/1000118648","genre":"Dissertation","author":[{"family":"Rill","given":"Jochen"}],"publisher":"Karlsruher Institut f\u00fcr Technologie (KIT)","abstract":"The cryptographic methodology of formal security analysis usually works in three steps: \r\nchoosing a security model, describing a system and its intended security properties, and creating a formal proof of security.\r\nFor basic cryptographic primitives and simple protocols this is a well understood process and is performed regularly.\r\nFor more complex systems, as they are in use in real-world settings it is rarely applied, however.\r\nIn practice, this often leads to missing or incomplete descriptions of the security properties and requirements of such systems, which in turn can lead to insecure implementations and consequent security breaches.\r\nOne of the main reasons for the lack of application of formal models in practice is that they are particularly difficult to use and to adapt to new use cases.\r\n\r\nWith this work, we therefore aim to investigate how cryptographic security models can be used to argue about the security of real-world systems.\r\nTo this end, we perform case studies of three important types of real-world systems: data outsourcing, computer networks and electronic payment.\r\n\r\nFirst, we give a unified framework to express and analyze the security of data outsourcing schemes.\r\nWithin this framework, we define three privacy objectives: \\emph{data privacy}, \\emph{query privacy}, and \\emph{result privacy}.\r\nWe show that data privacy and query privacy are independent concepts, while result privacy is consequential to them.\r\nWe then extend our framework to allow the modeling of \\emph{integrity} for the specific use case of file systems.\r\nTo validate our model, we show that existing security notions can be expressed within our framework and we prove the security of CryFS---a cryptographic cloud file system.\r\n\r\nSecond, we introduce a model, based on the Universal Composability (UC) framework, in which computer networks and their security properties can be described \r\nWe extend it to incorporate time, which cannot be expressed in the basic UC framework, and give formal tools to facilitate its application.\r\nFor validation, we use this model to argue about the security of architectures of multiple firewalls in the presence of an active adversary.\r\nWe show that a parallel composition of firewalls exhibits strictly better security properties than other variants.\r\n\r\nFinally, we introduce a formal model for the security of electronic payment protocols within the UC framework.\r\nUsing this model, we prove a set of necessary requirements for secure electronic payment.\r\nBased on these findings, we discuss the security of current payment protocols and find that most are insecure.\r\nWe then give a simple payment protocol inspired by chipTAN and photoTAN and prove its security within our model.\r\n\r\nWe conclude that cryptographic security models can indeed be used to describe the security of real-world systems.\r\nThey are, however, difficult to apply and always need to be adapted to the specific use case.","number-of-pages":127,"kit-publication-id":"1000118648"}]