Mobile values, new names, and secure communication

被引：313

作者：

Abadi, M ^{[1
]}

Fournet, C

机构：

[1] Bell Labs, Lucent Technol, Res, Murray Hill, NJ 07974 USA

[2] Microsoft Corp, Res, Redmond, WA 98052 USA

来源：

ACM SIGPLAN NOTICES | 2001年 / 36卷 / 03期

关键词：

D O I：

10.1145/373243.360213

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We study the interaction of the "new" construct with a rich but common form of (first-order) communication. This interaction is crucial in security protocols, which are the main motivating examples for our work; it also appears in other programming-language contexts. Specifically, we introduce a simple, general extension of the pi calculus with value passing, primitive functions, and equations among terms. We develop semantics and proof techniques for this extended language and apply them in reasoning about some security protocols.

引用

页码：104 / 115

页数：12

共 45 条

[1] Secure implementation of channel abstractions
Abadi, M
Fournet, C
Gonthier, G
[J]. THIRTEENTH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 1998, : 105 - 116
[2] A calculus for cryptographic protocols: The spi calculus
Abadi, M
Gordon, AD
[J]. INFORMATION AND COMPUTATION, 1999, 148 (01) : 1 - 70
[3] Secrecy by typing in security protocols
Abadi, M
[J]. JOURNAL OF THE ACM, 1999, 46 (05) : 749 - 786
[4] Abadi M, 1998, LECT NOTES COMPUT SC, V1443, P868, DOI 10.1007/BFb0055109
[5] ABADI M, 1998, 154 DIG EQ CORP SYST
[6] ABADI M, 1998, 149 DIG EQ CORP SYST
[7] Abadi M., 2000, LECT NOTES COMPUTER, V1872, P3
[8] ABADI M, 2000, P 27 ACM S PRINC PRO, P302
[9] Amadio R., 2000, LECT NOTES COMPUTER, V1877, P380
[10] [Anonymous], 1982, 23 ANN S FDN COMPUTE, DOI DOI 10.1109/SFCS.1982.45

← 1 2 3 4 5 →