verifpal is a programming language created in 2019.
| #1314on PLDB | 5Years Old |
// 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)
]| Feature | Supported | Token | Example |
|---|---|---|---|
| Comments | ✓ | // A comment |
|
| Line Comments | ✓ | // | // A comment |
| Semantic Indentation | X |