Open AccessA Formal Verification Method for Security Protocol Implementations Based on Model Learning and Tamarin
Author(s) -
Xieli Zhang,
Yuefei Zhu,
Changzhi Gu,
Xuyang Miao
Publication year - 2021
Publication title -
journal of physics. conference series
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.21
H-Index - 85
eISSN - 1742-6596
pISSN - 1742-6588
DOI - 10.1088/1742-6596/1871/1/012102
Subject(s) - implementation , computer science , protocol (science) , universal composability , cryptographic protocol , wide mouth frog protocol , vulnerability (computing) , two phase commit protocol , formal methods , theoretical computer science , programming language , computer security , cryptography , transaction processing , alternative medicine , database transaction , pathology , medicine , distributed transaction
The verification of security protocol implementations is notoriously difficult and important. In this paper, combining with the model learning using Tamarin, a formal verification tool of protocol specification, a formal verification method for security protocol implementations is proposed. We extract state machine information from protocol implementations by model learning, and determine suspicious paths in the finite-state machines by cross-validation between different implementations of the same protocol; and then verify whether the suspicious paths violate the security properties of the protocol using Tamarin. It can be used to detect logical errors in protocol implementations and avoid relying on expert experience to make compliance rules from protocol documents when using model checking tools. The effectiveness of this method is demonstrated by the vulnerability detection of the typical ChangeCipherSpec in the TLS protocol implementation. The method proposed can help developers to develop more robust implementations of security protocols.