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

Computing

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

33 Citations (Scopus)

405 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	IEEE 29th Computer Security Foundations Symposium CSF 2016
Subtitle of host publication	Proceedings
Place of Publication	Piscataway
Publisher	Institute of Electrical and Electronics Engineers
Pages	325-340
Number of pages	16
ISBN (Electronic)	9781509026074
DOIs	https://doi.org/10.1109/CSF.2016.30
Publication status	Published - 2016
Event	29th IEEE Computer Security Foundations Symposium - Fundação Calouste Gulbenkian (FCG), Lisbon, Portugal Duration: 27 Jun 2016 → 1 Jul 2016 http://csf2016.tecnico.ulisboa.pt/ (Link to Conference website)

Publication series

Name	Proceedings of the IEEE
Publisher	IEEE
ISSN (Electronic)	2374-8303

Conference

Conference	29th IEEE Computer Security Foundations Symposium
Abbreviated title	CSF 2016
Country/Territory	Portugal
City	Lisbon
Period	27/06/16 → 1/07/16
Internet address	http://csf2016.tecnico.ulisboa.pt/ (Link to Conference website)

Keywords

Formal methods
Human errors
Security protocols
Usable security

ASJC Scopus subject areas

General Engineering

Access to Document

10.1109/CSF.2016.30

Author Accepted Manuscript
© 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, 349 KB

Cite this

@inproceedings{dbdafe1adace407cb4062d6f13eb1d73,

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",

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

year = "2016",

doi = "10.1109/CSF.2016.30",

language = "English",

series = "Proceedings of the IEEE",

publisher = "Institute of Electrical and Electronics Engineers",

pages = "325--340",

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

url = "http://csf2016.tecnico.ulisboa.pt/",

}

Basin, D, Radomirovic, S & Schmid, L 2016, Modeling human errors in security protocols. in IEEE 29th Computer Security Foundations Symposium CSF 2016: Proceedings. Proceedings of the IEEE, Institute of Electrical and Electronics Engineers, Piscataway, pp. 325-340, 29th IEEE Computer Security Foundations Symposium, Lisbon, Portugal, 27/06/16. https://doi.org/10.1109/CSF.2016.30

TY - GEN

T1 - Modeling human errors in security protocols

AU - Basin, David

AU - Radomirovic, Sasa

AU - Schmid, Lara

N1 - No funding info

PY - 2016

Y1 - 2016

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 - Proceedings of the IEEE

SP - 325

EP - 340

BT - IEEE 29th Computer Security Foundations Symposium CSF 2016

PB - Institute of Electrical and Electronics Engineers

CY - Piscataway

T2 - 29th IEEE Computer Security Foundations Symposium

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

Radomirovic, Sasa

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

Radomirovic, Sasa

Cite this