Protocol composition logic

Protocol Composition Logic is a formal method that is used for proving security properties of protocols that use symmetric key and Public key cryptography. PCL is designed around a process calculi with actions for possible protocol steps like generating some random number, perform encryption and decryption, send and receive messages and digital signature verification actions. Some problems with the logic have been found implying that some currently claimed proofs cannot be proven within the logic.