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.^[1]

References

^ Cremers, Cas (2008), "On the Protocol Composition Logic PCL", Proceedings of the 2008 ACM symposium on Information, computer and communications security - ASIACCS '08, p. 66, arXiv:0709.1080, doi:10.1145/1368310.1368324, ISBN 9781595939791, S2CID 7618247

[1] Cremers, Cas (2008), "On the Protocol Composition Logic PCL", Proceedings of the 2008 ACM symposium on Information, computer and communications security - ASIACCS '08, p. 66, arXiv:0709.1080, doi:10.1145/1368310.1368324, ISBN 9781595939791, S2CID 7618247

[1]