Verifpal

https://github.com/symbolicsoft/verifpal
Admin
Verifpal is software for verifying the security of cryptographic protocols using symbolic formal...
Tokens:9,952
Snippets:85
Trust Score:9
Update:5 months ago
Show doc for...
Tokens:
Raw
### Install Verifpal with Scoop (Windows)

Source: https://github.com/symbolicsoft/verifpal/blob/master/README.md

Install Verifpal using the Scoop package manager on Windows for automatic updates.

```bash
scoop bucket add verifpal https://github.com/symbolicsoft/verifpal.git
scoop install verifpal
```

--------------------------------

### Install Verifpal with Homebrew (Linux/macOS)

Source: https://github.com/symbolicsoft/verifpal/blob/master/README.md

Install Verifpal using the Homebrew package manager on Linux and macOS for automatic updates.

```bash
brew tap verifpal.com/source https://github.com/symbolicsoft/verifpal
brew install verifpal
```

--------------------------------

### Compile Verifpal from Source

Source: https://github.com/symbolicsoft/verifpal/blob/master/README.md

Build Verifpal from source using Cargo. Ensure Rust is installed. The binary will be in target/release/.

```bash
cargo build --release
```

--------------------------------

### Run Verifpal Tests

Source: https://github.com/symbolicsoft/verifpal/blob/master/README.md

Execute the full test suite for Verifpal using Cargo. This requires Rust to be installed.

```bash
cargo test --release
```

--------------------------------

### HKDF and AEAD Double Ratchet Example

Source: https://context7.com/symbolicsoft/verifpal/llms.txt

Demonstrates the use of HKDF for key derivation and AEAD for authenticated encryption in a double ratchet mechanism. This example models a secure communication protocol between Alice and Bob, including initial key exchange and subsequent message encryption/decryption.

```verifpal
// examples/test/double_ratchet.vp — HKDF + AEAD double ratchet
attacker[active]

principal Alice[
    knows private a_id
    ga_id = G^a_id
    generates a_eph0
    ga_eph0 = G^a_eph0
]

principal Bob[
    knows private b_id
    gb_id = G^b_id
    generates b_eph0
    gb_eph0 = G^b_eph0
]

Alice -> Bob: [ga_id], [ga_eph0]
Bob -> Alice: [gb_id], [gb_eph0]

principal Alice[
    dh_root = HASH(gb_id^a_id, gb_eph0^a_eph0)
    rk1, ck_a1 = HKDF(dh_root, nil, nil)      // multi-output HKDF
    mk_a1, _ = HKDF(ck_a1, nil, nil)
    generates msg1
    e1 = AEAD_ENC(mk_a1, msg1, ga_eph0)
]

Alice -> Bob: e1

principal Bob[
    dh_root_b = HASH(ga_id^b_id, ga_eph0^b_eph0)
    rk1_b, ck_b1 = HKDF(dh_root_b, nil, nil)
    mk_b1, _ = HKDF(ck_b1, nil, nil)
    msg1_b = AEAD_DEC(mk_b1, e1, ga_eph0)?    // checked decryption
    generates b_eph1
    gb_eph1 = G^b_eph1
    rk2_b, ck_b2 = HKDF(rk1_b, HASH(ga_eph0^b_eph1), nil)
    mk_b2, _ = HKDF(ck_b2, nil, nil)
    generates msg2
    e2 = AEAD_ENC(mk_b2, msg2, gb_eph1)
]

Bob -> Alice: [gb_eph1], e2

queries[
    confidentiality? msg1
    confidentiality? msg2
    authentication? Alice -> Bob: e1
    authentication? Bob -> Alice: e2
    equivalence? msg1, msg1_b       // Alice's msg1 == Bob's decrypted copy
    equivalence? msg2, msg2_a
]
// Expected: c0c0a0a0e1e1
```

--------------------------------

### Building and Testing Verifpal with Cargo

Source: https://context7.com/symbolicsoft/verifpal/llms.txt

