next up previous
Next: Proofs of Exemplary Protocols Up: Weakest Preconditions Previous: Decryption

Construction of Shared Secrets

Many protocols rely on the concept of a shared secret. This is different from a shared key in that we do not use the secret to encrypt or hide information, but rather to validate a message. In this section we present the wps for shared secrets. It is important to note that we are specifically concerned about the creation shared secrets, where we have sent the secret to another entity and await validation. Constructing a shared secret is an asymmetrical process. One of the two parties must initiate the construction by generating a fresh value to be used as a secret. The other party must finish the construction by returning the secret under construction in a context which makes it clear that no third party is being misled. In this presentation the following notation is used:

   table266
Table 12: A completes a shared secret under construction.

The wps in Table 12 are used in the construction of shared secrets. Its not clear which parties can apply the operation of completing a shared secret. Clearly, belief in a completed secret can only be generated by parties who believe in the secret under construction, which will generally only be the initiating party. However, in the case that ``A tex2html_wrap_inline1355 B'' and ``B said tex2html_wrap_inline1381'' are in the set of preconditions there is no reason why Z (who may or may not have any knowledge regarding A, B, or tex2html_wrap_inline1381 ) couldn't apply the operation and complete the shared secret. This would not give Z any information about A, B, or N tex2html_wrap_inline1171 (Z sees N tex2html_wrap_inline1171 would not become true), but still seems a bit odd.


next up previous
Next: Proofs of Exemplary Protocols Up: Weakest Preconditions Previous: Decryption

Jim Alves-Foss
Fri Aug 1 16:00:31 PDT 1997