Formal analysis of modern security protocols

Get BibTex-formatted data

Author

Yasinsac, Alec; Childs, Justin

Entry type

article

Abstract

Analyzing security protocols is notoriously difficult. In this paper, we show how a novel tool for analyzing classical cryptographic protocols can be used to model and analyze complex Internet security protocol families. CPAL-ES allows the representation of the interaction between two sub-protocols. Within a protocol such as Transport Layer Security (TLS) these are selected from a collection of sub-protocols utilized by a principal. Modeling subversion related to sub-protocol interactions is an important part of formally understanding attacks upon protocol suites. The CPAL environment contains sufficient functionality to verify the feasibility of these attacks. We also define and classify the characteristics that add complexity to modern security protocol and some impacts this complexity has on security protocol analysis. Finally, we discuss the modifications that were necessary in our formal method tool to answer this complexity and show how the tool illuminated flaws in the TLS protocol.

Date

2004 – 04 – 05

URL

http://www.sciencedirect.com

Journal

Information Sciences an International Journal

Key alpha

Yasinsac

Number

INS 7054

Publisher

Elsevier Inc.

Affiliation

Computer Science Department, Flordia State University

Publication Date

2004-04-05

Copyright

2004 by Elsevier Inc.

Keywords

Network security; Formal methods; Cryptographic protocols; Weakest preconditions

Language

English

Location

A hard-copy of this is in the Papers Cabinet

Subject

modern security protocols

BibTex-formatted data

To refer to this entry, you may select and copy the text below and paste it into your BibTex document. Note that the text may not contain all macros that BibTex supports.

@Article{ Yasinsac,
	title = "Formal analysis of modern security protocols",
	author = "Yasinsac, Alec; Childs, Justin",
	year = "2004",
	month = "04",
	journal = "Information Sciences an International Journal",
	number = "INS 7054",
	publisher = "Elsevier Inc.",
	day = "05",
	abstract = " Analyzing security protocols is notoriously difficult.  In this paper, we show how a novel tool for analyzing classical cryptographic protocols can be used to model and analyze complex Internet security protocol families.  CPAL-ES allows the representation of the interaction between two sub-protocols.  Within a protocol such as Transport Layer Security (TLS) these are selected from a collection of sub-protocols utilized by a principal.  Modeling subversion related to sub-protocol interactions is an important part of formally understanding attacks upon protocol suites.  The CPAL environment contains sufficient functionality to verify the feasibility of these attacks.
We also define and classify the characteristics that add complexity to modern security protocol and some impacts this complexity has on security protocol analysis.  Finally, we discuss the modifications that were necessary in our formal method tool to answer this complexity and show how the tool illuminated flaws in the TLS protocol.",
	affiliation = "Computer Science Department, Flordia State University",
	copyright = "2004 by Elsevier Inc.",
	keywords = "Network security; Formal methods; Cryptographic protocols; Weakest preconditions",
	language = "English",
	subject = "modern security protocols",
	url = "www.sciencedirect.com",
}