On the Protocol Composition Logic PCL

A recent development in formal security protocol analysis is the Protocol Composition Logic (PCL), proposed by Datta, Derek, Mitchell, Pavlovic and Roy in [DDMP05,DDMR07]. We identify a number of unresolved problems with the current version of the logic, as well as problems with extensions of the logic as found in e.g. [HSD+05]. The identified problems imply strong restrictions on the scope of current PCL, and imply that many currently claimed PCL proofs cannot be proven within the logic, or make use of unsound axioms. Where possible, we propose solutions for these problems.