Computer Science

Directed Research Project Details

SPINGenerator: a Tool for Automatic Construction of Promela Programs for Cryptographic Protocols

Abstract

Cryptographic protocols are widely used in modern communiation. However, it is not easy to desin a cryptographic protocol correctly. Model checking is one of the formal methods to help detect flaws in a cryptographic protocol, and Spin is one of the model checkers used with the input of Promela programs. However, in practice, writing a Promela program for Spin takes much effot, and sometimes is error-prone. It seems benefitial to create a tool to automate the process of writing Promela program. In my DRP presentation, I will explain the problems in manually coding Promela program, and how these steps are automated via a tool, SPINGenerator. In current implementation, SPINGenerator has limited applicable domain.