Show simple item record

dc.contributor.author
Staub, Cedric
dc.date.accessioned
2017-07-06T09:07:54Z
dc.date.available
2017-06-10T23:11:35Z
dc.date.available
2017-07-06T09:07:54Z
dc.date.issued
2013
dc.identifier.uri
http://hdl.handle.net/20.500.11850/73721
dc.identifier.doi
10.3929/ethz-a-009959880
dc.description.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.
en_US
dc.language.iso
en
en_US
dc.publisher
Eidgenössische Technische Hochschule Zürich
en_US
dc.rights.uri
http://rightsstatements.org/page/InC-NC/1.0/
dc.subject
CODIERUNG (INFORMATIONSTHEORIE)
en_US
dc.subject
DATA SECURITY + DATA PROTECTION (OPERATING SYSTEMS)
en_US
dc.subject
NETWORK PROTOCOLS + COMMUNICATION PROTOCOLS (COMPUTER SYSTEMS)
en_US
dc.subject
NETZWERKPROTOKOLLE + KOMMUNIKATIONSPROTOKOLLE (COMPUTERSYSTEME)
en_US
dc.subject
CODING (INFORMATION THEORY)
en_US
dc.subject
DATENSICHERHEIT + DATENSCHUTZ (BETRIEBSSYSTEME)
en_US
dc.title
Adding support for user-defined sorts and sorted function symbols to Tamarin
en_US
dc.type
Master Thesis
dc.rights.license
In Copyright - Non-Commercial Use Permitted
dc.date.published
2013
ethz.size
41 p.
en_US
ethz.code.ddc
0 - Computer science, information & general works::004 - Data processing, computer science
en_US
ethz.code.ddc
0 - Computer science, information & general works::004 - Data processing, computer science
en_US
ethz.identifier.nebis
009959880
ethz.publication.place
Zürich
en_US
ethz.publication.status
published
en_US
ethz.leitzahl
ETH Zürich::00002 - ETH Zürich::00012 - Lehre und Forschung::00007 - Departemente::02150 - Dep. Informatik / Dep. of Computer Science::02660 - Institut für Informationssicherheit
en_US
ethz.leitzahl
ETH Zürich::00002 - ETH Zürich::00012 - Lehre und Forschung::00007 - Departemente::02150 - Dep. Informatik / Dep. of Computer Science
en_US
ethz.date.deposited
2017-06-10T23:12:58Z
ethz.source
ECOL
ethz.source
ECIT
ethz.identifier.importid
imp593651219a11921240
ethz.identifier.importid
imp59366b457d36666404
ethz.ecolpid
eth:7360
ethz.ecitpid
pub:116675
ethz.eth
yes
en_US
ethz.availability
Open access
en_US
ethz.rosetta.installDate
2017-07-06T09:07:57Z
ethz.rosetta.lastUpdated
2018-11-05T14:00:54Z
ethz.rosetta.versionExported
true
ethz.COinS
ctx_ver=Z39.88-2004&amp;rft_val_fmt=info:ofi/fmt:kev:mtx:journal&amp;rft.atitle=Adding%20support%20for%20user-defined%20sorts%20and%20sorted%20function%20symbols%20to%20Tamarin&amp;rft.date=2013&amp;rft.au=Staub,%20Cedric&amp;rft.genre=unknown&amp;rft.btitle=Adding%20support%20for%20user-defined%20sorts%20and%20sorted%20function%20symbols%20to%20Tamarin
 Search via SFX

Files in this item

Thumbnail

Publication type

Show simple item record