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.
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.
| Original language | English |
|---|---|
| Book series | Lecture Notes in Computer Science |
| Volume | 6996 |
| Pages (from-to) | 75-89 |
| Number of pages | 15 |
| ISSN | 0302-9743 |
| DOIs | |
| Publication status | Published - 2011 |
| Event | 9th International Symposium on Automated Technology for Verification and Analysis - Taipei, Taiwan, Province of China Duration: 11 Oct 2011 → 14 Oct 2011 Conference number: 9 |
Conference
| Conference | 9th International Symposium on Automated Technology for Verification and Analysis |
|---|---|
| Number | 9 |
| Country/Territory | Taiwan, Province of China |
| City | Taipei |
| Period | 11/10/2011 → 14/10/2011 |