Expected Output: simple-proverif

This is the exact ASCII diagram and Mermaid file the crypto-protocol-diagram skill should produce when given model.pv as input.

---

Step 0 classification

Input: model.pv — ProVerif file (.pv extension, contains process, let, in/out). Input type: Spec (ProVerif).

Step S2: Parties extracted

• AliceProc → participant A as Alice
• BobProc → participant B as Bob

Step S3: Message flow (channel c)

Step S4: Crypto operations

• AliceProc: hmac(key, concat(nonce, identity)) → Note over A: mac = HMAC(k, nonce \\|\\| id)
• BobProc: new nonce → Note over B: nonce ← fresh()
• BobProc: checkhmac(mac, key, ...) → alt block (verify succeeds / fails)

Step S5: Ambiguities

• Dolev-Yao model applies: annotate with ⚠️
• Auth success sends true over c — in a real protocol this would be implicit; annotate as optional output

---

Inline ASCII Diagram

Protocol: HMAC Challenge-Response Authentication (ProVerif model)
Output:   hmac-challenge-response.md

Alice                    Bob
   |                      |
   |   -- Authentication  |  --
   |                      |
   +--------------------->|  identity
   |                      |
   |                      +--.
   |                      |  | nonce ← fresh()
   |                      |<-'
   |                      |
   |       nonce          |
   |<- - - - - - - - - - -+
   |                      |
   +--.                   |
   |  | mac = HMAC(k,     |
   |  | nonce || id)      |
   |<-'                   |
   |                      |
   +--------------------->|  mac
   |                      |
   |                      +--.
   |                      |  | checkHMAC(mac, k,
   |                      |  | nonce || identity)
   |                      |<-'
   |                      |
   |  [on verify success] |
   |                      +----.
   |                      |    | auth_ok
   |                      |<---'
   |                      |
   |  [on verify failure] |
   |                      | (abort)

⚠️ ProVerif note: all messages transit adversary network (Dolev-Yao model)

Protocol Summary

• Parties: Alice (initiator), Bob (responder/verifier)
• Round complexity: 1.5 RTT (3 messages)
• Key primitives: HMAC with shared symmetric key; fresh nonce
• Authentication: Unilateral (Alice authenticates to Bob only)
• Forward secrecy: No (static shared key k; compromise reveals all sessions)
• Notable: query attacker(k) verifies the shared key remains secret under Dolev-Yao. No mutual authentication — Bob does not prove identity to Alice.

---

Mermaid File: hmac-challenge-response.md

# HMAC Challenge-Response Authentication Sequence Diagram

```mermaid
sequenceDiagram
    participant A as Alice
    participant B as Bob

    Note over A,B: ⚠️ ProVerif Dolev-Yao model — all messages transit adversary network

    rect rgba(241, 196, 15, 0.15)
        Note over A,B: Authentication
        A->>B: identity
        Note over B: nonce ← fresh()
        B-->>A: nonce
        Note over A: mac = HMAC(k, nonce || identity)
        A->>B: mac
        Note over B: checkHMAC(mac, k, nonce || identity)
        alt verification succeeds
            Note over B: auth_ok
        else verification fails
            Note over B: abort
        end
    end
```

## Protocol Summary

- **Parties:** Alice (initiator), Bob (responder)
- **Round complexity:** 1.5 RTT (3 messages)
- **Key primitives:** HMAC with shared symmetric key; fresh nonce
- **Authentication:** Unilateral (Alice → Bob only)
- **Forward secrecy:** No
- **Notable:** No mutual authentication. `query attacker(k)` checks key secrecy.