In order to demonstrate the use of GNY, we will first show a simple example. Two agents already know each others' keys, and Alice will send a message to Bob, encrypted using his public key and signed using Alice's private key.
First, we will show the informal message passing description:
That is, to send an encrypted message to Bob, Alice needs to send the following:
Now, written in GNY logic, this is what we know:
That is, Bob receives a message containing his identity, a message encrypted with a symmetric key and a symmetric key encrypted with his public key.
Obviously, Bob can't do a lot with this without some assumptions. Let's define them here:
Before we can derive anything meaningful from the message, we need some rules from the GNY logic. First up is the message decryption rule:
That is, if Bob has a message encrypted using his public key, and he has the corresponding private key, he can read the message. The same is true for symmetrically encrypted messages. The next rule is the message interpretation rule I1:
This rule states that if you have a message encrypted with a private key, we have that private key, and we know it belongs to, we can assume that the encrypted message was once said by Q, and also that the message encrypted was once said by Q. Now, we can derive the following from the message:
Now, Bob has successfully decrypted Alice's message. However, he doesn't know that the message was actually written by Alice until he uses the OpenPGP verification rule V1:
Which is part of the protocol, and says that A wrote the message to B. Now, Bob knows Alice sent the message to him.
One of the key factors in OpenPGP is that all messages sent are sure to be sent by sender. This means that Bob can verify that the message actually came from Alice. However, anyone in possession of the decrypted message can do the same. To do this, we introduce a third party, Eve. Let's suppose that Alice tries to send a message to Bob, and Bob accidentally (or on purpose) discloses what Alice said. Now Eve, seeing the plaintext and the hash belonging with it, can verify that Alice indeed once said this, even if she never was able to decrypt the message herself. We can demonstrate this in the logic. First, we define our assumptions:
Now, Alice sends a message to Bob, and Eve's eavesdropping on the conversation. Bob publishes Alice's message to the world:
That is, not only Bob receives the message, Eve hears it as well. With this message, she can't do a lot. However, when Bob publishes the message (or Eve gains access to it through other means, like hacking into Bob's computer or stealing his private key), Eve is able to decrypt the hash. Thus, Eve can show anyone Alice must have said M to Bob:
Thus, even without having Bob's private key, Eve can deduce A was responsible for the message. Since encrypted messages often aren't encrypted for nothing, Alice might not want Bob to be able to disclose this information.
Now, we have previously stated the importance of the connection between the public key and the person it belongs to. One cannot verify this connection by using it cleverly. To show this, suppose Alice and Bob try to send a message tot each other. To verify their identity, Alice asks Bob a question only he would know and Alice the answer to and only Alice would be able to ask.
Receiving the correct response, Alice might be under the impression that the key indeed belongs to Bob, and thus that communication is safe. However, suppose a third party, let's call her Mallery the malicious attacker, was able to supply Alice with a faked key. Now, we have a set of assumptions:
That is, Alice has Mallory's key and is under the impression that it is Bob's key. Next to that, Mallory knows that Alice beliefs this. Now, Alice can send her secret question to Bob. However, Actually Mallory receives it (by tapping into her mail account, for example) before Bob does.
Now, Mallory is able to decrypt this message, since it is encrypted using her public key. She can take this message, change it, and then send it on to Bob. In this case, we leave Alice's secret message for what it is, and send it on.
Now, Bob, hearing Alice's message, might assume Alice actually sent it. So now, he trusts the message, and replies with the answer. However, Mallory once again intercepts the message, and sends it on to Alice:
This way, Alice and Bob are under the impression they can talk to each other using Mallory's keys. As long as Mallory keeps intercepting the messages, this interception will not be noticed. Thus, the establishing of public keys cannot be done using the same channel.