Adding support for user-defined sorts and sorted function symbols to Tamarin
OPEN ACCESS
Loading...
Author / Producer
Date
2013
Publication Type
Master Thesis
ETH Bibliography
yes
Citations
Altmetric
OPEN ACCESS
Data
Rights / License
Abstract
A security protocol is an exchange of messages between multiple parties with the intent of achieving certain security properties, such as confidentiality of message contents or authentication. Security protocol verification tools are used to formally verify the properties these protocols claim. These tools are often limited by the type of protocols they can model appropriately. Recently, a new tool called Tamarin was developed which allows for the modeling of security protocols that make use of Diffie-Hellman exponentiation, as well as allowing for advanced security properties, such as compromising adversaries.
We extend the theory behind Tamarin to allow for the modeling of protocols which could not be properly modeled before. Our changes include support for user-defined sorts and function symbols, built-in natural numbers, and iterated function application. We argue how our changes fit with the original theory behind Tamarin. We implement our modifications and show examples of protocols modeled with the new capabilities. We present an improvement in the modeling of existing protocols in the Tamarin security protocol verification tool. We exemplify part of our improvements by a protocol working with a simple encrypted counter value, called the Counter protocol. We also show a protocol which could not be properly modeled in Tamarin before: we present a protocol based on a minimal hash chain based on our iterated function application extension.
We extend the theory behind Tamarin to allow for the modeling of protocols which could not be properly modeled before. Our changes include support for user-defined sorts and function symbols, built-in natural numbers, and iterated function application. We argue how our changes fit with the original theory behind Tamarin. We implement our modifications and show examples of protocols modeled with the new capabilities. We present an improvement in the modeling of existing protocols in the Tamarin security protocol verification tool. We exemplify part of our improvements by a protocol working with a simple encrypted counter value, called the Counter protocol. We also show a protocol which could not be properly modeled in Tamarin before: we present a protocol based on a minimal hash chain based on our iterated function application extension.
Permanent link
Publication status
published
External links
Editor
Book title
Journal / series
Volume
Pages / Article No.
Publisher
Eidgenössische Technische Hochschule Zürich
Event
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
CODIERUNG (INFORMATIONSTHEORIE); DATA SECURITY + DATA PROTECTION (OPERATING SYSTEMS); NETWORK PROTOCOLS + COMMUNICATION PROTOCOLS (COMPUTER SYSTEMS); NETZWERKPROTOKOLLE + KOMMUNIKATIONSPROTOKOLLE (COMPUTERSYSTEME); CODING (INFORMATION THEORY); DATENSICHERHEIT + DATENSCHUTZ (BETRIEBSSYSTEME)
Organisational unit
02660 - Institut für Informationssicherheit / Institute of Information Security
02150 - Dep. Informatik / Dep. of Computer Science