These bash commands are used to build the Verifpal release binary and run its comprehensive test suite, which includes both integration and unit tests. Ensure Rust is installed before executing these commands.

```bash
# Install Rust (if needed)
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh

# Build release binary
cargo build --release
# Binary at: target/release/verifpal

# Run all tests (unit + integration)
cargo test --release
# Expected: test result: ok. 152 integration tests + 31 unit tests passed.
```

--------------------------------

### Protocol Model with Multiple Query Types

Source: https://context7.com/symbolicsoft/verifpal/llms.txt

Illustrates how to combine various query types (confidentiality, authentication, freshness, equivalence) within a single Verifpal model. This example models a protocol involving digital signatures and public-key encryption, demonstrating signature verification and re-encryption.

```verifpal
// Combining multiple query types in a single model
attacker[active]

principal Alice[
    knows private sk_alice
    generates nonce, msg
    pk_alice = G^sk_alice
    sig = SIGN(sk_alice, msg)
]

principal Bob[
    knows private sk_bob
    generates nonce_b
    pk_bob = G^sk_bob
]

Alice -> Bob: [pk_alice], nonce, msg, sig

principal Bob[
    _ = SIGNVERIF(pk_alice, msg, sig)?    // verify signature; halt on failure
    enc = PKE_ENC(pk_alice, msg)          // re-encrypt for Alice
]

Bob -> Alice: enc

principal Alice[
    msg_back = PKE_DEC(sk_alice, enc)?
]

queries[
    confidentiality? msg                      // is msg secret?
    authentication? Alice -> Bob: sig         // did Bob receive sig from Alice?
    freshness? nonce                          // is nonce fresh each session?
    equivalence? msg, msg_back                // does Alice get back what she sent?

    // Precondition: only check auth if Bob received sig from Alice on the wire
    authentication? Alice -> Bob: msg [
        precondition[Alice -> Bob: sig]
    ]
]
```

--------------------------------

### Programmatic Verification with `verify(file_path)`

Source: https://context7.com/symbolicsoft/verifpal/llms.txt

Use `verify(file_path)` to parse a model, run checks, execute scenarios, and get results. Handles all errors via `VerifpalError` variants.

```rust
use verifpal::{verify, VerifyResult};

fn main() {
    match verify("examples/simple.vp") {
        Ok((results, code)) => {
            // code = compact result string, e.g. "c1a0"
            println!("Result code: {}", code);

            for r in &results {
                if r.resolved {
                    // r.resolved == true means an attack was found (property violated)
                    println!(
                        "FAIL  {} — {}",
                        r.query.kind.name(),   // "confidentiality", "authentication", ...
                        r.summary              // human-readable attack explanation
                    );
                } else {
                    println!("PASS  {}", r.query.kind.name());
                }
            }

            // Use the result code in CI: each pair is <kind><0|1>
            // c0 = confidentiality holds, c1 = broken
            // a0 = authentication holds, a1 = broken
            assert_eq!(code, "c1a0");
        }
        Err(e) => {
            // VerifpalError::Parse, ::Sanity, ::Resolution, or ::Internal
            eprintln!("Error: {}", e);
            std::process::exit(1);
        }
    }
}
```

--------------------------------

### Verifpal Qualifiers: Password Confidentiality

Source: https://context7.com/symbolicsoft/verifpal/llms.txt

Demonstrates the use of 'password', 'private', and 'public' qualifiers in Verifpal for managing secret and guessable values. This example tests confidentiality of a password-hashed value against an attacker.

```verifpal
// examples/test/password.vp — password confidentiality
attacker[active]

principal B[]

principal A[
    knows password a          // guessable by attacker if sibling is known
    knows private b           // fully secret
    knows private z
    c = ENC(PW_HASH(a), z)    // attacker knows c (leaked below) but not z,
                               // so cannot verify password guesses → z stays confidential
    leaks a
    leaks b
    leaks c
]

A -> B: a, b, c

queries[
    confidentiality? a    // resolved: a is leaked → c0=broken (c1)
    confidentiality? b    // resolved: b is leaked → broken (c1)
    confidentiality? c    // c is leaked → broken (c1)
    confidentiality? z    // z is never leaked, sibling unknown → holds (c0)
]
// Expected result code: c1c1c1c0
```

