Using Checkable Types in Automatic Protocol Analysis

A
ACSAC
1999
15th Annual Computer Security Applications Conference (ACSAC '99)
Abstract - Using Checkable Types in Automatic Protocol Analysis

	This Article
	Subscribers, please Login Purchase article: $19 PDF IEEE Xplore Subscribers RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Stephen H. Brackin

15th Annual Computer Security Applications Conference (ACSAC '99)

Phoenix, Arizona

December 06-December 10

ISBN: 0-7695-0346-2

	ASCII Text	x
	Stephen H. Brackin, "Using Checkable Types in Automatic Protocol Analysis," Computer Security Applications Conference, Annual, pp. 99, 15th Annual Computer Security Applications Conference (ACSAC '99), 1999.

	BibTex	x
	@article{ 10.1109/CSAC.1999.816017, author = {Stephen H. Brackin}, title = {Using Checkable Types in Automatic Protocol Analysis}, journal ={Computer Security Applications Conference, Annual}, volume = {0}, year = {1999}, issn = {1063-9527}, pages = {99}, doi = {http://doi.ieeecomputersociety.org/10.1109/CSAC.1999.816017}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Computer Security Applications Conference, Annual TI - Using Checkable Types in Automatic Protocol Analysis SN - 1063-9527 SP EP A1 - Stephen H. Brackin, PY - 1999 KW - Cryptographic Protocols KW - Formal Methods KW - Automatic Analysis VL - 0 JA - Computer Security Applications Conference, Annual ER -

Stephen H. Brackin, Arca Systems / Exodus Communications

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/CSAC.1999.816017

The Automatic Authentication Protocol Analyzer, 2nd Version (AAPA2) is a fast, completely automatic tool for formally analyzing cryptographic protocols. It correctly identifies vulnerabilities or their absence in 43 of 51 protocols studied in the literature, and it finds errors in previously asserted authentication properties of two large commercial protocols. This paper describes the AAPA2 and its modeling of type, equality, and inequality tests performed by protocol participants. This description includes defining the AAPA2's Interface Specification Language, 2nd Version (ISL2), which expresses user assumptions about identifiably distinct plaintext types.

Index Terms:

Cryptographic Protocols, Formal Methods, Automatic Analysis

Citation:

Stephen H. Brackin, "Using Checkable Types in Automatic Protocol Analysis," acsac, pp.99, 15th Annual Computer Security Applications Conference (ACSAC '99), 1999

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.