Overview

Owl is a programming language and proof assistant designed to help developers build cryptographic security protocols with mathematical guarantees of correctness and security.

The intended workflow of Owl is as follows: first, the developer writes a protocol in the Owl language, which uses information-flow and refinement types to specify and prove security. Then, the protocol can be extracted using our compiler into a high-performance implementation in Verus, an extension of Rust with formal verification capabilities, that is guaranteed by construction to be functionally correct and secure against source-level side channels.

The repository for Owl can be found here.

Owl's Design

The Owl language is backed by two main programming language technologies: information-flow types, which reasons about the secrecy information of data in the program; and refinement types, which use SMT solvers (we use Z3) to imbue types with logical specifications.

The key novelty of Owl is that information-flow and refinement types, on their own, are not enough. We also need to faithfully model the security guarantees of cryptographic operations, such as encryption. To do this, Owl's type system comes with a soundness proof that every well-typed protocol is cryptographically secure.

In addition to formal verification of protocol designs, Owl also enables protocol developers to automatically extract real-world code that one can link with. Our compiler, described in our USENIX Security paper, uses Verus to compile Owl protocols into efficient, interoperable, side-channel resistant Rust libraries that are automatically formally verified to be correct.

Comparisons between Owl and Other Tools

There are two classes of verification tools which Owl intersects with: game-hopping cryptographic provers, based on relational program logics, such as EasyCrypt; and "security protocol verifiers", such as CryptoVerif and Tamarin.

Compared to EasyCrypt, Owl is less general but significantly more automated. EasyCrypt allows the user to prove arbitrary cryptographic theorems using an expressive probabilistic logic; on the other hand, Owl is specifically targeted at security protocols, such as WireGuard HPKE.

Compared to CryptoVerif and Tamarin, the advantage of Owl is that its type system guarantees the properties of computational security, compositionality, and a high degree of proof automation.

Calling Owl

Owl is a Haskell package, built with cabal. Run cabal run owl to see options for the executable. If developing a protocol, the most useful option is --log-typecheck:

cabal run owl -- test.owl --log-typecheck

which will output debug and progress information.

Owl by Example: Encrypted Key

We begin with an example: suppose Alice and Bob already have a pre-shared key, psk, and want to use it to exchange a data key, k_data. so that later on, they can use k_data to exhange a secret nonce x:

A, B already have key psk 

A -> B : {k_data}_psk 

B -> A : {x}_(k_data)

A : retrieve x

First, Alice sends Bob an encryption of k_data under psk. In return, Bob sends Alice an encryption of x under k_data. After recieving Bob's message, Alice can obtain the value of x by decrypting Bob's message using k_data.
While this protocol is simple, it naturally scales to real-world use cases, such as the protocol underlying Kerberos.

We will describe the Owl version of the protocol in sections. The full protocol is given here. We can run and typecheck this protocol via cabal run owl -- docs/encrypted_key_basic.owl.

To encode this protocol in Owl, we first specify the localities, which comprise the parties of the protocol:

locality alice
locality bob

Next, we specify the names for the protocol. Names correspond to cryptographic secrets, such as keys and nonces. There are three names for our protocol: psk, k_data, and x. The corresponding name declarations are given below:

name x : nonce @ bob
name k_data : enckey Name(x) @ alice 
name psk : enckey Name(k_data) @ alice, bob

Name Declarations

Name declarations are of the form name N : nt @ L, where N is the identifier for the name, nt is a name type, and L is a set of localities. The localities constrain where the name is randomly sampled and stored. Names which are stored at two localities, such as psk, correspond to a trusted joint setup, while names stored at one locality, such as k_data, may be sampled lazily whenever they are needed.

Name Types

Name types constrain how the name is sampled and how it may be used. We see two name types above: nonce, which corresponds to opaque, random data; and enckey t, which corresponds to an authenticated symmetric encryption key (e.g., AES-GCM) for data of type t. Additional name types include sigkey t for signing keys, mackey t for message authentication codes (MACs), and DH, for Diffie-Hellman keys.

Encryption Keys in Owl

The name type enckey t contains a type, t, for the underlying data the key is meant to encrypt. In our example, psk encrypts data of type Name(k_data). Here, Name(n) is a singleton type for the value of name n; thus, our protocol will maintain and enforce that (unless psk is corrupt) that valid ciphertexts under psk only contain k_data, and nothing else. Similarly, k_data only may encrypt the value of x.

Structs and Enums

Data types in Owl, in addition to the Name(n) type, can express arbitrary structs and enums. Our protocol uses a Result enum, defined below:

enum Result {
    | SomeResult Name(x)
    | NoResult
}

Currently, enums may have either zero or one pieces of data attached to constructors.

The Protocol: Alice

One of the main novel features of Owl is that procedures for different parties may be type checked independently. As long as Alice's code satsifies the key constraints given by the name declarations, we are guaranteed that Alice is secure. So, let's begin the protocol with the code for Alice:

1: def alice_main () @ alice : if sec(k_data) then Result else Data<adv> = 
2:    let c = samp enc(get(psk), get(k_data)) in
3:    output c;
4:    input i in // i : Data<adv> 
5:    corr_case k_data in
6:    let res = dec(get(k_data), i) in 
7:    case res {
8:        | Some j => SomeResult(j)
9:        | None => NoResult()
10:   }

Line 1 defines alice_main, the main procedure for Alice. Other than the name, we know it's Alice's procedure since it's annotated with the locality alice. We'll get back to the type annotation for alice_main in a little bit.

