Analyzing security protocols with secrecy types and logic programs

被引：76

作者：

Abadi, M

Blanchet, B

机构：

[1] Univ Calif Santa Cruz, Dept Comp Sci, Santa Cruz, CA 95064 USA

[2] Ecole Normale Super, Dept Informat, CNRS, F-95005 Paris, France

来源：

JOURNAL OF THE ACM | 2005年 / 52卷 / 01期

关键词：

languages; security; theory; verification; cryptographic protocols; logic programming; process calculi; secrecy properties; typing;

D O I：

10.1145/1044731.1044735

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

We study and further develop two language-based techniques for analyzing security protocols. One is based on a typed process calculus; the other, on untyped logic programs. Both focus on secrecy properties. We contribute to these two techniques, in particular by extending the former with a flexible, generic treatment of many cryptographic operations. We also establish an equivalence between the two techniques.

引用

页码：102 / 146

页数：45

共 55 条

[1] Abadi M, 2004, LECT NOTES COMPUT SC, V2986, P340
[2] Secrecy types for asymmetric communication
Abadi, M
Blanchet, B
[J]. THEORETICAL COMPUTER SCIENCE, 2003, 298 (03) : 387 - 415
[3] Abadi M, 2003, LECT NOTES COMPUT SC, V2694, P316
[4] A calculus for cryptographic protocols: The spi calculus
Abadi, M
Gordon, AD
[J]. INFORMATION AND COMPUTATION, 1999, 148 (01) : 1 - 70
[5] Secrecy by typing in security protocols
Abadi, M
[J]. JOURNAL OF THE ACM, 1999, 46 (05) : 749 - 786
[6] Abadi M, 2000, NATO ADV SCI I F-COM, V175, P39
[7] ABADI M, 2001, P 28 ACM S PRINC PRO, P104, DOI DOI 10.1145/373243.360213
[8] Abadi M., 2002, P 11 INT C WORLD WID, P387
[9] AIELLO W, 2002, P 9 ACM C COMP COMM, P48
[10] Amadio R., 2000, LECT NOTES COMPUTER, V1877, P380

← 1 2 3 4 5 6 →