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 条
  • [41] Interoperable Defensive Strategies of Network Security Evaluation
    Alarood, Ala Abdulsalam
    Alzahrani, Ahmed Omar
    [J]. IEEE ACCESS, 2024, 12 : 33959 - 33971
  • [42] Security Analysis of Smart Home Implementations
    Mahadewa, Kulani
    [J]. FORMAL METHODS AND SOFTWARE ENGINEERING, ICFEM 2018, 2018, 11232 : 450 - 454
  • [43] Security Risks in Deep Learning Implementations
    Xiao, Qixue
    Li, Kang
    Zhang, Deyue
    Xu, Weilin
    [J]. 2018 IEEE SYMPOSIUM ON SECURITY AND PRIVACY WORKSHOPS (SPW 2018), 2018, : 123 - 128
  • [44] Security risks in deep learning implementations
    Xiao, Qixue
    Li, Kang
    Zhang, Deyue
    Xu, Weilin
    [J]. arXiv, 2017,
  • [45] From security protocols to systems security
    Monahan, B
    [J]. SECURITY PROTOCOLS, 2005, 3364 : 307 - 323
  • [46] Security Analysis on InfiniBand Protocol Implementations
    Subedi, Kul Prasad
    Dasgupta, Dipankar
    Chen, Bo
    [J]. PROCEEDINGS OF 2016 IEEE SYMPOSIUM SERIES ON COMPUTATIONAL INTELLIGENCE (SSCI), 2016,
  • [47] Program Analysis of Cryptographic Implementations for Security
    Rahaman, Sazzadur
    Yao, Danfeng
    [J]. 2017 IEEE CYBERSECURITY DEVELOPMENT (SECDEV), 2017, : 61 - 68
  • [48] On the Security of Partially Masked Software Implementations
    Barenghi, Alessandro
    Pelosi, Gerardo
    [J]. 2014 11TH INTERNATIONAL CONFERENCE ON SECURITY AND CRYPTOGRAPHY (SECRYPT), 2014, : 492 - 499
  • [49] A New Security Metric for SOA Implementations
    Larson, Dave
    Liu, Jigang
    [J]. 2013 IEEE 7TH INTERNATIONAL CONFERENCE ON SOFTWARE SECURITY AND RELIABILITY - COMPANION (SERE-C), 2013, : 103 - 109
  • [50] Security management: Targets, essentials and implementations
    Zhao Jing
    Zheng Jianwu
    [J]. ADVANCES AND INNOVATIONS IN SYSTEMS, COMPUTING SCIENCES AND SOFTWARE ENGINEERING, 2007, : 211 - +
12345