First, Alice needs to encrypt k_data under psk; this is done in Line 2. The expression samp enc(x, y) performs an encryption of plaintext y under key x. The key and plaintext are given by get(psk) and get(k_data); here, get(N) retrieves the locally known value of name N. The get(N) operation requires that we are currently in a valid locality for N. (Thus, since x is stored only at bob, perfoming get(x) in Alice's code would raise an error).

Input and Output

Next, Line 3 performs an output, which sends the value c to the network. In Owl, we protect security against an attacker who we assume controls the entire network. Indeed, Alice and Bob cannot talk to each other directly, but only through the attacker-controlled network.

After outputting the ciphertext, Alice moves to the second stage, where she gets a message from Bob and attempts to decrypt it. Line 4 performs an input expression, retrieving a message from the network and binding it to i. Since the attacker controls the network, we don't have any guarantee about the value of i, other than it came from the attacker; thus, i has type Data<adv>, which stands for arbitrary public data, possibly controlled by the attacker. Here, adv is a label, which is used to specify information flow properties. We'll explain labels below.

The central invariant of Owl is that all data flowing in an out of the attacker has label Data<adv>. Thus, Owl checks in Line 3 that c has type Data<adv> as well.

Labels, Decryption and `corr_case`

Now, Alice needs to perform the decryption using k_data. Since all cryptography in Owl is strongly typed, we expect that the result of decryption will have the type corresponding to k_data's name type, Name(x).

However, this is not the case if k_data is obtained by the attacker (e.g., the attacker gains access to Alice's local disk to read k_data). We model this capability of the attacker by allowing it to corrupt a set of names before protocol execution. This set of names is given by the information flow label, adv. Labels are intuitively sets of names, along with the symbolic label adv for the adversary: L ::= 0 | [n] (where n is a name) | L /\ L | adv Labels support a flows-to partial order, L1 <= L2, which says if the set of dependencies in L1 is captured by L2.

If the name k_data is corrupt, then when Alice decrypts i under k_data, we shouldn't expect the result to be x; for example, the attacker could encrypt its own nonce under k_data instead! This is reflected in the type we compute for res, in Line 6: res : if sec(k_data) then Option (Name(x)) else Option(Data<adv>).

This type means that either k_data is secret (meaning that [k_data] !<= adv) and res : Option(Name(x)), or k_data is corrupt (i.e., [k_data] <= adv) and res : Option(Data<adv>).

To reason about the protocol, we split the type checking into two cases, depending on whether k_data is corrupt. This is done in Line 5: corr_case k_data. The corr_case command is often needed when performing decryptions, signature verifications, etc. (If you don't perform a needed corr_case, you'll get an error message about the query [k_data] <= adv being inconclusive.)

Finally, we perform a pattern match on res in Lines 7-9. Because of the previous corr_case, this pattern match is checked twice -- once for when k_data is secret, and once for when it's corrupt.

In the secret case, we have that res : Option(Name(x)). Thus, when res is Some j, we have that j : Name(x), and thus SomeResult(j) has type Result.

The corrupt case is more subtle. We have that res : Option(Data<adv>), under the assumption that [k_data] <= adv; thus, when we match res against Some j, we have that j : Data<adv>. In this case, the constructor SomeResult(j) also has type Data<adv>. Essentially, all function symbols in Owl can be thought of having two typing rules: a strongly typed one, where the types match up as expected:

j : Name(x)
-----------
SomeResult(j) : Result

and an overapproximating one, where we instead overapproximate all types with Data<L>, the type of arbitrary data with label L:

j : Data<L>
-----------
SomeResult(j) : Data<L>

The second branch is well-typed when k_data is corrupt, since NoResult() is a constant, and hence has type Data<L> for any L.

At the end of the procedure, we have that Alice returns one of two possible types, depending on adv:

If [k_data] !<= adv, then we return a value of type Result;
If [k_data] <= adv, then we return a value of type Data<adv>.

These two return types unify with the annotated return type of alice_main, if sec(k_data) then Result else Data<adv>, since this return type normalizes to the corresponding side under one of the two assumptions above on the adversary.

The code for Bob is similar, and can be seen in the source file here.

Hierarchical Label Model

Labels in Owl represent per-name dataflow dependencies. Since psk encrypts k_data, and k_data encrypts x, our name declarations induce the following flows:

[x] <= [k_data]
[k_data] <= [psk]

Two labels L1 and L2 are considered equivalent whenever L1 <= L2 and L2 <= L1. Thus, we have that [x] /\ [k_data] = [k_data].

Hierarchical Corruption

Since labels form a partial order, and corruption is defined via the flows-to relation, we have that corruption is hierarchical as well. For example, if psk is corrupt, then we have that x is as well, since [x] <= [k_data] <= [psk] <= adv.

Complete Example

/* 
    A, B already have key k

    A -> B : {k_data}_k

    B -> A : {x}_(k_data)

    A : retrieve x
*/

locality alice
locality bob

name x : nonce @ bob
name k_data : enckey Name(x) @ alice 
name psk : enckey Name(k_data) @ alice, bob 

enum Result {
    | SomeResult Name(x)
    | NoResult
}

def alice_main () @ alice
     : if sec(k_data) then Result else Data<adv> = 
    let c = aenc(get(psk), get(k_data)) in
    output c to endpoint(bob);
    input i in 
    corr_case k_data in
    let res = adec(get(k_data), i) in 
    case res {
     | Some j => SomeResult(j)
     | None => NoResult()
    }
    
def bob_main () @ bob : Unit =
    input i in // i : Data<adv>
    corr_case psk in
    case adec(get(psk), i)  {
     | Some k => 
        let c = aenc(k, get(x)) in
        output c to endpoint(alice)
     | None => ()
    }

Syntax

Below serves as a reference to the syntax of Owl.

Overview

Owl is composed of specification-level objects, such as names and (data) types, and expressions, which are meant to be run.

The specification-specific syntax of Owl is stratified in a number of layers:

names, which are type-level cryptographic keys;
labels, which drive Owl's information-flow typing rules;
types, which specify the types of data; and
name types, which can be thought of as specifications for names (as types are specifications for data).

Names

Names in Owl are cryptographic keys which are reflected to the type level. Names can either be base names, given by an identifier (e.g., n), or derived names of the form KDF<...>(...) (explained below).

Base names are created by a name declaration:

name k : nt @ loc

where nt is a name type and loc is a locality. In an expression, you can obtain the value of k by calling get(k) (this will not work if the code is running at a different locality than the name, however). The type of get(k) is Name(k) (explained below).

Name declarations (among other things) can be indexed, as so:

name k<i, j @ k> : enckey t @ loc<k>

This creates a name k indexed by two session IDs, i and j, and a party ID k. All indices may be used in the type t, but only party IDs may be used in the associated locality.

KDF Names

Aside from assuming names as input to the protocol, names can also be derived via a call to a key derivation function. Owl currently supports HKDF. A secure output of HKDF results in value of type Name(KDF<nk_1 || ... || nk_n; i; nt>(a, b, c)). Details about the KDF operation and KDF name are specified here.

Name Types

Each name in Owl has a name type, which is intuitively the cryptographic permissions that the corresponding key is allowed to be used for. Each cryptographic operation has a corresponding name type.

Grammar

Names:

N ::= n // Base name
   |  n<i@j> // Indexed name
   |  KDF<nk_1 || ... || nk_n; i; nt>(a, b, c) // KDF Name

Name Types:

Below is an (incomplete) list of some name types supported by Owl:

DH, for Diffie-Hellman;
nonce, for random, unstructured secrets
nonce |LC|, for random, unstructured secrets where |LC| is a length constant;
sigkey T, for signing keys;
enckey T, for encryption keys;
pkekey T, for public encryption keys;
mackey T, for MAC keys;
NT<..>(x, y, .., z) for name type abbreviations. Here, <..> contains (optional) index parameters; while x, y, ..., z are arguments given as atomic expressions;
st_aead ..., for stateful AEAD details here;
kdf ... and dualkdf ... for KDF keys details here.

Labels

Labels form the basis of Owl's information flow analysis. The two most important labels are name labels and the adversary labels. If N is a name, then [N] is the label associated to N. (For example, get(N) has label [N]). The adversary label, adv, is the label for public data. Owl labels form a semilattice, meaning that there is a binary operation /\ between labels that constructs the least upper bound of the two labels.

Here is an example piece of code that exercises labels:

locality alice
name n : nonce @ alice
name m : nonce @ alice

def foo() @ alice : Unit = 
    input i in 
    let j : Data<adv> = i in 
    let x : Data<[n]> = get(n) in 
    let y : Data<[m]> = get(m) in 
    let z : Data<[n] /\ [m]> = x ++ y in 
    ()

After defining two names n and m, we take an input i from the network inside of foo. We then assign i to j, and give it the type Data<adv>; this type represents "data labelled at adv". Hence, x has type Data<[n]>, y has type Data<[m]>, and x ++ y has type Data<[n] /\ [m]> (since we are combining x and y through concatenation).

Indexed joins of labels

In more complicated code, one might have an indexed name n<i> and need to represent the label for data that depends on some n<i>, but we don't know which one. In this case, one can use an indexed join:

locality alice
name n<i> : nonce @ alice

def foo<i>() @ alice : Unit = 
    input i in 

    let x : Data<[n<i>]> = get(n<i>) in 
    let y : Data</\_k [n<k>]> = x in 
    ()

Here, the label /\_k [n<k>] is the join over all labels of the form [n<k>], for all k.

Information Flow Ordering

Given two labels L1 and L2, the proposition L1 <= L2 states that label L1 flows to L2. The bottom of the information flow lattice is static (so static flows to everything).

We use the information flow order to define corruption. We say that the name n is corrupt if [n] <= adv, and is secret otherwise (which we write as [n] !<= adv).

A central part of Owl is that the information flow ordering is influenced by crytographic primitives. If n is an encryption key for data labeled at L, then we get that L <= [n]. More details are given when discussing cryptographic operations.

Grammar

L ::= [N]
    | static
    | adv
    | L /\ L
    | /\_i L   // Join over index

In addition to the above, there are a few labels internal to the implementation of Owl --- top and ghost --- but these can be safely ignored in user code.

Types

Cryptographic security in Owl is expressed via types. Owl types can be thought of as having two components: a secrecy component, expressed using information-flow labels; and an integrity component, expressed using refinement and singleton types. As is common in information-flow type systems, Owl types support subtyping, which states when data in one type can be considered to have another type.

Basic Types

Logically, all data in Owl are bytestrings --- even structs and enums, which should be thought of as holding their parsed representations (where structs have their field concatenated, and enums are implicitly tagged unions).

Data Types

Suppose L and L' are labels, and a is an atomic expression. Then, the types Data<L>, Data<L, |L|> and Data<L> |a| all represent arbitrary data (i.e., bytestrings) with various secrecy and integrity information.

The type Data<L> represents arbitrary data with secrecy L.
The type Data<L, |L'|> represents arbitrary data with secrecy L, where the length of that data has label L'. This is mostly used in the form Data<L, |adv|>, which represents public-length data.
The type Data<L> |a| represents data with secrecy L, where the length of that data is statically known to have length equal to the value of a. The most common use case here is where a is a constant: e.g., Data<adv> |32|, for 32-byte length data, or Data<adv> | |nonce| |, where |nonce| is the constant for the length of a nonce name.

The above types use the information-flow lattice to define the subtyping order. For example, Data<L> is a subtype of Data<L'> whenever `L <= L'.

A unifying principle of Owl is that all data are bytestrings. Thus, the (non-ghost component

Unit and Lemma

The type Unit (with distinguished element ()) behaves as it does in other languages. Importantly, however, the Unit type can be refined, just as any other type can be. Thus, we can say things like:

locality alice

def foo(x : Data<adv>, pf : (_:Unit{x != 0x1234})) @ alice : Unit = 
    ()

Here, we refine the Unit type with a proof that x is not equal to 0x1234. (We could have refined x as well, but it is often convenient to detatch the proof from the data). In this special case, we can also type:

def foo(x : Data<adv>, pf : Lemma{x != 0x1234}) @ alice : Unit = 
    ()

Here, Lemma{P} is sugar for _:Unit{P}.

Bool

If L is an information flow label, then Bool<L> is the type of booleans with secrecy level L. Just like with Data, Bool respects subtyping with respect to the level L.

To express arbitrary integrity properties, Owl supports refinement types. If T is a type, and P is a proposition that mentions x : T, then x:T{P} is a type. Refinement types in Owl behave similarly to F*, and are checked using an SMT solver.

Structs, Enums, and Option Types

Owl supports byte-precise data types via structs and enums.

Structs

Below is a simple struct, used in our formalization of WireGuard:

// And the transport layer message
struct transp {
      _transp_tag : Const(0x04000000)
    , _transp_receiver : Data<adv> |4|
    , _transp_counter  : Data<adv> | |counter| | 
    , _transp_packet   : Data<adv> 
}

A struct is defined by a number of fields, specified by an identifier and a type. The naming scheme we use here for each field (_struct_field) is not necessary, but useful for namespacing. The first field here has a const type, while the next two are data types refined with a length, and the last is simply public data. While the above struct is used for a network format, Owl structs can also be used for internal data structures for protocols, such as a record of the most recently derived secret keys.

Dependent Structs

The types in structs can depend on previous values:

locality alice

struct ne_pair {
    x : Data<adv> | 2 |, 
    y : (z:Data<adv> | 2 | {z != x}) 
}

def foo() @ alice : Unit = 
    let v : ne_pair = ne_pair(0x1234, 0x5678) in  // OK 
    let v2 : ne_pair = ne_pair(0x1234, 0x1234) in  // Fails to type check
    ()

Invalid Structs (and other data)

Since all data in Owl are byte strings, building a struct may have meaning even if the corresponding type refinements in the struct do not hold. We model this through the following strategy: applying invalid arguments to a function results in the information-flow approximation to their type. In the case of structs, this is justified since a constructor for a struct in Owl's semantics is simply a function which concatenates its arguments together.

We can see this here:


// tst.owl

locality alice

name n : nonce @ alice

struct ne_pair {
    x : Data<adv> | 2 |, 
    y : (z:Data<adv> | 2 | {z != x}) 
}

def foo() @ alice : Unit = 
    let v : ne_pair = ne_pair(0x1234, 0x5678) in 
    let v2 = ne_pair(get(n), 0x) in  // 0x = empty byte string
    debug printTyOf(v); 
    debug printTyOf(v2); 
    ()

When we run the above code with cabal run owl -- tst.owl --log-typecheck, we get the following output:

  Type for v: ne_pair
  Type for v2: .res:(Data<[n]>){.res == ne_pair(get(n), 0x)}

Here, v is a valid ne_pair (because all relevant subtyping queries succeeded), while v2 is not. In this case, Owl simply re-interprets ne_pair as the concatenation function.

In the type refinement for v2, we see that Owl remembers that the value of v2 is equal to ne_pair(get(n), 0x). (In type refinements, ne_pair is interpreted as a pure function on byte strings.)

(Details for the debug expression are given here.)

Parsing

Since a value of type ne_pair is regarded as a specially formatted byte string, we do not destruct it via . syntax, as one does in C. Instead, we have parse statements:

locality alice

name n : nonce @ alice

struct ne_pair {
    x : Data<adv> | 2 |, 
    y : (z:Data<adv> | 2 | {z != x}) 
}

def foo() @ alice : Unit = 
    let v : ne_pair = ne_pair(0x1234, 0x5678) in 
    parse v as ne_pair(a, b) in 
    ()

More details are given below.

Singleton Types

A singleton type is a type with exactly one inhabitant. Other than unit, Owl uses singleton types pervasively to reason about type refinements.

Const

Given a fixed byte sequence, such as 0x1234, Const(0x1234) is the singleton type for exactly that byte sequence. Such a type is useful to specify tags in TLV formats, for example. Since 0x1234 is a hardcoded constant, this type is a subtype of Data<static>.

Name

A name type is a specification for a name, and is part of a name declaration. For example:

locality alice
name n : nonce @ alice
name k : enckey Name(n) @ alice

Here, nonce and enckey Name(n) are name types. Each name type is in one-to-one correspondence to a keyed cryptographic primitives. More details are given here.

Exists Types

If-then-else types

If p is a proposition, and t1 / t2 are types, then if p then t1 else t2 is a type. If Owl can prove that p holds (or doesn't hold), then this type will automatically simplify to t1 (respectively, t2).

If-then-else types are most useful for specifying the return types of procedures that depend on whether something is corrupted. For example:

locality alice
locality bob

name n : nonce
name K : enckey Name(n)

def server (k : Name(K)) @ bob : if sec(K) then Option Name(n) else Option Data<adv> = 
    input i in 
    adec(k, i)

The return type of the server states that if the name K is a secret, we get a value of type Option Name(n) (i.e., a value which is either None or Some(v), where v = get(n)); if K is corrupt, then we get Option Data<adv>. This is achieved using authenticated encryption.

Ghost

It is often useful to add information to a data structure that only exists for proof purposes. An example of this is given below:


name eph : DH @ alice
name n : nonce @ alice 

struct stage2_t {
    recvd_eph_pk : Ghost,
    val : if recvd_eph == dhpk(get(eph)) then  Name(n) else Data<adv>
}

Here, we have a pair of two values: the first, which has no runtime representation, represents a received ephemeral public key. The second has an if-then-else type which states that the val is equal to get(n) if the ephemeral key is the expected one, and arbitrary junk data otherwise.

Grammar of Types

t ::=  
    | Data<L>
    | Data<L> |aexpr| 
    | Data<L, |L|> // L : Label
    | Ghost
    | x:t{phi} // phi : Prop
    | Option t
    | s // where s is a struct or enum
    | if prop then t else t
    | Bool<L> // L : Label
    | Unit
    | Name(n) // n : Name
    | vk(n) // n : Name, n must have name type sigkey t for some t
    | dhpk(n) // n : Name, n must have name type DH
    | encpk(n) // n : Name, n must have name type pkekey t
    | shared_secret(n, m) // n, m : Name, must have name type DH
    | exists i. t // binds an index i in t
    | Const(HC) // HC is a hex constant, eg 0x1234

Localities

Localities specify the parties of the protocol. Every compiled name declaration and def must be attached to a locality. Localities for a single party are declared simply as

locality alice

while a family of localities (e.g., specifying a protocol between $n$ servers and clients) are specified with an arity, like so:

locality Server : 1
locality Client : 1

Here, the 1 represents the number of party IDs the locality takes as input. For example, we may declare this:

name n<@j> : nonce @ Server<j>

to mean that each server stores a single name; while this:

name n<i@j> : nonce @ Server<j>

means that each server Server<j> stores a family of names n<i,j>. Here, i is a session ID; party IDs and session IDs are detailed in indices.

Indices

To handle protocols with a polynomial number of parties, or a polynomial number of sessions for each party, Owl has a notion of an index. Indices can be thought of as type-level numbers (albeit ones that cannot be added, but just passed around). Indices come in three types: party IDs, which are used to index a collection of parties (e.g., the ith client); session IDs, which are used to index within a computation carried out by a single locality (e.g., the ith Diffie-Hellman computation done by a particular party); and ghost indices, which only have proof content.

We introduce indices during computations by having index arguments to defs:

locality Server : 1
name n<i@j> : nonce @ Server<j>
def client_main<i@j>(x : Name(n<i@j>)) @ Server<j> : Unit = 
    let y = get(n<i@j>) in 
    assert (x == y);
    ()

First, we have a locality with an arity 1, meaning it takes one party ID. Then, we have the indexed name n<i@j>, which takes a session ID i and a party ID j. (The @ symbol separates session IDs from party IDs). Index arguments are then introduced after the method name during a def.

Structs and enums can also be indexed:

locality Server : 1
name n<i@j> : nonce @ Server<j>

struct MyStruct<i,j> {
    v : Name(n<i@j>)
}

def client_main<i@j>(s : MyStruct<session i,pid j>) @ Server<j> : Unit = 
    ()

Due to a current design limitation, the syntax for indices is a bit different for structs and enums.
Indices are introduced into struct declarations without regard for their type (thus, we have <i,j> instead of <i@j>). When making reference to a struct type (e.g., for MyStruct), one must then annotate the index type (hence, we have MyStruct<session i, pid j>.)

Propositions

A proposition is a proof-level property that may be true or false. Propositions in Owl are checked using an SMT solver. We can see them at work here:

locality alice

def client(x : Data<adv> |2|, y : Data<adv> |2|, z : Data<adv> |2|, w : Data<adv> |2| ) @ alice : Unit = 
    assert (123 == 123);
    assert ((concat(x, y) == concat(z, w)) ==> (x == z));
    ()

Assert statements carry propositions, and fail to type check if the SMT solver fails to prove that the proposition is always true. We can see in the second line that the SMT solver can be used to prove nontrivial facts, such as the fact that concatenation is injective (when appropriate side conditions on lengths hold).

Propositions can show up in refinement types, if-then-else types, assert/assume expressions, and pcase expressions, among other places.

Predicates

A predicate is a proposition-level macro. An example is below:

locality alice

predicate ok(v) = 
    (v == 0x1234 \/ v == 0x2345)

def foo(x : (v:Data<adv>{ok[v]})) @ alice : Unit = 
    assert (x != 0x5555);
    ()

Predicates do not require type annotations on its arguments, since at the level of propositions, all values are bitstrings. Note that when we apply ok, we must use square brackets (such as ok[v]); this is a current limitation of the parser.

Grammar

p ::= // prop
    | True
    | False
    | corr(N) // N : Name. N is corrupt; same as [N] <= adv
    | sec(N) // N : Name. N is secret; same as [N] !<= adv
    | let x = a in p // a : atomic expr
    | a1 == a2 // a1, a2 : atomic expr
    | a1 != a2 // a1, a2 : atomic expr
    | i1 =idx i2 // i1, i2 : index
    | i1 !=idx i2 // i1, i2 : index
    | l1 <= l2 // l1, l2 : label
    | l1 !<= l2 // l1, l2 : label
    | happened(foo<..>(x, y, ..., z)) // foo is a method name; <..> are index parameters (optional); x, y, .., z are arguments (atomic exprs)
    | forall x : idx, y : idx, ..., z : idx. p // x, y, z are identifiers
    | forall x : bv, y : bv, ..., z : bv. p // x, y, z are identifiers
    | aad(N)[a] // N : Name, a : atomic expr
    | in_odh(a, b, c) // a, b, c : atomic expr
    | honest_pk_enc<N>(a) // N : Name, a : atomic expr
    | foo<...>[x, y, .., z] // foo is a predicate; <..> are index  parameters (optional); x, y, .., z are arguments (atomic exprs)
    | a // a : atomic expr. Implicit cast to (a == true)

Expressions

Computations in Owl are carried out by expressions. Expressions are stratified into two levels: atomic expressions, which represent pure computations; and effectful expressions. Note that in Owl, cryptographic operations are considered effectful.

Atomic Expressions

Atomic expressions represent pure computations, and can thus arise up in type-level constructs such as propositions.

Length Constants

When specifying (for example) data formats, it is important to know the length of an encryption key. For this purpose, Owl supports the syntax |LC|, where LC here is the name for a length constant. For example, type Data<adv> | |nonce| | is parsed as follows:

Data<adv> | a | is a type, whenever a is an atomic expression;
|nonce| is an atomic expression, since nonce is the name for a length constant (which specifies the length of names of type nonce).

The supported length constants currently are:

nonce; for the length of get(N) if N : nonce;
DH, for the length of get(N) if N : DH. Note that this is a Diffie-Hellman secret (i.e., exponent), not a group element;
enckey; for the length of get(N) if N : enckey T;
pke_sk; for the length of get(N) if N : pkekey T;
sigkey; for the length of get(N) if N : sigkey T;
kdfkey; for the length of get(N) if N is a KDF key
mackey; for the length of get(N) if N : mackey T;
signature; for the length of the result of sign;
pke_pk; for the length of enc_pk(x) when x is a secret key for public-key encryption (i.e., has type Name(N) if N : pkekey T);
vk; for the length of vk(x) when x is a signing key (i.e., has type Name(N) if N : sigkey T);
maclen; for the length of a MAC computed by mac
tag; for the length of an enum tag (typically one byte);
counter; for the length of a counter, used primarily by authenticated encryption;
crh; for the length of a collision-resistant hash;
group; for the length of a group element.

User-defined functions

In Owl, we can define funcs, which are atomic expression-level macros. A mininal example is below:

locality alice

func make_foo(x) = 
    x ++ 0x1234

def foo() @ alice : Unit =
    input i in
    output make_foo(i)

Grammar

a ::= // atomic expr
    | a * a // integer multiplication
    | a ++ a // concatenation
    | a1 &&& a2 // if a1 : Lemma p1, and a2 : Lemma p2, then a1 &&& a2 : Lemma (p1 /\ p2)
    | a1 && a2 // Boolean conjunction
    | a1 + a2  // integer addition
    | !a // Boolean negation
    | () // unit
    | true
    | false 
    | "<alphanum>" // Strings
    | 0x<hexConst> // Hex const; e.g., 0x1234. 0x is the empty hex constant.
    | <natural>    // Integers; e.g., 67. 
    | | LC | // Length constants, where LC is a name of a length constant. 
    | gkdf<nks; j>(a, b, c) // KDF operation in Ghost. nks is a row of name kinds (separated by ||); j is an integer index into this row, and a, b, c are atomic exprs.
    | get(N) // obtain the value of a base name N.
    | get_encpk(N) // obtain the public key for N, if N : Name corresponds to a public encryption key.
    | get_vk(N) // obtain the verification key for N, if N : Name corresponds to a signing key.
    | f<...>(x, y, .., z) // apply function symbol f to arguments x, y, ..., z : atomic expr. Inside <...> are _function parameters_ (used mainly for index arguments to constructors for structs and enums).
    | x // x is a variable

Assert/assume

Case-Splitting on a Proposition

Pattern Matching

Parsing Structs

Case Analysis on Enums

Debug Expressions

Declarations

Above, we have seen examples of declaring names, methods via def (see here and here), structs and enums, and localities. Below, we outline a number of additional top-level declarations used in Owl protocols.

Type and Name Type definitions

One can give abbrevations for both types and name types:

locality alice
locality bob

nametype my_nonce = nonce

name m : my_nonce @ alice 

type my_msg_t = Name(m)

def client(v : my_msg_t) @ alice : Unit = 
    assert (v == get(m));
    ()

Name type abbreviations may also carry index arguments:

locality alice
name m<i> : nonce @ alice

nametype my_key<i> = enckey Name(m<i>)

name k<i> : my_key<i> @ alice

def client<i>(my_k : Name(k<i>)) @ alice : Unit = 
    let c = aenc(my_k, get(m<i>)) in
    ()

Corruption declarations

It is often necessary to restrict the adversary model by asserting that certain names are known to the adversary by default. We do this with a corruption declaration, which is as follows:

locality alice

name n : nonce @ alice
name m : nonce @ alice

corr [n] ==> [m] // If n is corrupt, m is as well

All corruption declarations in Owl are hypothetical, and have the form corr L1 ==> L2; this emits the axiom that if L1 <= adv, then L2 <= adv. One can add non-hypothetical corruption axioms by letting the left-hand side be adv:

locality alice

name n : nonce @ alice
corr adv ==> [n]

The above constructs a name n which Owl trusts is randomly generated, but readable by the adversary.

Corruption declarations can be indexed:

locality alice

name n<i> : nonce @ alice 
name m<i> : nonce @ alice 

corr<i> [m<i>] ==> [n<i>]

ODH Declarations

To associate Diffie-Hellman shared secrets with hash permissions, one can use an ODH declaration. More detail is given here.

Counter Declarations

Owl has a notion of a monotonic counter, which is used primarily for authenticated encryption (but can be used for other purposes). An example is given below:

locality alice

counter C @ alice

def foo() @ alice : Unit = 
    inc_counter C; // Increments the counter by one
    let x : (v:Data<adv>{length(v) == |counter|}) = get_counter C in 
    ()

Counters support two operations: inc_counter, which increments it by one; and get_counter, which returns the current value of the counter. Owl doesn't currently model that the counter is monotonic, but the fact that we cannot reset or decrement the counter guarantees monotonicity. More details are given here.

Predicate Declarations

Details here.

Func Declarations

Details here

Cryptographic Operators

Authenticated Encryption

In Owl, symmetric encryption is performed via authenticated encryption. We assume IND-CPA, INT-CTXT, and Key Privacy, which together state that encryptions under a correctly sampled secret key leak nothing about the message or the key other than the message's length. (See The Owl paper for more details.) These are reasonable assumptions for modern ciphers, such as AES-GCM or ChaCha20-Poly1305.

There are two closely associated cryptographic abstractions Owl uses for symmetric encryption. The first, simply given by the name type enckey T (where T is a type), is "textbook" encryption, where encryption takes two arguments --- the key and the message --- and decryption similarly takes two arguments --- the key and the ciphertext. In this "textbook" version, the nonce used by the symmetric cipher is randomly generated as part of compilation (and canonically appended to the ciphertext).

[!NOTE] Owl proves asymptotic security, which means that security issues arising from sampling the same nonce twice are out of scope. For this reason, the user should be aware of the concrete cipher implementation being used along with domain considerations when using textbook encryption.

In the second version, we allow more precice control via a stateful AEAD primitive. In this version, the Owl program is able to use a monotonically increasing counter for encryption, and associate an AAD (additional authenticated data) to each ciphertext. This is the encryption scheme that is used for WireGuard.

Textbook Encryption

To obtain an encryption key, declare a name with enckey T as its name type, where T is a type. Note that since encryption does not hide message lengths, T cannot hold secret lengths.

To encrypt, use aenc(k, m) where k is the key, and m is the message. This operation is well typed under the following two scenarios:

If k : Name(N) where N : enckey T, N is a secret (i.e., [N] !<= adv), and m : T, then the result has type c:Data<adv>{length(c) == cipherlen(m)};
If k and m are both public (i.e., subtype into Data<adv>), then the result is public and has no additional properties. Note that if k : Name(N) but N is corrupt (i.e., [N] <= adv), then k : Data<adv>.

Above, cipherlen(m) is the function which statically computes the length of a symmetric ciphertext given the length of m. Owl does not assume any particular axioms about cipherlen. For example, cipherlen(m) could be 4 + length(m) due to a four-byte tag for authentication.

On the other side, to decrypt, use adec(k, c) where k is the key, and c is the ciphertext. This operation is well typed under the following two scenarios:

If k : Name(N) where N : enckey T, N is a secret, and c : Data<adv>, we return Option T;
If k : Name(N) where N : enckey T, and N is corrupt, and c is public, we return Option Data<adv>; and
If k and c are both public (but k is not necessarily a key), we return Data<adv>.

A complete example is given in tests/success/encrypted_key.owl.

Stateful AEAD

An AEAD scheme, such as ChaCha20-Poly1305, has the following interface: in addition to the key and message, the encryptor also provides a nonce N and associated data (AAD). (Note that this notion of a nonce is different than Owl's use of the term "nonce" for opaque, random data.) For security, the nonce must not be reused for different encryptions.

In return, encryption provides a ciphertext and and authentication tag, which Owl packages together. On the other side, the decryptor must provide not only the key and ciphertext/tag pair, but also the nonce N and AAD being used.

Since the nonce cannot be reused, modern protocols, such as WireGuard and HPKE, typically implement the nonce using a monotonically increasing counter which the two parties maintain separately. Some protocols (such as HPKE) additionally hide the nonce by XORing it with unique randomness each encryption, providing an anonymity guarantee.

Owl can handle both of these scenarios.

Simple Monotonic Counter for Nonce

We will begin by first describing how Stateful AEAD is used with a simple increasing counter. First, let's look at the name declarations:

locality alice
locality bob

counter N @ alice
counter N_recv @ bob

name m : nonce @ alice // Just for defining the type of message to encrypt.

name k : st_aead Name(m)
            aad x. (x == 0x1234)
            nonce N 
          @ alice, bob

Before defining the encryption key, we need to define a counter. The important one here is N, which is the counter used for encryption. (The counter N_recv will be used for decryption; we will return to this later.) We can see this in the name type for the encryption key k; in addition to the type being encrypted (here, Name(m)) we also see two additional pieces of metadata. The aad field aad x. (x == 0x1234) states that we are only allowing encryptions where the AAD is exactly 0x1234; and the nonce field N states that we are using N for encryption.

Now, let's look at the way we encrypt:

def client() @ alice : Unit = 
    let c =  st_aead_enc<N>(get(k), get(m), 0x1234) in 
    output c;
    ()

To encrypt, we use the cryptographic operation st_aead_enc, which takes one argument in angle brackets --- the name of the counter used for encryption --- and three ordinary arguments, for the key, message, and AAD. Whenever we call st_aead_enc, the extracted protocol will read the current value of N, use that for the encryption nonce, and increment N as part of encryption; in this way, we guarantee by construction that all nonces used are unique.

Just as in textbook encryption, the typing rules are split according to whether the key k is secret. We additionally require that if k is secret, the AAD must be correct. Additionally, since the counter N is compiled to local state, we require that st_aead_enc<N>(...) is only called at locality alice.

Now, looking at decryption:

def server(my_aad : Data<adv>) @ bob : Unit = 
    input c in
    let ctr = get_counter N_recv in 
    inc_counter N_recv;
    corr_case k in
    case st_aead_dec(get(k), c, my_aad, ctr) {
        | Some x => assert(sec(k) ==> (x == get(m) /\ my_aad == 0x1234))
        | None => ()
    }

For the purpose of demonstration, we have the server take the AAD my_aad as input. (In reality, the AAD would either be computed before decryption, or perhaps packaged in a struct alongside the ciphertext.) We see that st_aead_dec takes four arguments, instead of two: the key, ciphertext, AAD, and counter. To retrive the counter, we call get_counter N_recv. We then increment the counter using inc_counter N_recv. (Since we only require the counter is unique per encryption, it is always sound to read and increment the counter.) If decryption succeeds and the key is secret, the server learns that the message is authentic and the AAD predicate is true.

Using a Pattern for Fine-Grained Nonce Control

In certain protocols (such as HPKE) we don't want to have the nonce be verbatim the counter, but instead a function of the counter. This allows, for example, the counter's value to be randomly offset by a base (via an XOR).

We support this style of nonce in the following way:

locality alice
locality bob

counter N @ alice
counter N_recv @ bob

name m : nonce @ alice // just for defining the type of message

name base : nonce |counter| @ alice, bob 

corr adv ==> [base]

name k : st_aead Name(m)
            aad x. (x == 0x1234)
            nonce N
            // optionally: a pattern for the counter
            pattern i. xor(i, get(base)) 
        @ alice, bob

The difference is we now have a name base, with type nonce |counter|. This name type is similar to the regular nonce type, but is required to have length of counters (written |counter|), rather than the default length of nonces, |nonce|. Via a corr declaration, we require that the base is public. We then declare st_aead with a pattern, which states how the counter should be transformed before encrypting. Here, we transform the nonce by XORing it with the base. For the pattern to be accepted by Owl, Owl must verify that it is injective.

Now, for encryption and decryption:

def client() @ alice : Unit = 
    let my_base = get(base) in 
    let c =  st_aead_enc<N, pattern i. xor(i, my_base)>(get(k), get(m), 0x1234) in 
    output c;
    ()

def server() @ bob : Unit = 
    input c in 
    let base = get(base) in 
    let ctr = get_counter N_recv in 
    corr_case k in 
    case st_aead_dec(get(k), c, 0x1234, xor(ctr, base)) {
        | Some x => assert(sec(k) ==> (x == get(m) ))
        | None => ()
    }

For encryption, we must add the pattern to the call to enc_st_aead. Note here that the pattern may involve local computations (such as my_base); Owl verifies that the pattern given is equivalent to the pattern attached to the key. For decryption, we simply pass the derived nonce directly to st_aead_dec.

[!NOTE] The purpose of XORing the counter with a base is to provide anonymity; as such, HPKE asserts that the base should be secret. However, for Owl, the counter must be public, since the ordinary security model of AEAD assumes public counters.

Signatures

Public Key Encryption

MACs

Diffie-Hellman and HKDF

Most protocols performing key exchange include key derivation, where secret keys are created out of (a combination of) prior protocol secrets. Owl supports reasoning about key derivation via a type-based model of HKDF, the dominant key derivation algorithm used in modern protocols.

Background on HKDF

The HKDF algorithm (combining the extract and expand phases) takes four arguments:

A salt;
An IKM (Input Keying Material);
An info, for contextual information; and
A desired length, N.

Given these arguments, HKDF deterministically outputs N bytes. The security guarantees assumed of HKDF are complex, but we outline them here. Technically, Owl assumes that HKDF is a Dual-PRF (is a PRF when keyed either in salt or IKM position); and that the PRF-ODH assumption holds for HKDF. Intuitively, given an HKDF call res = HKDF(salt, info, ikm, N), we assume that the output res is computationally indistinguishable from uniform to an attacker:

When the salt is uniformly random, and secret; OR
The IKM contains secret uniform randomness; OR
The IKM contains a Diffie-Hellman shared secret, where both Diffie-Hellman keys are secret.

We assume that the info may be public and adversarially-controlled.

Additionally, in certain instances, the HKDF algorithm is allowed to leak values of the form HKDF(salt, h^x, ikm, N) to the adversary, even when x is a secret and h is adversarially-chosen. (This is the PRF-ODH assumption).

Name Types for HKDF

Intuitively, there are three different ways of using HKDF (often which are used simultaneously): with a uniform secret in salt position; with a uniform secret in IKM position; and with a Diffie-Hellman secret in IKM position. The first two cases are handled by a special name type, while the latter is handled by a special declaration.

Uniform Secrets in Salt Position: `kdf` type

To specify an HKDF secret in salt position, one uses the following name type:

name k : kdf {ikm info.
    PROPERTY_1 -> NAME ROW_1, 
    ...
    PROPERTY_k -> NAME ROW_k
} @ ...

where PROPERTY_i is a proposition that can make use of the variables ikm and info (referring to the other arguments to the current HKDF call); and each NAME ROW has the following syntax:

nt ::= .. // name type
<annotation> := public | strict
ELEM ::= nt | <annotation> nt
NAME ROW ::= ELEM || ... || ELEM

Thus each NAME ROW is a list of ELEMs, separated by ||. Each ELEM is a name type, with an optional annotation. As is hinted here, and outlined below, KDF calls result in fresh Owl names for each (secret) input given. Each name type appearing in a KDF name type must be a uniform one (e.g., nonce or enckey, and not, for example a signing key); this corresponds to the assumption that HKDF outputs uniform randomness.

An example name declaration KDF type is below:

name k : kdf {ikm info.
    (info == 0x01) -> enckey Name(alice1),
    (info == 0x02) -> strict kdf {ikm info.
        (info == 0x01) -> enckey Name(alice2),
        (info == 0x02) -> kdf {ikm info.
            (info == 0x01) -> enckey Name(alice3)
        }
    }
} @ alice, bob

This declares a shared key k such that:

If it is hashed with an info = 0x01, it produces an encryption key for Name(alice1);
If it is hashed with an info = 0x02, it produces a strict KDF key such that:
- If hashed with info = 0x01, it produces an encryption key for Name(alice2); and
- If hashes with info = 0x02, produces a KDF key such that:
  - If hashed with info = 0x01, produces an encryption key for Name(alice3).

The complete example can be found here.

Uniform Secrets in IKM Position: `dualkdf` type

To specify a uniform secret in IKM position, one uses the dualkdf nametype:

name k2 : dualkdf {salt info.
    PROPERTY_1 -> NAME ROW_1, 
    ...
    PROPERTY_k -> NAME ROW_k
} @ ...

It is exactly the same as the kdf type above, except binds the value of salt and info instead of ikm and info.

Name Annotations for HKDF

There are two annotations that one can place on each name type inside of a KDF: public, and strict. The public annotation simply says that the result of the hash should be considered a public piece of randomness (similarly to how we can use corr declarations to assume a given name is public).

The strict annotation has to do with Owl's information flow assumptions about the output name from the HKDF call. If the name n is returned by the KDF call kdf<...>(x, y, z) (and hence there is a genuine secret in x or y, as described below), by default, Owl does not assume that n is a secret. This behavior may be desired if one is modeling a corruption scenario where one hashes a secret using ephemeral information, stores the resulting key on disk, and then the attacker gains access to the disk.

However, in certain secruity analyses, it may be desirable to assume that if we hash secrets, then the result is automatically a secret. This can be achieved by annotating the name type with strict.

`self` parameter for `kdf`/`dualkdf`

In addition to the arguments ikm/info and salt/info for kdf and dualkdf respectively, one can also optionally make reference to the key being defined using self:

nametype shared_secret_t = 
    kdf {ikm info self. 
        ... // Here, self is equal to the key being defined
    
    }

This is useful, for example, to make reference to a "sibling" hash in a hash chain. However, such a self parameter should be used with caution, as it is still experimental.

ODH Declarations

The third way to declare that a secret is suitable for calling HKDF is an ODH declaration, standing for Oracle Diffie-Hellman. An example ODH declaration is given below:

locality alice

name X : DH @ alice
name Y : DH @ alice

name n : nonce @ alice

odh L : 
    X, Y -> {salt info.
        salt == 0x -> strict enckey Name(n)
    }

To use odh, one first needs two names of name type DH. Then, we give an identifier for the ODH declaration (here, L). Then, after specifying the two names X and Y, and after the ->, we have the same syntax as a dualkdf name.

Calling KDF

Owl Compiler

Owl features a compiler pipeline that translates well-typed Owl programs into efficient Rust code that is machine verified (using Verus) to be correct and secure. Using Owl, you can produce bit-precise models of protocols that adhere to specified cipher suite choices and binary network formats, in addition to the strong security guarantees provided by our typechecker.

The Owl compiler (also known as "OwlC" or "Owl extraction") is described in detail in our USENIX Security 2025 publication; this document provides guidance on how to use the Owl compiler and its generated output, and how to model implementation-level details such as cipher suite choices and message formats.

Running the compiler

The artifact for our USENIX Security 2025 publication, available here, provides a Docker image containing all the dependencies required to run the Owl compiler and verify its output. The artifact evaluation appendix in that archive provides instructions on how to set up and use the Docker image. For those using this repository from source, you'll need to use the following instructions.

Prerequisites. Follow the setup in README.md to install cabal, ghc, and z3. Rust's cargo tool, the verus binary, and verusfmt must also be available in PATH when you run the verification script.
Compilation command. From the repository root run:
```
cabal run owl -- --extract path/to/protocol.owl
```
The verifier type-checks your protocol first. On success, the compiler emits a Rust crate under extraction/<protocol-stem>/.
Output layout. The compiled Rust crate is in the extraction/ subdirectory. The Owl compiler will generate extraction/src/lib.rs, while all other files in extraction/src/ contain libraries of helper routines (e.g., code for cryptographic primitives). We also provide run_verus.sh, a script that orchestrates running Verus and verusfmt to verify the generated Rust crate. A full representative example crate in client_example/extraction/.

Verifying the output with Verus

Change into the extraction directory:
```
cd extraction
```
Execute the provided script, passing the workspace root:
```
./run_verus.sh $PWD
```
The script orchestrates running Verus to check the proof obligations for the generated Rust module; it also runs Verus's autoformatter, verusfmt, to prettify the generated code. Ensure verus, verusfmt, and required Rust targets are installed; the script will exit with a non-zero status if verification fails.

Iterating. When you re-run the compiler, it overwrites the crate root extraction/src/lib.rs. Re-run Verus after every change to the Owl source to re-verify the generated output.

Owl length constants

Owl's source language lets you specify the length of byte buffers: the Data type for byte buffers may optionally carry a length refinement. As well as non-negative integers, Owl provides built-in length constants that you can use in type annotations and length expressions. These constants represent the sizes of cryptographic keys or data, and are automatically resolved to concrete byte values during compilation. The following constants are available:

|group|: Length of a Diffie-Hellman group element. Used for DH private/public keys and shared secrets.
|enckey|: Length of an authenticated encryption key. Used for symmetric encryption keys.
|kdfkey|: Length of a key derivation function output. Used for KDF-derived keys.
|mackey|: Length of a MAC key. Used for message authentication code keys.
|nonce|: Length of a nonce. Used for IVs for symmetric encryption. The nonce name type in Owl can also carry a customized length, e.g., nonce |8|.
|tag|: Length of an AEAD authentication tag.
|maclen|: Length of a MAC output. Used for MAC values.
|counter|: Length of a counter value (8 bytes little-endian, by default). Used for stateful AEAD counters.
|sigkey|: Length of a digital signature private key. Used for digital signature keys.
|pkekey|: Length of a public-key encryption private key. Used for PKE keys.

These constants can be used in length annotations like Data<adv> | |group| | or in length expressions like cipherlen(|group|). The compiler resolves them to concrete numerical values based on the configured cipher suites.

The cipherlen(n) function computes the length of an AEAD ciphertext given a plaintext length n, adding the authentication tag size (typically 16 bytes for ChaCha20Poly1305): cipherlen(n) = n + TAG_SIZE.

Customising cipher suites

Owl’s runtime library currently hosts implementations of cryptographic in extraction/src/execlib.rs. The compiler must assume specific parameter sizes when setting struct layouts, so changing cipher suites currently requires updates in two locations:

Runtime crypto module (extraction/src/execlib.rs).
- Update CIPHER, HMAC_MODE, and related constructors to select the desired primitives (for example, switch from Chacha20Poly1305 to Aes256Gcm).
- Ensure helper functions (owl_aead::*, owl_hmac::*, HKDF glue, etc.) route into implementations that match your choice. If you replace or extend the crypto back-end, maintain the same function signatures used by the generated code (owl_enc, owl_dec, owl_mac, ...). You can add additional Rust libraries by modifying Cargo.toml.
Hard-coded length table (src/Extraction/ExtractionBase.hs).
- Update concreteLength so that constants such as ENCKEY_SIZE, NONCE_SIZE, MACKEY_SIZE, and TAG_SIZE reflect the new primitive. This mapping controls the combinator sizes the compiler bakes into the generated proofs. A mismatch between the runtime library and these constants will cause Verus verification to fail or, worse, produce unsound assumptions.

After both changes, re-run the compiler and Verus to confirm the pipeline remains consistent.

Binary message formats and Vest

Owl protocols communicate over the network by exchanging binary messages. The compiler translates Owl struct and enum definitions into Vest format descriptions, which provide verified parsing and serialization for these messages.

What is Vest?

Vest is a verified parsing and serialization library for Verus. It uses a combinator-based approach, where complex formats are built by combining primitive formats. Each combinator describes how to parse a portion of a byte sequence and how to serialize structured data back into bytes.

Among other properties, Vest proves roundtrip correctness, i.e., that parsing and serializing are mutual inverses. This rules out parser malleability and format confusion attacks, providing strong security guarantees about the format. For more details, see our USENIX Security 2025 publication on Vest.

Vest provides a front-end, VestDSL, that translates human-readable format descriptions in an RFC-like language into Vest combinators. Owl's compiler pipeline does not use this front-end; instead, it directly translates Owl structs and enums into Vest combinators.

Combinator primitives

Owl uses the following primitive Vest combinators.

Variable(n): Parses exactly n bytes. Used for fixed-size fields like Data<adv> |4|.
Tail: Parses all remaining bytes until the end of the input. Used for variable-length trailing fields like Data<adv> (without a length annotation).
Tag<U8, u8>(value): Parses a single byte tag that must equal value. Used for enum discriminants and constant markers.
OwlConstBytes<N>(bytes): Parses exactly N bytes that must match the constant bytes. Used for fixed constants like Const(0x01000000). This is an Owl-specific combinator implemented in extraction/src/owl_const_bytes.rs.

Complex formats are built by nesting these combinators into tuples, representing sequential fields, and tagged unions, representing enums.

How Owl translates structs

When you define a struct in Owl, the compiler generates:

A spec-level struct (owlSpec_*) representing the logical structure.
An exec-level struct (owl_*) with runtime buffer types (OwlBuf, SecretBuf).
Combinator functions (spec_combinator_*, exec_combinator_*) that describe the binary format.
Parse and serialize functions that use the combinators.

The translation maps each field type to a combinator:

Const(0x...) → OwlConstBytes<N>(constant_bytes)
Data<adv> |n| → Variable(n) where n is a concrete length
Data<adv> (no length) → Tail
Nested structs → nested combinator tuples

How Owl translates enums

Enums are translated using ord_choice!, a Vest macro which generates a tagged union:

Each variant gets a Tag<U8, u8>(discriminant) followed by its payload combinator.
The discriminant is assigned sequentially (1, 2, 3, ...) based on the order in the enum definition.
Variants with data use their payload combinator; variants without data use Variable(0) (the empty byte sequence).

Worked example: WireGuard message formats

The WireGuard protocol defines three message types for its handshake and data transport. The WireGuard protocol specification describes these formats in detail. Our WireGuard case study models these message types as Owl structs in tests/wip/wg/defs.owl. Here, we explain how the protocol format descriptions translate into Owl struct definitions and then into Vest combinators:

Message 1 (Handshake initiation)

Protocol format (from WireGuard protocol specification):

msg = handshake_initiation {
    u8 message_type
    u8 reserved_zero[3]
    u32 sender_index
    u8 unencrypted_ephemeral[32]
    u8 encrypted_static[AEAD_LEN(32)]
    u8 encrypted_timestamp[AEAD_LEN(12)]
    u8 mac1[16]
    u8 mac2[16]
}

Here, message_type = 1, reserved_zero = {0, 0, 0}, and AEAD_LEN(n) = n + 16 (plaintext length plus authentication tag).

Owl definition (tests/wip/wg/defs.owl):

struct msg1 {
      _msg1_tag : Const(0x01000000)
    , _msg1_sender : Data<adv> |4|
    , _msg1_ephemeral : Data<adv> | |group| |
    , _msg1_static : Data<adv> | cipherlen(|group|) | 
    , _msg1_timestamp: Data<adv> | cipherlen(12) |
    , _msg1_mac1: Data<adv> | |maclen| |
    , _msg1_mac2: Const(0x00000000000000000000000000000000)
}

We combine the constant message_type and reserved_zero fields into a single constant msg1_tag field.

Translation to Vest combinator:

#![allow(unused)]
fn main() {
spec fn spec_combinator_owlSpec_msg1() -> (
    (((((((OwlConstBytes<4>,      // _msg1_tag: 0x01000000
    Variable(4)),                 // _msg1_sender: 4 bytes
    Variable(32)),                // _msg1_ephemeral: |group| = 32 bytes
    Variable(48)),                // _msg1_static: cipherlen(32) = 32 + 16 tag = 48
    Variable(28)),                // _msg1_timestamp: cipherlen(12) = 12 + 16 tag = 28
    Variable(16)),                // _msg1_mac1: |maclen| = 16 bytes
    OwlConstBytes<16>)            // _msg1_mac2: 16 zero bytes
) {
    let field_1 = OwlConstBytes::<4>(SPEC_BYTES_CONST_01000000_MSG1);
    let field_2 = Variable(4);
    let field_3 = Variable(32);
    let field_4 = Variable(48);
    let field_5 = Variable(28);
    let field_6 = Variable(16);
    let field_7 = OwlConstBytes::<16>(SPEC_BYTES_CONST_0000..._MSG1);
    ((((((field_1, field_2), field_3), field_4), field_5), field_6), field_7)
}
}

The combinator is a nested 7-tuple where each element corresponds to one field. Constants become OwlConstBytes with the constant value baked in; fixed-length fields become Variable(n) with the concrete length.

Translation mapping: The protocol's message_type (1 byte) and reserved_zero[3] combine into a single 4-byte constant 0x01000000. The u32 sender_index becomes a 4-byte field. The unencrypted_ephemeral[32] maps to |group| (32 bytes for Curve25519). The encrypted fields use cipherlen(n) which accounts for the AEAD tag: cipherlen(32) = 48 and cipherlen(12) = 28.

Message 2 (Handshake response)

Protocol format (from WireGuard protocol specification):

msg = handshake_response {
    u8 message_type
    u8 reserved_zero[3]
    u32 sender_index
    u32 receiver_index
    u8 unencrypted_ephemeral[32]
    u8 encrypted_nothing[AEAD_LEN(0)]
    u8 mac1[16]
    u8 mac2[16]
}

Where message_type = 2 and encrypted_nothing is an encryption of an empty plaintext (just the 16-byte authentication tag).

Owl definition:

struct msg2 {
      _msg2_tag : Const(0x02000000)
    , _msg2_sender: Data<adv> |4|
    , _msg2_receiver: Data<adv> |4|
    , _msg2_ephemeral: Data<adv> | |group| |
    , _msg2_empty: Data<adv> | cipherlen(0) |
    , _msg2_mac1: Data<adv> | |maclen| |
    , _msg2_mac2: Const(0x00000000000000000000000000000000)
}

Transport message (Data packet)

Protocol format (from WireGuard protocol specification):

msg = packet_data {
    u8 message_type
    u8 reserved_zero[3]
    u32 receiver_index
    u64 counter
    u8 encrypted_encapsulated_packet[]
}

Where message_type = 4 and encrypted_encapsulated_packet[] is a variable-length field containing the encrypted payload (whose length is determined by the ciphertext).

Owl definition:

struct transp {
      _transp_tag : Const(0x04000000)
    , _transp_receiver : Data<adv> |4|
    , _transp_counter  : Data<adv> | |counter| | 
    , _transp_packet   : Data<adv> 
}

Translation:

#![allow(unused)]
fn main() {
spec fn spec_combinator_owlSpec_transp() -> (
    OwlConstBytes<4>,      // _transp_tag: 0x04000000
    Variable(4),           // _transp_receiver: 4 bytes
    Variable(8),           // _transp_counter: |counter| = 8 bytes
    Tail                  // _transp_packet: variable-length remainder
) { ... }
}

Note that _transp_packet has no length annotation, so it becomes Tail, consuming all remaining bytes. This is appropriate for encrypted payloads whose length is determined by the ciphertext.

Using generated parsers and serializers

The compiler generates parse_owl_* and serialize_owl_* functions that use these combinators. The parse function uses the exec combinator to parse the buffer, then constructs the struct from the parsed tuple. The spec-level parse function (parse_owlSpec_*) provides the specification that the exec function must match, wrapping the Vest combinator calls.

Design guidelines

When defining message formats in Owl:

Use Const(...) for fixed tags and markers that identify message types or protocol versions.
Use Data<...> |n| for fixed-length fields where n is a concrete length or length expression (e.g., |group|, cipherlen(12)).
Use Data<...> (no length) for variable-length trailing fields like encrypted payloads. Owl will only accept a type without a length annotation as the last field in a struct or as an enum payload, since otherwise there could be ambiguity in parsing.
Use enums for tagged unions where the tag identifies which variant follows. Enum tags are assigned in ascending order starting from 1.

The compiler automatically handles length calculations (e.g., cipherlen(n) = n + TAG_SIZE) and generates both spec and exec combinators that Verus verifies are equivalent.

Generated interface overview

The compiler emits a high-level Rust API that mirrors your Owl protocol.

Module structure. lib.rs re-exports:
- The Owl-specific support code (e.g., execlib, speclib, crypto modules).
- Generated structs, enums, and combinators that correspond to Owl datatypes.
- Protocol entry points specialised for each locality.
Effect handlers. The trait OwlEffects defines the operations the runtime must supply: sampling randomness (owl_sample), interacting with the network (owl_output, owl_input), and fused serialization, an optimization that allows the output primitive to serialize structured data directly onto the network. To integrate the code, implement OwlEffects for your IO environment. The generated procedures require an OwlEffects implementation to execute.
Configurations and state. For each locality, the compiler creates:
- cfg_<Role> structs holding immutable parameters (pre-configured crypto keys).
- state_<Role> structs representing mutable session state (stateful AEAD counters).
Session APIs. Functions such as cfg_Server::owl_server_send and cfg_Server::owl_server_recv correspond to Owl def blocks. They accept a tracked ITreeToken (synchronising with the specification), mutate the role state, and produce either results or errors (OwlError).
Constants and specifications. The module exports both spec- and exec-level constants describing crypto parameters (SPEC_CIPHER, CIPHER, etc.) and message formats (SPEC_BYTES_CONST_*). Generated proofs rely on these constants matching the runtime behaviour.
Public and secret buffers. The generated code uses OwlBuf for public data (corresponding to Data<adv> in Owl) and SecretBuf for secret data (corresponding to secret names and values with secret labels).

Client example

The client_example directory contains a small example of a verified application using a cryptographic protocol. It provides a simple echo server that receives an encrypted message, decrypts it, encrypts the same plaintext under a different key, and sends it back to the client. The file server.rs contains a simple harness that shows how to implement the OwlEffects trait and wire the generated API into an application.

Interaction trees and specifications

Owl embeds protocol specifications using interaction trees (ITrees), which provide a structured representation of protocol behavior as sequences of effectful operations (I/O, random sampling, and declassification). The generated Verus code includes specification functions that construct ITree values representing the protocol's control flow and I/O behavior.

What are interaction trees?

An ITree<A> is a recursive data structure that represents an effectful computation returning a value of type A. ITrees have the following variants¹:

Formally, our ITrees are a simplified, inductive variant of the interaction trees defined in the original work, restricted to just the effects that we care about in Owl. The original paper that defined interaction trees is: Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. 2019. Interaction trees: representing recursive and impure programs in Coq. POPL 2020. https://doi.org/10.1145/3371119

Input: Represents receiving data from the network, containing a continuation that specifies how to proceed with the received data.
Output: Represents sending data to the network, containing the data to send, an optional endpoint to send to, and a continuation.
Sample: Represents sampling randomness (e.g., generating nonces or keys), containing the length to sample and a continuation.
Declassify: Represents operations that declassify secret information (e.g., decryption, MAC verification), containing a declassifying operation and a continuation.
Ret: Represents the final return value of the protocol operation.

These variants compose to form tree structures that capture the complete I/O behavior of a protocol, enabling Verus to reason about information flow and correctness properties.

The `owl_spec!` macro

The compiler generates specifications using the owl_spec! macro, which provides a domain-specific language for constructing ITrees from Owl source code. The macro translates Owl protocol definitions into ITree specifications that Verus can verify.

For each def block in your Owl source code, the compiler generates a corresponding *_spec function. For example, if your Owl code defines:

def server_send(m: Data<adv>):
    ...

The compiler generates a Verus specification function:

#![allow(unused)]
fn main() {
pub open spec fn server_send_spec(
    cfg: cfg_Server,
    mut_state: state_Server,
    m: Seq<u8>
) -> (res: ITree<(owlSpec_ServerResult, state_Server), Endpoint>) {
    owl_spec!(mut_state, state_Server,
        // ... translated Owl code ...
    )
}
}

The owl_spec! macro accepts two type parameters (the mutable state variable name and its type) followed by an expression written in a syntax that mirrors Owl's language constructs. The macro is defined in extraction/src/speclib.rs.

For more details on the theoretical foundations of our verification strategy, and how our ITrees connect to the executable code, see Section 4 of our USENIX Security 2025 paper.

Notes on reusability

The following section is based on the artifact appendix that accompanies our USENIX Security 2025 paper. It discusses important security considerations related to incorporating code generated by Owl into larger codebases, whether verified or unverified.

The echo server illustrates how to connect a library generated by OwlC to a larger verified codebase. Verus will verify that the application logic follows its specifications. However, as discussed in our USENIX Security 2025 paper, Verus does not presently feature information-flow control or cryptographic reasoning, so it cannot prove cryptographic security properties about handwritten specifications. Developers must therefore take care that any handwritten specifications do not leak protocol secrets or otherwise compromise the security properties of the code proven in Owl. The best practice for developing verified applications using OwlC is to write as much of the application logic as possible in Owl, with handwritten specifications only for simple interfaces and functionality that does not directly interact with secrets.

Incorporating code generated by OwlC into larger Rust projects

OwlC generates a library crate that can straightforwardly be integrated into verified code in Verus. Examples of this are in the echo_server_example directory, as we discuss below. Our WireGuard and HPKE case studies illustrate how to integrate the generated libraries into pre-existing Rust codebases. We discuss some high-level considerations here.

Integrating a library generated by OwlC into a pre-existing Rust codebase requires building an interface between verified and unverified code. As with any such interface, the developer must make sure that the unverified calling context satisfies the preconditions of the verified routine. For OwlC, this means that all arguments to generated protocol routines must match the Owl types of the corresponding Owl protocol routine. That is, if an Owl routine takes as argument a key k, then the generated Verus routine must only be called with the runtime value of the key k.

OwlC relies on Rust abstract types and Verus verification conditions to maintain important soundness and correctness properties. Our SecretBuf wrapper types are opaque, so that implementation code cannot leak secrets via side channels. However, connecting to unverified Rust code may necessitate breaking some of these abstraction barriers. For instance, an application may need to reveal a SecretBuf to display a decrypted plaintext message to the user.

When connecting to unverified code, developers may therefore need to add "escape hatches" that enable such functionality. This must be done with extreme care. We recommend that any such escape hatches be annotated with a Verus precondition of requires false, so that verified code cannot use them, and the generated libraries remain sound.

Owl Book