Type-Based Automated Verification of Authenticity in Asymmetric Cryptographic Protocols

Morten Dahl; Naoki Kobayashi; Yunde Sun; Hans Hüttel

doi:10.1007/978-3-642-24372-1_7

Type-Based Automated Verification of Authenticity in Asymmetric Cryptographic Protocols

Morten Dahl, Naoki Kobayashi, Yunde Sun, Hans Hüttel

Institut for Datalogi

Publikation: Bidrag til tidsskrift › Konferenceartikel i tidsskrift › Forskning › peer review

2 Citationer (Scopus)

Abstract

Gordon and Jeffrey developed a type system for verification of
asymmetric and symmetric cryptographic protocols.
We propose a modified version of Gordon and Jeffrey's type system
and develop a type inference algorithm for it, so that protocols can
be verified automatically as they are, without any type annotations
or explicit type casts. We have implemented a protocol verifier
SpiCa based on the algorithm, and confirmed its effectiveness.

Originalsprog	Engelsk
Bogserie	Lecture Notes in Computer Science
Vol/bind	6996
Sider (fra-til)	75-89
Antal sider	15
ISSN	0302-9743
DOI	https://doi.org/10.1007/978-3-642-24372-1_7
Status	Udgivet - 2011
Begivenhed	9th International Symposium on Automated Technology for Verification and Analysis - Taipei, Taiwan Varighed: 11 okt. 2011 → 14 okt. 2011 Konferencens nummer: 9

Konference

Konference	9th International Symposium on Automated Technology for Verification and Analysis
Nummer	9
Land/Område	Taiwan
By	Taipei
Periode	11/10/2011 → 14/10/2011

Bibliografisk note

Proceeedings of the 9th International Symposium on Automated Technology for Verification and Analysis 2011. Bultan, T. & Hsiung, P.-A. (eds.)

Adgang til dokumentet

10.1007/978-3-642-24372-1_7

AUB Link

Søg efter materialet i Aalborg Universitetsbiblioteks søgemaskine

Citationsformater

@inproceedings{54c464a28da64a389798f434664795dc,

title = "Type-Based Automated Verification of Authenticity in Asymmetric Cryptographic Protocols",

abstract = "Gordon and Jeffrey developed a type system for verification of asymmetric and symmetric cryptographic protocols. We propose a modified version of Gordon and Jeffrey's type systemand develop a type inference algorithm for it, so that protocols canbe verified automatically as they are, without any type annotations or explicit type casts. We have implemented a protocol verifier SpiCa based on the algorithm, and confirmed its effectiveness.",

author = "Morten Dahl and Naoki Kobayashi and Yunde Sun and Hans H{\"u}ttel",

note = "Proceeedings of the 9th International Symposium on Automated Technology for Verification and Analysis 2011. Bultan, T. & Hsiung, P.-A. (eds.); 9th International Symposium on Automated Technology for Verification and Analysis ; Conference date: 11-10-2011 Through 14-10-2011",

year = "2011",

doi = "10.1007/978-3-642-24372-1_7",

language = "English",

volume = "6996",

pages = "75--89",

journal = "Lecture Notes in Computer Science",

issn = "0302-9743",

publisher = "Physica-Verlag",

}

TY - GEN

T1 - Type-Based Automated Verification of Authenticity in Asymmetric Cryptographic Protocols

AU - Dahl, Morten

AU - Kobayashi, Naoki

AU - Sun, Yunde

AU - Hüttel, Hans

N1 - Conference code: 9

PY - 2011

Y1 - 2011

N2 - Gordon and Jeffrey developed a type system for verification of asymmetric and symmetric cryptographic protocols. We propose a modified version of Gordon and Jeffrey's type systemand develop a type inference algorithm for it, so that protocols canbe verified automatically as they are, without any type annotations or explicit type casts. We have implemented a protocol verifier SpiCa based on the algorithm, and confirmed its effectiveness.

AB - Gordon and Jeffrey developed a type system for verification of asymmetric and symmetric cryptographic protocols. We propose a modified version of Gordon and Jeffrey's type systemand develop a type inference algorithm for it, so that protocols canbe verified automatically as they are, without any type annotations or explicit type casts. We have implemented a protocol verifier SpiCa based on the algorithm, and confirmed its effectiveness.

U2 - 10.1007/978-3-642-24372-1_7

DO - 10.1007/978-3-642-24372-1_7

M3 - Conference article in Journal

SN - 0302-9743

VL - 6996

SP - 75

EP - 89

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

T2 - 9th International Symposium on Automated Technology for Verification and Analysis

Y2 - 11 October 2011 through 14 October 2011

ER -