Adding support for user-defined sorts and sorted function symbols to Tamarin
![Thumbnail](/bitstream/handle/20.500.11850/73721/eth-7360-01.pdf.jpg?sequence=3&isAllowed=y)
Open access
Author
Date
2013Type
- Master Thesis
ETH Bibliography
yes
Altmetrics
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.<br/><br/>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. Show more
Permanent link
https://doi.org/10.3929/ethz-a-009959880Publication status
publishedPublisher
Eidgenössische Technische Hochschule ZürichSubject
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 Security02150 - Dep. Informatik / Dep. of Computer Science
More
Show all metadata
ETH Bibliography
yes
Altmetrics