  The pi calculus is a basic theory of mobile communication based on the notion
of interaction, which, aimed at analyzing and modelling the behaviors of
communication process in communicating and mobile systems, is widely applied to
the security analysis of cryptographic protocol's design and implementation.
But the pi calculus does not provide perfect logic security analysis, so the
logic flaws in the design and the implementation of a cryptographic protocol
can not be discovered in time. The aim is to analyze whether there are logic
flaws in the design and the implementation of a cryptographic protocol, so as
to ensure the security of the cryptographic protocol when it is encoded into a
software and implemented. This paper introduces logic rules and proofs, binary
tree and the KMP algorithm, and proposes a new extension the pi calculus
theory, a logic security analysis framework and an algorithm. This paper
presents the logic security proof and analysis of TLS1.3 protocol's
interactional implementation process. Empirical results show that the new
extension theory, the logic security analysis framework and the algorithm can
effectively analyze whether there are logic flaws in the design and the
implementation of a cryptographic protocol. The security of cryptographic
protocols depends not only on cryptographic primitives, but also on the coding
of cryptographic protocols and the environment in which they are implemented.
The security analysis framework of cryptographic protocol implementation
proposed in this paper can ensure the security of protocol implementation.
