Theory manual
theory
"manual"
imports
"KeyserverEx"
begin
section‹Common Pitfalls\label{sec:commonpitfalls}›
text‹
This section explains some common pitfalls, along with solutions, that one may encounter when
writing trac specifications.
›
subsection‹Not Including an Initial Value-Producing Transaction›
text‹
Trac specifications that contain value-typed variables should also declare a transaction that
produces fresh values.
Take, for instance, a trac specification that contains only one transaction:
\begin{trac}
Transactions:
attackDef(PK:value)
receive PK
attack.
\end{trac}
This protocol is technically secure because no values are ever produced.
Similarly, if we just look at the protocol with the following transaction then we find that it is
also secure:
\begin{trac}
Transactions:
attackDef(PK:value)
attack.
\end{trac}
The reason it is secure is because of the occurs-message transformation that is being applied to
each transaction $T$ of the protocol for technical reasons:
A \inlinetrac|receive occurs(PK)| action is added to $T$ for each value-typed variable PK declared in
$T$, and a \inlinetrac|send occurs(PK)| is added to $T$ for each \inlinetrac|new PK| action occurring in $T$.
Since no values are actually produced in any protocol run, then no occurs-message is produced, and
so the attackDef transaction cannot ever be applied.
One would, however, naturally expect that such a protocol is not secure.
For this reason we require that each trac specification includes a value-producing transaction if
there are any value-typed variables occurring in the trac specification at all.
For instance, when including such a transaction to our example we get a valid trac transaction
specification:
\begin{trac}
Transactions:
valueProducer()
new PK
send PK.
attackDef1(PK:value)
attack.
\end{trac}
Another example is the following which is also a valid trac transaction specification because it
does not declare any value-typed variables:
\begin{trac}
Transactions:
attackDef2()
attack.
\end{trac}
Both protocols have attacks, as expected.
Examining the generated Isabelle definitions reveals that the \inlinetrac|valueProducer| transaction
produces an occurs message while the \inlinetrac|attackDef1| transaction expects to receive an occurs
message:›