Type-Based Automated Verification of Authenticity in Asymmetric Cryptographic Protocols

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

Publikation: Bidrag til tidsskriftKonferenceartikel i tidsskriftForskningpeer review

1 Citation (Scopus)

Resumé

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.
OriginalsprogEngelsk
BogserieLecture Notes in Computer Science
Vol/bind6996
Sider (fra-til)75-89
Antal sider15
ISSN0302-9743
DOI
StatusUdgivet - 2011
Begivenhed9th International Symposium on Automated Technology for Verification and Analysis - Taipei, Taiwan
Varighed: 11 okt. 201114 okt. 2011
Konferencens nummer: 9

Konference

Konference9th International Symposium on Automated Technology for Verification and Analysis
Nummer9
LandTaiwan
ByTaipei
Periode11/10/201114/10/2011

Bibliografisk note

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

Citer dette

@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.)",
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",

}

Type-Based Automated Verification of Authenticity in Asymmetric Cryptographic Protocols. / Dahl, Morten; Kobayashi, Naoki; Sun, Yunde; Hüttel, Hans.

I: Lecture Notes in Computer Science, Bind 6996, 2011, s. 75-89.

Publikation: Bidrag til tidsskriftKonferenceartikel i tidsskriftForskningpeer review

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 - Proceeedings of the 9th International Symposium on Automated Technology for Verification and Analysis 2011. Bultan, T. & Hsiung, P.-A. (eds.)

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

VL - 6996

SP - 75

EP - 89

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

SN - 0302-9743

ER -