Protocol composition logic

Protocol Composition Logic is a formal method that can be used for proving security properties of cryptographic protocols that use symmetric-key and public-key cryptography. PCL is designed around a process calculus with actions for various possible protocol steps (e.g. generating random numbers, performing encryption, decryption and digital signature operations as well as sending and receiving messages).

Some problems with the logic have been found, implying that some currently claimed results cannot be proven within the logic.