Your Name
18 lines
614 B
Lean4
18 lines
614 B
Lean4
-- This module serves as the root of the `InductiveVerification` library.
|
|
-- Import modules here that should be built as part of the library.
|
|
import InductiveVerification.Basic
|
|
|
|
inductive Agent
|
|
| Server : Agent
|
|
| Friend : Nat → Agent
|
|
| Spy : Agent
|
|
|
|
inductive Msg
|
|
| Agent : Agent → Msg -- Agent names
|
|
| Number : Nat → Msg -- Ordinary integers, timestamps, ...
|
|
| Nonce : Nat → Msg -- Unguessable nonces
|
|
| Key : Key → Msg -- Crypto keys
|
|
| Hash : Msg → Msg -- Hashing
|
|
| MPair : Msg → Msg → Msg -- Compound messages
|
|
| Crypt : Key → Msg → Msg -- Encryption, public- or shared-key
|