Theory KeyserverEx

(*  Title:      KeyserverEx.thy
    Author:     Andreas Viktor Hess, DTU
    Author:     Sebastian A. Mödersheim, DTU
    Author:     Achim D. Brucker, University of Exeter
    Author:     Anders Schlichtkrull, DTU
    SPDX-License-Identifier: BSD-3-Clause

section‹A Brief Overview of Isabelle/PSPSP\label{sec:overview}›
  In this section, we briefly explain how to use Isabelle/PSPSP for proving the security of 
  protocols. As Isabelle/PSPSP is build on top of Isabelle/HOL, the overall user interface
  and the high-level language (called Isar) are inherited from Isabelle. We refer the reader
  to cite"nipkow2002isabelle" and the system manuals that are part of the Isabelle 
  distribution. The latter are accessible within Isabelle/jEdit in the documentation pane 
  on the left-hand side of the main window . 

  In the following, we will illustrate the use of our system by analyzing a simple keyserver 
  protocol (this theory is stored in the file \inlinebash|PSPSP-Manual/KeyserverEx.thy|. When 
  loading this theory in Isabelle/jEdit, please ensure that the 
  session @{session "Automated_Stateful_Protocol_Verification"} is active (this session provides

  When done, please move the text cursor to the section ``Proof of Security''. There are some 
  orange question marks at the side of some lines. These are the comments from Isabelle that 
  indicate the timing results we ask for: when moving the cursor to the corresponding line,
  and selecting the \verb|Output|-Tab on the bottom of the Isabelle window (ensure that there is 
  a tick-mark on ``Auto update''), you see the timing information provided by Isabelle for each step. 
  Your Isabelle should look similar to \autoref{fig:Keyserver}.
  \caption{Opening \inlinebash|KeyserverEx.thy| in Isabelle/jEdit.}\label{fig:Keyserver}

  The Isabelle IDE (called Isabelle/jEdit) is a front-end for Isabelle that supports most features
  known from IDEs for programming languages. The input area (in the middle of the upper part of 
  the window) supports, e.g., auto completion, syntax highlighting, and automated proof generation 
  as well as interactive proof development. The lower part shows the current output (response)
  with respect to the cursor position.

  We will now briefly explain this example in more detail. First, we start with the theory header: 
  As in Isabelle/HOL, formalization happens within theories. A theory is a unit with a name that 
  can import other theories. Consider the following theory header: ›
text‹which opens a new theory \texttt{KeyserverEx} that is based on the top-level theory of 
Isabelle/PSPSP, called @{theory "Automated_Stateful_Protocol_Verification.PSPSP"}. Within this 
theory, we can use all definitions and tools provided by Isabelle/PSPSP. For example, 
Isabelle/PSPSP provides a mechanism for measuring the run-time of certain commands. This 
mechanism can be turned on as follows:›
declare [[pspsp_timing]]

subsection‹Protocol Specification›
The protocol is specified using a domain-specific language that, e.g., could also be used by a 
security protocol model checker. We call this language ``trac'' and provide a dedicated environment 
(command) @{command "trac"} for it: ›
Protocol: Keyserver

honest = {a,b,c}
dishonest = {i}
agent = honest ++ dishonest

ring/1 valid/1 revoked/1 deleted/1

Public sign/2 crypt/2 pair/2
Private inv/1

sign(X,Y) -> Y
crypt(X,Y) ? inv(X) -> Y
pair(X,Y) -> X,Y

# Out-of-band registration
  new PK
  insert PK ring(A)
  insert PK valid(A)
  send PK.

# Out-of-band registration (for dishonest users; they reveal their private keys to the intruder)
  new PK
  insert PK valid(A)
  send PK
  send inv(PK).

# User update key
  PK in ring(A)
  new NPK
  delete PK ring(A)
  insert PK deleted(A)
  insert NPK ring(A)
  send sign(inv(PK),pair(A,NPK)).

# Server update key
  receive sign(inv(PK),pair(A,NPK))
  PK in valid(A)
  NPK notin valid(_)
  NPK notin revoked(_)
  delete PK valid(A)
  insert PK revoked(A)
  insert NPK valid(A)
  send inv(PK).

# Attack definition
  receive inv(PK)
  PK in valid(A)

The command @{command "trac"} automatically translates this specification into a family of formal 
HOL definitions. Moreover, basic properties of these definitions are also already proven 
automatically (i.e., without any user interaction): for this simple example, already over 350 
definitions and theorems are automatically generated, respectively, formally proven. For example, 
the following induction rule is derived:
@{thm [display] "Keyserver_Ana.induct"}

subsection ‹Protocol Model Setup›
text‹Next, we show that the defined protocol satisfies the requirement of our protocol model
(technically, this is done by instantiating several Isabelle locales, resulting in over 1750 
theorems ``for free.''). The underlying instantiation proofs are fully automated by our tool:›
protocol_model_setup spm: Keyserver

subsection ‹Fixed Point Computation›
text‹Now we compute the fixed-point: ›
compute_fixpoint Keyserver_protocol Keyserver_fixpoint
text‹We can inspect the fixed-point with the following command: › 
thm Keyserver_fixpoint_def
text‹Moreover, we can use Isabelle's @{command "value"}-command to compute its size:›
value "let (FP,_,TI) = Keyserver_fixpoint in (size FP, size TI)"

subsection ‹Proof of Security›
text‹ After these steps, all definitions and auxiliary lemmas for the security proof are available. 
Note that the security proof will fail, if any of the previous commands did fail. A failing command 
is sometimes hard to spot for non Isabelle experts: the status bar next to the scroll bar 
on the right-hand side of the window should not have any ```dark red'' markers.

We can do a fully automated security proof using a new command @{command "protocol_security_proof"}:›