--------------------------------

### Canonical Pretty-Printing of Verifpal Models

Source: https://context7.com/symbolicsoft/verifpal/llms.txt

The `verifpal pretty` command parses a .vp model file and re-emits it in a canonical, fully normalized format. This is useful for code review, version control diffs, and validating model well-formedness without running the analysis.

```bash
verifpal pretty examples/messaging/signal_small.vp
```

```bash
verifpal pretty my_protocol.vp > my_protocol_normalized.vp
```

--------------------------------

### Analyze Protocol Model with Verifpal CLI

Source: https://context7.com/symbolicsoft/verifpal/llms.txt

Use the `verifpal verify` command to run the full verification engine against a .vp model file. It provides a live TUI analysis log and a final summary. The `--result-code` flag suppresses the TUI for CI scripts, outputting a compact result code string.

```bash
verifpal verify examples/simple.vp
```

```bash
verifpal verify examples/simple.vp --result-code
```

```bash
verifpal verify examples/simple.vp --character jevil
```

--------------------------------

### Programmatic Verification: `verify(file_path)`

Source: https://context7.com/symbolicsoft/verifpal/llms.txt

The primary library entry point for programmatic verification. It parses a model file, runs checks, executes the attacker scenario, and returns verification results and a compact result-code string. Errors are returned as `VerifpalError` variants.

```APIDOC
## `verify(file_path)` — Programmatic verification

### Description
Parses the model, runs sanity checks, executes the attacker scenario (passive or active as specified in the model), and returns a `Vec<VerifyResult>` plus a compact result-code string. All errors are returned as `VerifpalError` variants.

### Parameters
- **file_path** (string) - Required - Path to the Verifpal model file.

### Returns
- `Ok((Vec<VerifyResult>, string))` on success, where `Vec<VerifyResult>` contains detailed results and the string is a compact result-code.
- `Err(VerifpalError)` on failure.

### Example
```rust
use verifpal::{verify, VerifyResult};

match verify("examples/simple.vp") {
    Ok((results, code)) => {
        println!("Result code: {}", code);
        for r in &results {
            if r.resolved {
                println!("FAIL  {} — {}", r.query.kind.name(), r.summary);
            } else {
                println!("PASS  {}", r.query.kind.name());
            }
        }
        assert_eq!(code, "c1a0");
    }
    Err(e) => {
        eprintln!("Error: {}", e);
        std::process::exit(1);
    }
}
```
```

--------------------------------

### Model Parsing with `parse_file` and `parse_string`

Source: https://context7.com/symbolicsoft/verifpal/llms.txt

Parse Verifpal models from files using `parse_file` or from strings with `parse_string`. Both return `VResult<Model>` and reject syntax errors.

```rust
use verifpal::parser::{parse_file, parse_string};
use verifpal::types::{AttackerKind, Block};

// From a file
let model = parse_file("examples/simple.vp").expect("parse failed");
println!("Attacker: {}", model.attacker);  // "active" or "passive"
println!("Queries: {}", model.queries.len());

// From a string (useful in editors and WASM)
let src = r#" 
attacker[passive]

principal Alice[
    knows public k
    generates m
    c = ENC(k, m)
]

principal Bob[]

Alice -> Bob: c

queries[
    confidentiality? m
]
"#;
let model = parse_string("inline.vp", src).expect("parse failed");

// Inspect parsed blocks
for block in &model.blocks {
    match block {
        Block::Principal(p) => println!("Principal: {}", p.name),
        Block::Message(msg) => println!("Message transfer"),
        Block::Phase(ph) => println!("Phase: {}", ph.number),
    }
}
// Output:
// Principal: Alice
// Principal: Bob
// Message transfer

```

--------------------------------

### Building Verifpal WASM Module

Source: https://context7.com/symbolicsoft/verifpal/llms.txt

Compile Verifpal to a WebAssembly module for web-based applications using `wasm-pack`. This command targets the web environment and enables the `wasm` feature, while disabling default features.

```bash
# Build WASM module
cargo install wasm-pack
wasm-pack build --target web --features wasm --no-default-features
```

--------------------------------

### wasm_verify(input)

Source: https://context7.com/symbolicsoft/verifpal/llms.txt

Verifies a Verifpal model string in the browser. It accepts a `.vp` model as a string and returns a JSON object containing verification results.

```APIDOC
## wasm_verify(input: &str) -> String

### Description
This function is exposed via `wasm-bindgen` when the crate is compiled with the `wasm` feature. It takes a string representing a Verifpal model (`.vp` file content) and returns a JSON string. The JSON output includes fields such as `ok` (boolean indicating success), `results` (detailed verification outcomes), `code` (a compact result code), and `messages` (log information).

### Parameters
#### Path Parameters
None

#### Query Parameters
None

#### Request Body
- **input** (string) - Required - The Verifpal model content as a string.

### Request Example
```javascript
// Assuming Verifpal WASM module is loaded and initialized
const model = `
attacker[active]

principal Alice[
    generates a
    ga = G^a
]

principal Bob[
    generates b, m
    gb = G^b
    gab = ga^b
    e = AEAD_ENC(gab, m, nil)
]

Alice -> Bob: ga
Bob -> Alice: gb, e

queries[
    confidentiality? m
    authentication? Bob -> Alice: e
]
`;

const jsonResult = wasm_verify(model);
const result = JSON.parse(jsonResult);
```

### Response
#### Success Response (200)
- **ok** (boolean) - True if verification succeeded, false otherwise.
- **results** (array) - An array of objects, each detailing a query and its outcome.
- **code** (string) - A compact string representing the overall verification result.
- **messages** (array) - An array of log messages generated during verification.

#### Response Example
```json
{
  "ok": true,
  "code": "c1a0",
  "results": [
    {
      "query": "confidentiality? m",
      "resolved": false,
      "summary": "holds"
    },
    {
      "query": "authentication? Bob -> Alice: e",
      "resolved": false,
      "summary": "holds"
    }
  ],
  "messages": [
    "Log message 1",
    "Log message 2"
  ]
}
```

### Error Handling
If `ok` is false, an `error` field will be present in the JSON response detailing the parsing or verification error.
```

--------------------------------

### Verifpal Internal JSON Interface for IDEs

Source: https://context7.com/symbolicsoft/verifpal/llms.txt

The `verifpal internal-json` command provides a machine-readable JSON interface for IDE integrations like the VS Code extension. It reads model source text from stdin (terminated with `0x04`) and accepts subcommands like `knowledgeMap` or `verify`.

```bash
cat my_model.vp | printf '%s\x04' "$(cat -)" | verifpal internal-json knowledgeMap
```

```json
{
  "Constants": [{"Name":"m1"},{"Name":"a"},{"Name":"ga"},...],
  "Creator":   ["Alice","Alice","Alice",...],
  "Assigned":  ["m1","a","G^a",...],
  "KnownBy":   [[],[], [{"Bob":"Alice"}],...],
  "Principals":["Alice","Bob"],
  "Phase":     [[0],[0],[0],...],
  "MaxPhase":  0
}
```

```bash
cat my_model.vp | printf '%s\x04' "$(cat -)" | verifpal internal-json verify
```

```json
{
  "ok": true,
  "results": [
    {"query":"confidentiality? m1","resolved":true,"kind":"confidentiality","summary":"..."},
    {"query":"authentication? Bob -> Alice: e1","resolved":false,"kind":"authentication","summary":""}
  ],
  "code": "c1a0",
  "messages": ["Attacker is configured as active.", ...]
}
```

--------------------------------

### Verifpal Phases: Testing Forward Secrecy

Source: https://context7.com/symbolicsoft/verifpal/llms.txt

Demonstrates how to use `phase[N]` blocks and `leaks` declarations in Verifpal to test forward secrecy. This models long-term key compromise after a protocol session to check if session secrets remain secure.

