Overview

This HTML page is a visualization of a security protocol correctness proof. The underlying theory (i.e. protocol model, verification theory, and verification algorithm) is described in the paper Strong Invariants for the Efficient Construction of Machine-Checked Protocol Security Proofs by Meier, Cremers, and Basin.

The page was generated automatically and you can find additional information about the the generation process in the top pane. If you need more space to investigate the proofs and visualizations, you can adjust the layout by moving the splitters.

Security Protocol Theories

In the left pane, you find a pretty-printed version of the security protocol theory that was verified. A security protocol theory is a sequence of protocol definitions and security properties that these protocols (should) satisfy. Each property that is satisfied is accompanied by a proof. Most elements of the left pane can be visualized. Just click on them to display their visualization in the center pane.

Protocol Definitions

A protocol is a set of roles where each role is a list of send and receive steps, which use pattern matching for sending and receiving messages. The labels of send and receive steps have no operational meaning. However, they are used for referencing these steps in the properties and proofs. Patterns are constructed using the following syntax.

'c'	A global constant named c.
~n	A freshly generated value (e.g., a nonce) named n.
?v	A message variable named v.
a	An agent variable named a; i.e. "no-prefix" marks agent variables.
h(m)	The hash of the pattern m.
{m}k	The encryption of the pattern m with the key k.
sign{m}k	A signature of the pattern m that can be verified with the key k.
x1,..,xn	The left-associative tuple (..((x1,x2),x3),..,xn) of the patterns x1,..,xn.
pk(a)	The long-term public key of a.
sk(a)	The long-term private key of a.
k(a,b)	The long-term shared key between a and b.

Please see our paper for additional information.

Protocol Properties

There are two types of properties that can be proven automatically: (1) Type invariants are required to make the case distinction on the possible sources of a message finite despite the untyped model we are working with. (2) Security properties like secrecy and authentication.

Type invariants state for each message variable of every role of the protocol what its possible contents can be in a reachable state of the protocol. In the paper referenced above, we only describe a single type invariant; namely that every message variable is either instantiated with a nonce or something the intruder knows before the variable was instantiated. We have generalized this construction such that the "type" of a variable can be specified more precisely. Types denote sets of messages parametrized over the system state and a thread i. They are built according to the following syntax.

Known@R_l	All messages known before thread i executed step l of role R.
n@R	A nonce named n generated by some thread j executing role R.
ty1 | ty2	The union of the messages denoted by ty1 and ty2.
...	Standard cryptographic constructors as for patterns.

Security properties are specified in the form of sequents (called judgments in the paper) where all thread identifiers in the premise are universally quantified and all additional thread identifiers in the conclusion are existentially quantified. Thread identifiers are prefixed with '#'. Local variables and actual freshly generated values are denoted by their corresponding patterns suffixed with the identifier of the thread that they are local to. Apart from these constructions the syntax of messages and the predicates used in the security property specifications should self-explanatory.

Proofs

Proofs are trees consisting of nested case distinctions, resolutions with already proven theorems, and triviality justifications. The calculus employed is described in the paper referenced above. The syntax for the proofs was inspired the Isabelle's proof language ISAR. For the actual proof script that can be machine-checked using Isabelle/HOL together with our formalization of the verification theory, see the reference in the top pane.

Note that for properties not satisfied by the protocol, the proof may contain missing branches. In these cases, the corresponding proof script is not accepted by Isabelle/HOL. Moreover, the proof state is likely to indicate an attack.

All non-trivial elements of the proofs can be visualized by clicking on them. For a case distinction on the possible sources of a message m, we also highlight this message in the visualization by a double border.

Visualization

There are three types of nodes:

1. Red colored ellipses list messages the intruder is supposed to know.
2. Colored rectangles list information about threads. They either just denote that a role step was executed by the given thread or they list additional equalities or compromisedness information about the given thread. The quantification of thread identifiers is denoted by the prefix "some" in the box with the additional information.
3. Gray rectangles list logical facts that cannot be associated to a fixed thread.

The nodes are connected by edges denoting the required ordering with respect to the reachable state in whose context we are conducting the proof. Edges from the additional thread information boxes to the first step executed by that thread have no logical meaning in our verification theory. They could however be seen as "thread creation" events.

Further Information

All of the work present here is work in progress. Both our implementation of the proof-generation tool as well as the Isabelle/HOL theories are scheduled to be open-sourced. If you would like to have a preliminary snapshot or if you have further questions, ideas, suggestions, ... please don't hesitate to write a mail to simon.meier@inf.ethz.ch.

Debug information for the last selected item providing it: