Questions Columns Rows
GitHub icon

verifpal

verifpal - Programming language

< >

verifpal is a programming language created in 2019.

#1484on PLDB 4Years Old

Verifpal is new software for verifying the security of cryptographic protocols. The Verifpal language is meant to illustrate protocols close to how one may describe them in an informal conversation, while still being precise and expressive enough for formal modeling. Verifpal reasons about the protocol model with explicit principals: Alice and Bob exist and have independent states.


Example from the web:
// All lines that start with "//" are treated as comments and ignored by Verifpal // A principal block looks like the following principal SmartphoneA[ // In the line below we state that Alice knows the public BroadcastKey knows public BroadcastKey // SK is going to be a secret random value // To define it we use the "generates" keyword // We will use the following template for SK variable names // SK[day number][principal initial] generates SK0A // We will use the following template for EphID variable names // EphID[day number][value number][principal initial] EphID00A, EphID01A, EphID02A = HKDF(nil, SK0A, BroadcastKey) ]

Language features

Feature Supported Token Example
Comments
// A comment
Line Comments //
// A comment
Semantic Indentation X

View source

- Build the next great programming language · Search · Add Language · Features · Creators · Resources · About · Blog · Acknowledgements · Stats · Sponsor · Traffic · Traffic Today · Day 278 · feedback@pldb.com · Logout