```verifpal
// examples/test/phase_forward_secrecy.vp — testing forward secrecy
attacker[active]

principal Alice[
    knows private a
    generates eph_a
    ga   = G^a
    geph = G^eph_a
]

principal Bob[
    knows private b
    generates m
    gb   = G^b
    gab  = ga^b           // long-term DH
    sess = HKDF(gab, nil, nil)
]

// (message exchange omitted for brevity)

phase[1]

principal Alice[leaks a]   // long-term key leaked after session
principal Bob[leaks b]

queries[
    confidentiality? m          // should hold (forward secrecy)
    authentication? Alice -> Bob: e1
    equivalence? m, m_dec
]
// Expected: c0a0e1  (confidentiality holds, auth holds, equivalence found)
```

--------------------------------

### Browser Verification with Verifpal WASM API

Source: https://context7.com/symbolicsoft/verifpal/llms.txt

Use this JavaScript code to load the Verifpal WASM module and perform verification on a given model. Ensure the WASM module is initialized before calling `wasm_verify` or `wasm_pretty`. The `wasm_verify` function returns a JSON string detailing the verification outcome, while `wasm_pretty` formats the input model.

```javascript
import init, { wasm_verify, wasm_pretty } from './verifpal_wasm.js';

await init();

const model = `
attacker[active]

principal Alice[
    generates a
    ga = G^a
]

principal Bob[
    generates b, m
    gb = G^b
    gab = ga^b
    e = AEAD_ENC(gab, m, nil)
]

Alice -> Bob: ga
Bob -> Alice: gb, e

queries[
    confidentiality? m
    authentication? Bob -> Alice: e
]
`;

const json = wasm_verify(model);
const result = JSON.parse(json);

if (!result.ok) {
    console.error("Verification error:", result.error);
} else {
    console.log("Result code:", result.code);
    // result.code example: "c1a0"

    result.results.forEach(r => {
        console.log(`${r.query}: ${r.resolved ? "ATTACK FOUND" : "holds"}`);
        if (r.resolved) console.log("  →", r.summary);
    });

    result.messages.forEach(m => console.log("[log]", m));
}

// Pretty-print the model
const prettyJson = JSON.parse(wasm_pretty(model));
if (prettyJson.ok) {
    console.log("Formatted model:
", prettyJson.output);
} else {
    console.error("Format error:", prettyJson.error);
}
```

--------------------------------

### wasm_pretty(input)

Source: https://context7.com/symbolicsoft/verifpal/llms.txt

Pretty-prints a Verifpal model string in the browser. It takes a string representing a Verifpal model and returns a JSON object with the formatted model or an error.

```APIDOC
## wasm_pretty(input: &str) -> String

### Description
This function, also exposed via `wasm-bindgen`, takes a Verifpal model string and returns a JSON string. If successful, the JSON contains an `output` field with the formatted model. If there's an error during formatting, it returns an `error` field.

### Parameters
#### Path Parameters
None

#### Query Parameters
None

#### Request Body
- **input** (string) - Required - The Verifpal model content as a string.

### Request Example
```javascript
// Assuming Verifpal WASM module is loaded and initialized
const model = `...`; // Verifpal model string
const prettyJson = wasm_pretty(model);
const formattedResult = JSON.parse(prettyJson);
```

### Response
#### Success Response (200)
- **ok** (boolean) - True if formatting succeeded, false otherwise.
- **output** (string) - The pretty-printed Verifpal model.

#### Response Example
```json
{
  "ok": true,
  "output": "Formatted model content..."
}
```

### Error Handling
If `ok` is false, an `error` field will be present in the JSON response detailing the formatting error.
```

--------------------------------

### Model Parsing: `parser::parse_file` / `parser::parse_string`

Source: https://context7.com/symbolicsoft/verifpal/llms.txt

Functions for parsing Verifpal models. `parse_file` reads from a file path, while `parse_string` parses from an in-memory string, useful for tests, editors, and WASM.

