Verifying implementations of security protocols by refinement
作者： Nadia Polikarpova , Michał Moskal
DOI: 10.1007/978-3-642-27705-4_5
关键词:
摘要: We propose a technique for verifying high-level security properties of cryptographic protocol implementations based on stepwise refinement. Our refinement strategy supports reasoning about abstract descriptions in the symbolic model cryptography and gradually concretizing them towards executable code. have implemented within general-purpose program verifier VCC applied it to an extract from draft reference implementation Trusted Platform Module, written C.
springer.com
researchgate.net 
sci-hub.st 参考文章(22)
Yannick Moy, Automatic modular static safety checking for C programs Paris 11. ,(2009)
K. Etessami, Analysis of Recursive Game Graphs Using Data Flow Equations verification model checking and abstract interpretation. pp. 282- 296 ,(2004) , 10.1007/978-3-540-24622-0_23
Leonardo de Moura, Nikolaj Bjørner, Z3: an efficient SMT solver tools and algorithms for construction and analysis of systems. pp. 337- 340 ,(2008) , 10.1007/978-3-540-78800-3_24
Francois Dupressoir, Andrew D. Gordon, Jan Jurjens, David A. Naumann, Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols ieee computer security foundations symposium. pp. 3- 17 ,(2011) , 10.1109/CSF.2011.8
Ernie Cohen, Markus Dahlweid, Mark Hillebrand, Dirk Leinenbach, Michał Moskal, Thomas Santen, Wolfram Schulte, Stephan Tobies, VCC: A Practical System for Verifying Concurrent C theorem proving in higher order logics. ,vol. 5674, pp. 23- 42 ,(2009) , 10.1007/978-3-642-03359-9_2
Rajeev Alur, Kousha Etessami, P. Madhusudan, A Temporal Logic of Nested Calls and Returns tools and algorithms for construction and analysis of systems. ,vol. 2988, pp. 467- 481 ,(2004) , 10.1007/978-3-540-24730-2_35
Stefan Hallerstede, Jean-Raymond Abrial, Refinement, Decomposition, and Instantiation of Discrete Models: Application to Event-B Fundamenta Informaticae. ,vol. 77, pp. 1- 28 ,(2007)
Oleg Mürk, Daniel Larsson, Reiner Hähnle, KeY-C: A Tool for Verification of C Programs Automated Deduction – CADE-21. ,vol. 4603, pp. 385- 390 ,(2007) , 10.1007/978-3-540-73595-3_27
David Aspinall, Jaroslav Ševčík, Formalising java's data race free guarantee theorem proving in higher order logics. pp. 22- 37 ,(2007) , 10.1007/978-3-540-74591-4_4
D. Dolev, A. Yao, On the security of public key protocols IEEE Transactions on Information Theory. ,vol. 29, pp. 198- 208 ,(1983) , 10.1109/TIT.1983.1056650