Computer-assisted verification of a protocol for certified email

被引：26

作者：

Abadi, M ^{[1
]}

Blanchet, B

机构：

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

[2] CNRS, Ecole Normale Super, Paris, France

[3] Max Planck Inst Informat, Saarbrucken, Germany

来源：

SCIENCE OF COMPUTER PROGRAMMING | 2005年 / 58卷 / 1-2期

关键词：

security protocols; protocol formal analysis;

D O I：

10.1016/j.scico.2005.02.002

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We present the formalization and verification of a recently developed cryptographic protocol for certified email. Relying on a tool for automatic protocol analysis, we establish the key security properties of the protocol. This case study explores the use of general correspondence assertions in automatic proofs, and aims to demonstrate the considerable power of the tool and its applicability to non-trivial, interesting protocols. (c) 2005 Elsevier B.V All rights reserved.

引用

页码：3 / 27

页数：25

共 18 条

[1] Analyzing security protocols with secrecy types and logic programs [J].

Abadi, M ;

Blanchet, B .

JOURNAL OF THE ACM, 2005, 52 (01) :102-146

[2]

ABADI M, 2002, 11 INT WORLD WID WEB

[3]

Bella G, 2003, LECT NOTES COMPUT SC, V2758, P352

[4]

Bella G, 1998, LECT NOTES COMPUT SC, V1485, P361, DOI 10.1007/BFb0055875

[5]

BELLA G, 1997, DIMACS WORKSH DESIGN

[6]

Bella S, 2002, 9 ACM C COMP COMM SE, P12

[7]

Blanchet B, 2003, LECT NOTES COMPUT SC, V2896, P188

[8]

Blanchet B, 2002, LECT NOTES COMPUT SC, V2477, P342

[9] An efficient cryptographic protocol verifier based on prolog rules [J].

Blanchet, B .

14TH IEEE COMPUTER SECURITY FOUNDATIONS WORKSHOP, PROCEEDINGS, 2001, :82-96

[10] Types and effects for asymmetric cryptographic protocols [J].

Gordon, AD ;

Jeffrey, A .

15TH IEEE COMPUTER SECURITY FOUNDATION WORKSHOP, PROCEEDINGS, 2002, :77-91

← 1 2 →