Stateful Protocol Composition in Isabelle/HOL

被引:2
|
作者
Hess, Andreas V. [1 ]
Modersheim, Sebastian A. [1 ]
Brucker, Achim D. [2 ]
机构
[1] Tech Univ Denmark, DTU Compute, Richard Petersens Plads,Bldg 324, DK-2800 Lyngby, Denmark
[2] Univ Exeter, Innovat Ctr, Streatham Campus,Rennes Dr, Exeter EX4 4RN, Devon, England
基金
欧盟地平线“2020”;
关键词
Protocol composition; stateful security protocol; Isabelle/HOL; FRAMEWORK;
D O I
10.1145/3577020
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
Communication networks like the Internet form a large distributed system where a huge number of components run in parallel, such as security protocols and distributed web applications. For what concerns security, it is obviously infeasible to verify them all at once as one monolithic entity; rather, one has to verify individual components in isolation. While many typical components like TLS have been studied intensively, there exists much less research on analyzing and ensuring the security of the composition of security protocols. This is a problem since the composition of systems that are secure in isolation can easily be insecure. The main goal of compositionality is thus a theorem of the form: given a set of components that are already proved secure in isolation and that satisfy a number of easy-to-check conditions, then also their parallel composition is secure. Said conditions should of course also be realistic in practice, or better yet, already be satisfied for many existing components. Another benefit of compositionality is that when one would like to exchange a component with another one, all that is needed is the proof that the new component is secure in isolation and satisfies the composition conditions-without having to re-prove anything about the other components. This article has three contributions over previous work in parallel compositionality. First, we extend the compositionality paradigm to stateful systems: while previous approaches work only for simple protocols that only have a local session state, our result supports participants who maintain long-term databases that can be shared among several protocols. This includes a paradigm for declassification of shared secrets. This result is in fact so general that it also covers many forms of sequential composition as a special case of stateful parallel composition. Second, our compositionality result is formalized and proved in Isabelle/HOL, providing a strong correctness guarantee of our proofs. This also means that one can prove, without gaps, the security of an entire system in Isabelle/HOL, namely the security of components in isolation and the composition conditions, and thus derive the security of the entire system as an Isabelle theorem. For the components one can also make use of our tool PSPSP that can perform automatic proofs for many stateful protocols. Third, for the compositionality conditions we have also implemented an automated check procedure in Isabelle.
引用
收藏
页数:36
相关论文
共 50 条
  • [1] Importing HOL into Isabelle/HOL
    Obua, Steven
    Skalberg, Sebastian
    AUTOMATED REASONING, PROCEEDINGS, 2006, 4130 : 298 - 302
  • [2] Stateful Protocol Composition
    Hess, Andreas V.
    Modersheim, Sebastian A.
    Brucker, Achim D.
    COMPUTER SECURITY (ESORICS 2018), PT I, 2018, 11098 : 427 - 446
  • [3] An interpretation of Isabelle/HOL in HOL Light
    McLaughlin, Sean
    AUTOMATED REASONING, PROCEEDINGS, 2006, 4130 : 192 - 204
  • [4] Safety and Conservativity of Definitions in HOL and Isabelle/HOL
    Kuncar, Ondrej
    Popescu, Andrei
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2018, 2 (POPL):
  • [5] Unifying Theories in Isabelle/HOL
    Feliachi, Abderrahmane
    Gaudel, Marie-Claude
    Wolff, Burkhart
    UNIFYING THEORIES OF PROGRAMMING, 2010, 6445 : 188 - +
  • [6] Random testing in Isabelle/HOL
    Berghofer, S
    Nipkow, T
    PROCEEDINGS OF THE SECOND INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, 2004, : 230 - 239
  • [7] Nominal techniques in Isabelle/HOL
    Urban, Christian
    JOURNAL OF AUTOMATED REASONING, 2008, 40 (04) : 327 - 356
  • [8] Data Refinement in Isabelle/HOL
    Haftmann, Florian
    Krauss, Alexander
    Kuncar, Ondrej
    Nipkow, Tobias
    INTERACTIVE THEOREM PROVING, ITP 2013, 2013, 7998 : 100 - 115
  • [9] A comparison of PVS and Isabelle/HOL
    Griffioen, D
    Huisman, M
    THEOREM PROVING IN HIGHER ORDER LOGICS, 1998, 1479 : 123 - 142
  • [10] From LCF to Isabelle/HOL
    Paulson, Lawrence C.
    Nipkow, Tobias
    Wenzel, Makarius
    FORMAL ASPECTS OF COMPUTING, 2019, 31 (06) : 675 - 698