diff --git a/develop/book/003_example.html b/develop/book/003_example.html index 5f4190c..bf7a11f 100644 --- a/develop/book/003_example.html +++ b/develop/book/003_example.html @@ -166,7 +166,7 @@

Modeling a Public unconnected.

The above rule can therefore be read as follows. First, generate a fresh name ~ltk (of sort fresh), which is - the new private (long term) key, and non-deterministically choose + the new private (long-term) key, and non-deterministically choose a public name A, for the agent for whom we are generating the key-pair. Afterward, generate the fact !Ltk($A, ~ltk) (the exclamation mark ! diff --git a/develop/tex/tamarin-manual.pdf b/develop/tex/tamarin-manual.pdf index 3a30b40..7f8a9de 100644 Binary files a/develop/tex/tamarin-manual.pdf and b/develop/tex/tamarin-manual.pdf differ