This paper proposes a logic for verifying security protocols in the computational model

which can describe the computation and communication actions precisely.We present a cryptographically sound proof system on the logic and can formalize the various security properties for encryption algorithms directly.During the research

several unsoundness of the formalization with the computational protocol compositional logic in prior work is discovered

and corresponding solutions are proposed.By proving the security properties for the Needham-Schroeder-Lowe protocol

the power of the logic is demonstrated.Being different from most of the current verification approaches

this logic reasons about the security of protocols from the security of cryptographic algorithms forwardly

and is both easy to use and cryptographically sound.