This repo holds a formal model of the C2PA Content Credentials system using the Cryptographic Protocol Shapes Analyzer (CPSA). Further details on our analysis of C2PA can be found in our paper here (anonymized for review).
We create five models for possible C2PA executions. All models are contained within the same file to allow comparative execution. Models, written in CPSA, are in C2PA.scm.
Models including generator0 and verifier0 demonstrate C2PA running without a timestamp.
Models including generator1 and verifier1 demonstrate C2PA running with a remote TSA service.
Models including generator3 and verifier3 demonstrate a C2PA execution where the timestamp is added as a simple manifest assertion.
Our first presented fix is for the generator to countersign the manifest. Models containing generator2 and verifier2 demonstrate C2PA running with a countersignature. Our second fix ensures that manifest assertions with timestamps cannot be stripped off by referencing the original manifest. Models containing generator4 and verifier4 demonstrate C2PA running with back-referenced manifest signatures.
The models specified for each of these scenarios produce our results. CPSA results are presented in the form of shapes. These shapes are represent all essentially unique executions of the protocol, and can be found in C2PA_shapes.xhtml. CPSA also outputs the entire search space as a text file (C2PA.txt), and the corresponding shapes for each of the attempted searches (C2PA.xhtml).
To use CPSA, follow instructions on the MITRE GitHub to install Haskell and CPSA.
After installing CPSA, this entire repo can be run from the root directory with the make command.
Old models files (.txt and .xhtml) can be removed by running make clean.
This repo also contains a demonstration of the retimestamping attack proved by CPSA. Anyone who can get a certificate, and access to a timestamp authority is able to attach their own timestamp. For more information on creating the attack, see the associated README.