```APIDOC
## `parser::parse_file(path)` / `parser::parse_string(file_name, src)` — Model parsing

### Description
`parse_file(path)` reads a `.vp` file from disk and returns a `Model`. `parse_string(file_name, src)` parses from an in-memory string, useful for tests, editors, and the WASM interface. Both return `VResult<Model>` and reject reserved keywords, undefined primitives, and malformed syntax with `VerifpalError::Parse`.

### Parameters
- **path** (string) - Required - Path to the `.vp` model file (for `parse_file`).
- **file_name** (string) - Required - A name for the source string (for `parse_string`).
- **src** (string) - Required - The Verifpal model content as a string (for `parse_string`).

### Returns
- `Ok(Model)` on successful parsing.
- `Err(VerifpalError::Parse)` if the model syntax is malformed or contains errors.

### Example
```rust
use verifpal::parser::{parse_file, parse_string};
use verifpal::types::{AttackerKind, Block};

// From a file
let model_from_file = parse_file("examples/simple.vp").expect("parse failed");
println!("Attacker: {}", model_from_file.attacker);

// From a string
let src = r#"attacker[passive]\n\nprincipal Alice[knows public k]\nAlice -> Bob: ENC(k, m)\nqueries[confidentiality? m]\n"#;
let model_from_string = parse_string("inline.vp", src).expect("parse failed");

for block in &model_from_string.blocks {
    match block {
        Block::Principal(p) => println!("Principal: {}", p.name),
        _ => {}
    }
}
```
```

--------------------------------

### Canonical Formatter: `pretty_print(model_file)`

Source: https://context7.com/symbolicsoft/verifpal/llms.txt

Parses a Verifpal model file and re-serializes it into a canonical text form. The output is stable and idempotent, useful for consistent formatting.

```APIDOC
## `pretty_print(model_file)` — Canonical formatter

### Description
Parses and re-serializes a model to a canonical text form. The output is stable and idempotent: running it twice yields the same result. Used by `verifpal pretty` CLI and the VS Code extension's format-on-save feature.

### Parameters
- **model_file** (string) - Required - Path to the Verifpal model file to format.

### Returns
- `Ok(string)` containing the canonical formatted model content on success.
- `Err(VerifpalError)` if parsing or formatting fails.

### Example
```rust
use verifpal::pretty_print;

match pretty_print("my_protocol.vp") {
    Ok(formatted) => {
        std::fs::write("my_protocol.vp", &formatted).unwrap();
        println!("Formatted {} bytes", formatted.len());
    }
    Err(e) => eprintln!("Format error: {}", e),
}
```
```

--------------------------------

### Verifpal Guards: MITM Prevention on Long-Term Keys

Source: https://context7.com/symbolicsoft/verifpal/llms.txt

Illustrates Verifpal message guards using square brackets `[]` to prevent man-in-the-middle substitutions on specific constants, like long-term keys. This models authenticated channels or pre-shared key pinning.

```verifpal
// examples/messaging/signal_small.vp — guards prevent MITM on long-term keys
attacker[active]

principal Alice[
    knows private alongterm
    galongterm = G^alongterm
]

principal Bob[
    knows private blongterm, bs
    generates bo
    gblongterm = G^blongterm
    gbs = G^bs
    gbo = G^bo
    gbssig = SIGN(blongterm, gbs)
]

Bob -> Alice: [gblongterm], gbssig, gbs, gbo  // guard on gblongterm: Alice pins it

principal Alice[
    generates ae1
    gae1 = G^ae1
    amaster = HASH(gbs^alongterm, gblongterm^ae1, gbs^ae1, gbo^ae1)
    arkba1, ackba1 = HKDF(amaster, nil, nil)
]

// ...further message exchanges...

queries[
    confidentiality? m1
    authentication? Alice -> Bob: e1
]
// phase[1] with leaks tests forward secrecy
```

--------------------------------

### Canonical Model Formatting with `pretty_print`

Source: https://context7.com/symbolicsoft/verifpal/llms.txt

