VisualCPSA

A graphical tool to create models of security protocols for Formal Methods verification in CPSA (Cryptographic Protocol Shapes Analyzer).

Comment

Inspiration

In a group project for a class, we analyzed a newly-developed key exchange protocol using CPSA. The results indicated that the protocol didn't provide the desired security guarantees. The question we asked ourselves was whether there was an actual problem with the protocol, or was the problem with our interpretation and modeling of the protocol. What followed was many rounds of modifying the model, testing, analyzing the results and then modifying the model again.

A graphical tool would make that kind of iterative modeling faster and less error-prone.

What it does

VisualCPSA is a graphical tool that allows analysts to draw a protocol and generates model code based on that drawing.

How we built it

VisualCPSA is built in Python using the Tkinter GUI package.

Challenges we ran into

I have never written a "Drag and Drop" GUI program before. Neither am I an expert in the syntax of CPSA. This project challenged me to learn more about both.

Accomplishments that we're proud of

What we learned

What's next for VisualCPSA

So far, VisualCPSA can create roles and strands for the CPSA model.
The next step is to expand into skeletons and other CPSA constructs.

Built With

Share this project:

Updates