Modeling human errors in security protocols

David Basin; Sasa Radomirovic; Lara Schmid

doi:10.1109/CSF.2016.30

Modeling human errors in security protocols

David Basin, Sasa Radomirovic, Lara Schmid

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

19 Citations (Scopus)

8 Downloads (Pure)

Abstract

Many security protocols involve humans, not machines, as endpoints. The differences are critical: humans are not only computationally weaker than machines, they are naive, careless, and gullible. In this paper, we provide a model for formalizing and reasoning about these inherent human limitations and their consequences. Specifically, we formalize models of fallible humans in security protocols as multiset rewrite theories. We show how the Tamarin tool can then be used to automatically analyze security protocols involving human errors. We provide case studies of authentication protocols that show how different protocol constructions and features differ in their effectiveness with respect to different kinds of fallible humans. This provides a starting point for a fine-grained classification of security protocols from a usable-security perspective.

Original language	English
Title of host publication	2016 IEEE 29th Computer Security Foundations Symposium (CSF)
Publisher	IEEE
Pages	325-340
Number of pages	6
ISBN (Electronic)	9781509026074
DOIs	https://doi.org/10.1109/CSF.2016.30
Publication status	Published - 11 Aug 2016
Event	29th IEEE Computer Security Foundations Symposium 2016 - Lisbon, Portugal Duration: 27 Jun 2016 → 1 Jul 2016

Publication series

Name	IEEE Computer Security Foundations Symposium
ISSN (Print)	1940-1434

Conference

Conference	29th IEEE Computer Security Foundations Symposium 2016
Abbreviated title	CSF 2016
Country/Territory	Portugal
City	Lisbon
Period	27/06/16 → 1/07/16

Keywords

Formal Methods
Human Errors
Security Protocols
Usable Security

ASJC Scopus subject areas

Engineering(all)

Access to Document

10.1109/CSF.2016.30

Download pdf
© 2016 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.
Accepted author manuscript, 359 KB

Cite this

@inproceedings{3a3e45813e644a55a9f8cd29482ef19b,

title = "Modeling human errors in security protocols",

abstract = "Many security protocols involve humans, not machines, as endpoints. The differences are critical: humans are not only computationally weaker than machines, they are naive, careless, and gullible. In this paper, we provide a model for formalizing and reasoning about these inherent human limitations and their consequences. Specifically, we formalize models of fallible humans in security protocols as multiset rewrite theories. We show how the Tamarin tool can then be used to automatically analyze security protocols involving human errors. We provide case studies of authentication protocols that show how different protocol constructions and features differ in their effectiveness with respect to different kinds of fallible humans. This provides a starting point for a fine-grained classification of security protocols from a usable-security perspective.",

keywords = "Formal Methods, Human Errors, Security Protocols, Usable Security",

author = "David Basin and Sasa Radomirovic and Lara Schmid",

year = "2016",

month = aug,

day = "11",

doi = "10.1109/CSF.2016.30",

language = "English",

series = "IEEE Computer Security Foundations Symposium",

publisher = "IEEE",

pages = "325--340",

booktitle = "2016 IEEE 29th Computer Security Foundations Symposium (CSF)",

address = "United States",

note = "29th IEEE Computer Security Foundations Symposium 2016, CSF 2016 ; Conference date: 27-06-2016 Through 01-07-2016",

}

TY - GEN

T1 - Modeling human errors in security protocols

AU - Basin, David

AU - Radomirovic, Sasa

AU - Schmid, Lara

PY - 2016/8/11

Y1 - 2016/8/11

N2 - Many security protocols involve humans, not machines, as endpoints. The differences are critical: humans are not only computationally weaker than machines, they are naive, careless, and gullible. In this paper, we provide a model for formalizing and reasoning about these inherent human limitations and their consequences. Specifically, we formalize models of fallible humans in security protocols as multiset rewrite theories. We show how the Tamarin tool can then be used to automatically analyze security protocols involving human errors. We provide case studies of authentication protocols that show how different protocol constructions and features differ in their effectiveness with respect to different kinds of fallible humans. This provides a starting point for a fine-grained classification of security protocols from a usable-security perspective.

AB - Many security protocols involve humans, not machines, as endpoints. The differences are critical: humans are not only computationally weaker than machines, they are naive, careless, and gullible. In this paper, we provide a model for formalizing and reasoning about these inherent human limitations and their consequences. Specifically, we formalize models of fallible humans in security protocols as multiset rewrite theories. We show how the Tamarin tool can then be used to automatically analyze security protocols involving human errors. We provide case studies of authentication protocols that show how different protocol constructions and features differ in their effectiveness with respect to different kinds of fallible humans. This provides a starting point for a fine-grained classification of security protocols from a usable-security perspective.

KW - Formal Methods

KW - Human Errors

KW - Security Protocols

KW - Usable Security

UR - http://www.scopus.com/inward/record.url?scp=84985905255&partnerID=8YFLogxK

U2 - 10.1109/CSF.2016.30

DO - 10.1109/CSF.2016.30

M3 - Conference contribution

AN - SCOPUS:84985905255

T3 - IEEE Computer Security Foundations Symposium

SP - 325

EP - 340

BT - 2016 IEEE 29th Computer Security Foundations Symposium (CSF)

PB - IEEE

T2 - 29th IEEE Computer Security Foundations Symposium 2016

Y2 - 27 June 2016 through 1 July 2016

ER -

Modeling human errors in security protocols

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Sasa Radomirovic

Cite this

Modeling human errors in security protocols

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Profiles

Sasa Radomirovic

Cite this