Use `pretty_print(model_file)` to parse and re-serialize a model into a stable, canonical text form. This function is idempotent and used by the CLI and VS Code extension.

```rust
use verifpal::pretty_print;

match pretty_print("my_protocol.vp") {
    Ok(formatted) => {
        // Write canonical form back to disk
        std::fs::write("my_protocol.vp", &formatted).unwrap();
        println!("Formatted {} bytes", formatted.len());
    }
    Err(e) => eprintln!("Format error: {}", e),
}
```

--------------------------------

### State Management: `reset_global_state()`

Source: https://context7.com/symbolicsoft/verifpal/llms.txt

Clears Verifpal's internal global state, which is necessary when running multiple models sequentially in the same process to prevent name collisions.

```APIDOC
## `reset_global_state()` — Multi-model process reuse

### Description
Verifpal uses global atomic maps for principal and value name interning (for performance). When running multiple models in the same process (e.g., parallel test suites or WASM workbench sessions), `reset_global_state()` must be called between model runs to clear these maps and prevent name collisions.

### Parameters
None.

### Returns
None.

### Example
```rust
use verifpal::{reset_global_state, verify};

fn run_model(path: &str, expected_code: &str) {
    reset_global_state();  // always reset before parsing a new model
    let (_, code) = verify(path)
        .unwrap_or_else(|e| panic!("verify failed for {}: {}", path, e));
    assert_eq!(code, expected_code, "FAIL {} (expected {}, got {})", path, expected_code, code);
}

fn main() {
    run_model("examples/simple.vp",             "c1a0");
    run_model("examples/test/double_ratchet.vp", "c0c0a0a0e1e1");
}
```
```

--------------------------------

### Resetting Global State with `reset_global_state()`

Source: https://context7.com/symbolicsoft/verifpal/llms.txt

Call `reset_global_state()` before running each model when processing multiple models in the same process to clear internal name-interning maps and prevent collisions.

```rust
use verifpal::{reset_global_state, verify};

fn run_model(path: &str, expected_code: &str) {
    reset_global_state();  // always reset before parsing a new model
    let (_, code) = verify(path)
        .unwrap_or_else(|e| panic!("verify failed for {}: {}", path, e));
    assert_eq!(
        code,
        expected_code,
        "FAIL {} (expected {}, got {})", path, expected_code, code
    );
}

fn main() {
    // Safe to call sequentially or in a test harness
    run_model("examples/simple.vp",             "c1a0");
    run_model("examples/test/double_ratchet.vp", "c0c0a0a0e1e1");
    run_model("examples/test/needham-schroeder-pk.vp", "a1a1c1c1");
}
```

--------------------------------

### Verifpal Model Structure: Diffie-Hellman Key Exchange

Source: https://context7.com/symbolicsoft/verifpal/llms.txt

Defines a Verifpal model for a Diffie-Hellman key exchange with AEAD encryption. It includes attacker type, principal declarations with knowledge and generation, message exchanges, and confidentiality/authentication queries.

```verifpal
// examples/simple.vp — Diffie-Hellman key exchange with AEAD
attacker[active]

principal Alice[
    knows public c0        // shared public constant
    generates a            // fresh random secret
    ga = G^a               // DH public key (equation)
]

Alice -> Bob: ga           // Alice sends her public key

principal Bob[
    knows public c0
    generates m1, b        // Bob's message and ephemeral key
    gb = G^b
    gab = ga^b             // shared DH secret
    e1 = AEAD_ENC(gab, m1, c0)  // encrypt m1 with shared key
]

Bob -> Alice: gb, e1       // Bob sends his key and ciphertext

principal Alice[
    gba = gb^a             // Alice computes the same shared secret (DH commutativity)
    e1_dec = AEAD_DEC(gba, e1, c0)?  // decrypt; ? = abort on failure
]

queries[
    confidentiality? m1                    // can the attacker learn m1?
    authentication? Bob -> Alice: e1       // did Alice receive e1 from Bob?
]
```
Tokens:
Raw