Deploy to GitHub Pages on develop: a6df687a05c2473573749494bdd7752b10…

…9f22ae

develop/book/003_example.html

@@ -166,14 +166,14 @@ <h2 id="modeling-a-public-key-infrastructure">Modeling a Public
       unconnected.</p>
       <p>The above rule can therefore be read as follows. First,
       generate a fresh name <code>~ltk</code> (of sort fresh), which is
-      the new private key, and non-deterministically choose a public
-      name <code>A</code>, for the agent for whom we are generating the
-      key-pair. Afterward, generate the fact <code>!Ltk($A, ~ltk)</code>
-      (the exclamation mark <code>!</code> denotes that the fact is
-      persistent, i.e., it can be consumed arbitrarily often), which
-      denotes the association between agent <code>A</code> and its
-      private key <code>~ltk</code>, and generate the fact
-      <code>!Pk($A, pk(~ltk))</code>, which associates agent
+      the new private (long term) key, and non-deterministically choose
+      a public name <code>A</code>, for the agent for whom we are
+      generating the key-pair. Afterward, generate the fact
+      <code>!Ltk($A, ~ltk)</code> (the exclamation mark <code>!</code>
+      denotes that the fact is persistent, i.e., it can be consumed
+      arbitrarily often), which denotes the association between agent
+      <code>A</code> and its private key <code>~ltk</code>, and generate
+      the fact <code>!Pk($A, pk(~ltk))</code>, which associates agent
       <code>A</code> and its public key <code>pk(~ltk)</code>.</p>
       <p>In the example, we allow the adversary to retrieve any public
       key using the following rule. Essentially, it reads a public-key