Verified Interoperable Implementations of Security Protocols

被引：30

作者：

Bhargavan, Karthikeyan ^{[1
]}

Fournet, Cedric ^{[1
]}

Gordon, Andrew D. ^{[1
]}

Tse, Stephen ^{[1
]}

机构：

[1] Univ Penn, Philadelphia, PA 19104 USA

来源：

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS | 2008年 / 31卷 / 01期

关键词：

Languages; Security; Theory; Verification; Functional programming; pi calculus; Web services; XML security;

D O I：

10.1145/1452044.1452049

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We present an architecture and tools for verifying implementations of security protocols. Our implementations can run with both concrete and symbolic implementations of cryptographic algorithms. The concrete implementation is for production and interoperability testing. The symbolic implementation is for debugging and formal verification. We develop our approach for protocols written in F#, a dialect of ML, and verify them by compilation to ProVerif, a resolution-based theorem prover for cryptographic protocols. We establish the correctness of this compilation scheme, and we illustrate our approach with protocols for Web Services security.

引用

页数：61

共 50 条

[1] Verified reference implementations of WS-security protocols
Bhargavan, Karthikeyan
Fournet, Cedric
Gordon, Andrew D.
[J]. WEB SERVICES AND FORMAL METHODS, PROCEEDINGS, 2006, 4184 : 88 - 106
[2] Sound Verification of Security Protocols: From Design to Interoperable Implementations
Arquint, Linard
Wolf, Felix A.
Lallemand, Joseph
Sasse, Ralf
Sprenger, Christoph
Wiesner, Sven N.
Basin, David
Mueller, Peter
[J]. 2023 IEEE SYMPOSIUM ON SECURITY AND PRIVACY, SP, 2023, : 1077 - 1093
[3] Provable implementations of security protocols
Gordon, Andrew D.
[J]. 21ST ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2006, : 345 - 346
[4] Verifying Implementations of Security Protocols by Refinement
Polikarpova, Nadia
Moskal, Michal
[J]. VERIFIED SOFTWARE: THEORIES, TOOLS, EXPERIMENTS, 2012, 7152 : 50 - +
[5] Bulwark: Holistic and Verified Security Monitoring of Web Protocols
Veronese, Lorenzo
Calzavara, Stefano
Compagna, Luca
[J]. COMPUTER SECURITY - ESORICS 2020, PT I, 2020, 12308 : 23 - 41
[6] Formally sound implementations of security protocols with Java']JavaSPI
Sisto, Riccardo
Copet, Piergiuseppe Bettassa
Avalle, Matteo
Pironti, Alfredo
[J]. FORMAL ASPECTS OF COMPUTING, 2018, 30 (02) : 279 - 317
[7] AnBx: Automatic generation and verification of security protocols implementations
School of Computing Science, Newcastle University, Newcastle upon Tyne, United Kingdom
[J]. Lect. Notes Comput. Sci., (156-173):
[8] AnBx: Automatic Generation and Verification of Security Protocols Implementations
Modesti, Paolo
[J]. FOUNDATIONS AND PRACTICE OF SECURITY (FPS 2015), 2016, 9482 : 156 - 173
[9] An analysis of conformance issues in implementations of standardized security protocols
Izquierdo, Antonio
Sierra, Jose M.
Torres, Joaquin
[J]. COMPUTER STANDARDS & INTERFACES, 2009, 31 (01) : 246 - 251
[10] Introduction to the special session on wireless protocols security & hardware implementations
Sklavos, N
[J]. MELECON 2004: PROCEEDINGS OF THE 12TH IEEE MEDITERRANEAN ELECTROTECHNICAL CONFERENCE, VOLS 1-3, 2004, : 757 - 758

← 1 2 3 4 5 →