Tomasz M. Kozlowski
and Scott A. Smolka
Department of Computer Science
SUNY at Stony Brook
Stony Brook, NY 11794-4400 USA
{tomek,sas}@cs.sunysb.edu
We analyze a security protocol that combines digital signatures with data encryption. The analysis technique we utilize is temporal logic model checking as provided by the Concurrency Factory specification and verification toolset [CLSS96]. We show that the protocol is secure, providing privacy and proof of authorship. We demonstrate, however, that a version of the protocol in which confirmation messages are used is susceptible to an attack. This is the case even if the encryption and signature operations are different, contrary to what is claimed in [Sch94]. Finally, we show how the protocol with confirmation messages can be fixed by including the identity of the sender in messages transmitted by the protocol.
Public-key cryptography [DH76, RSA78], which uses a public key for message encryption and a private key for message decryption, is a well-established method for the private transmission of sensitive data. Privacy in this case means that if two parties use public-key cryptography to exchange a message, an intermediary cannot intercept and read the message, intercept and modify the message, or fabricate a realistic-looking substitute message [Sch94].
In addition to privacy, users may also be interested in proof of authorship, such as that offered by handwritten signatures on paper documents. As pointed out in [Sch94], such proof must have the following characteristics: the signature must be unforgeable; the signature is authentic; the signature cannot be transferred from one document to another; the signature cannot be repudiated; and the signed document must be unalterable.
Digital signatures can be used for proof of authorship in a computer network, and certain public-key cryptosystems can be used to implement digital signatures. The basic idea is the following. Alice uses her private key to sign a document; Alice sends the document to Bob; and Bob uses Alice's public key to verify the signature. (As is traditional, we will use Alice and Bob as the protocol participants, sometimes abbreviated A and B.)
In this paper, we analyze a protocol that combines public-key cryptography with digital signatures, and therefore strives to offer both privacy and proof of authorship. The protocol appears in [Sch94, page 37,] and we refer to it as DSE, for Digital Signatures with Encryption. Using temporal logic model checking as provided by the Concurrency Factory specification and verification toolset [CLSS96], we show that DSE is secure, providing privacy and proof of authorship.
[Sch94] also considers a version of DSE with the additional feature of confirmation messages: whenever someone receives a message, he or she sends it back to the sender as a confirmation of receipt. We refer to this extension of DSE as DSEC, and show that DSEC is susceptible to an attack that compromises privacy. This is the case even if the encryption and signature operations are different, contrary to what is claimed in [Sch94]. By ``different'' we mean here that the signing operation is not the inverse of the encryption operation even when the same key is used in both, and likewise for the signature verification and decryption operations. The attack in question was extracted using the counter-example facility of the Concurrency Factory's model checker.
Finally, we show how DSEC can be fixed by including the identity of the sender in the messages transmitted by the protocol. Again, model checking is used to verify privacy and proof of authorship.
The structure of the rest of the paper is as follows. Section 2 provides an overview of the Concurrency Factory's VPL system specification language and model checking facility. Section 3 presents the protocols we are considering along with the possible attack on the DSEC protocol. Section 4 describes how we modeled the protocols in VPL, and encoded their correctness properties in the modal mu-calculus, the temporal logic supported by the Concurrency Factory's model checker. The results of our verification runs are the topic of Section 5. Finally, Section 6 concludes.
The Concurrency Factory [CLSS96] is an integrated toolset for the specification, verification, and implementation of concurrent and distributed real-time systems such as communication protocols and process control systems. The main features of the Factory are: a graphical user interface that allows the non-expert to design and simulate concurrent systems using GCCS, a graphical process algebra; a textual user interface for VPL; a suite of verification routines that currently includes a local model checker for the modal mu-calculus [RS97], a very expressive temporal logic, and a local model checker for a real-time extension of the modal mu-calculus [SS95]; and a graphical compiler that transforms GCCS and VPL specifications into executable Facile [TLK96] code.
We briefly describe here the components of the Factory that are most germane to our modeling and analysis of DSE and its variants: VPL and the local model checker for the modal mu-calculus. VPL is well suited for specifying concurrent systems with non-trivial control structure and data structures, and which involve value passing (as opposed to pure synchronization). VPL-supported data structures include integers of limited size and arrays and records composed of such integers. Structural equivalence of data types is employed, i.e. two integer types are considered the same if their sizes are equal and two records are equivalent when they have fields of the same type appearing in the same order.
A system specification in VPL is a tree-like hierarchy of subsystems. A subsystem is either a network or a process. A network consists of a collection of subsystems running in parallel and communicating with each other through typed channels. Processes are at the leaves of the hierarchy. Each subsystem, be it a process or a network, consists of a header, local declaration and body. The header specifies a unique name for the subsystem and a list of ``formal channels'' (by analogy with formal parameters of procedures in programming languages). The names of the formal channels of a subsystem can be used in the body of the subsystem and represent events visible to an external observer.
Declarations local to a network include specifications of the subsystems of the network and channels for communication between subsystems, hidden from the outside world. The body of a network is a parallel composition of its subsystems. A subsystem declared within a network can be used arbitrarily many times; each time a new copy of the subsystem is instantiated with actual channels substituted for the formal ones. Actual channels must match the formal ones introduced in the header and must be declared either as local channels or formal channels of the network immediately containing the subsystem.
Declarations local to a process consist of variable and procedure declarations. Procedure bodies, like process bodies, are sequences of statements. Simple statements of VPL are assignments of arithmetic or boolean expressions to variables, and input/output operations on channels. Complex statements include sequential composition, if-then-else, while-do, and nondeterministic choice in the form of the select statement.
VPL programs can be verified using LMC, the Concurrency Factory's local model checker for the propositional modal mu-calculus. LMC first produces a graph representation of the logical formula under consideration and then computes the product of this graph with the labeled transition system (guaranteed to be finite-state) underlying the VPL program. This ``product graph'' is constructed on-the-fly: each product graph node has an associated boolean value (representing the value of a subformula in an LTS state) and the value of a node is computed based on the values of its successors. Values of the terminal nodes in the product graph can be decided immediately based on the node itself. Nodes are never constructed unless their values are needed to determine the value of a previously constructed node.
To further reduce the size of the product graph, LMC avoids interleaving process transitions whenever the order of interleaving cannot affect the truth of a logical formula. Intuitively, this is achieved by enlarging the granularity of process steps so as to avoid redundant interleavings. LMC is also equipped with a diagnostic facility which allows the user to request that the contents of the depth-first search stack be displayed whenever a certain ``significant event'' occurs--for instance, when the search first encounters a state at which a logical variable is determined to be either true or false. This technique can be used to great effect, for instance, to discover execution paths leading to deadlocked states or corresponding to potential attacks on security protocols.
The protocols we analyze aim to provide privacy and proof of authorship to communicating agents, that is to guarantee:
Note that for the proof of authorship property we do not require that A has both signed and sent the message that B has received since this cannot be guaranteed. B could forward the message it received from A to some other agent C after decrypting and encrypting it appropriately. C would thus receive a message that had been signed by A but had been sent to her by B and not A.
The protocols utilize digital signatures and encryption algorithms, both of which are public-key algorithms [DH76]. The private key of an agent is used to sign a message, and the public key is used to verify the message; i.e. to verify that the message has indeed been signed by the agent who claims to have signed it. Another unrelated pair of private and public keys is used for the decryption and encryption operations, respectively.
The basic protocol we verify is as follows [Sch94, page 37,]:
1. Agent A signs a message with her private key.
Sa(M)
2. Agent A encrypts the message and signature with agent B's
public key and sends it to B.
Eb(Sa(M))
3. Agent B decrypts the message with his private key.
Db(Eb(Sa(M))) = Sa(M)
4. Agent B verifies the message with A's public key and recovers
the original message.
Va(Sa(M)) = M
We shall refer to this protocol as Digital Signatures with Encryption (DSE). Note that the choice of public key used for verification of the signature in step 4 depends on the plaintext sender ID associated with the message received by agent B. As will be shown, a modified version of this protocol, in which confirmation messages are used, can be attacked if this field is changed by an intruder.
Consider a version of the protocol in which confirmation messages are used. Whenever an agent receives a message, he or she sends it back to the sender as a confirmation of receipt. This protocol, which we refer to as DSE with Confirmation Messages (DSEC), is given as follows [Sch94, page 38,]:
1. Agent A signs a message with her private key, encrypts it
with agent B's public key, and sends it to B.
Eb(Sa(M))
2. Agent B decrypts the message with his private key and verifies
the signature with agent A's public key, thereby verifying that
A signed the message and, at the same time, recovering the message.
Va(Db(Eb(Sa(M)))) = Va(Sa(M)) = M
3. Agent B signs the message with his private key, encrypts it
with agent A's public key, and sends it back to A.
Ea(Sb(M))
4. Agent A decrypts the message with her private key, and verifies the signature with agent B's public key. If the resultant message is the same one A initially sent to B, agent A knows that B received the message accurately.
Vb(Da(Ea(Sb(M)))) = Vb(Sb(M)) = M
DSEC is vulnerable to an attack that compromises privacy. Assume that agent I is a legitimate system user with his own public and private keys. Further assume that I somehow gets access to a message that A has sent to B, and later resends this message to B, claiming that it comes from him (agent I):
1. Agent I sends the overheard message to agent B pretending
to be the sender.
Eb(Sa(M))
2. Agent B thinks that this is a legitimate message from agent
I so he decrypts the message with his private key and then tries
to verify agent I's signature with agent I's public key.
The resultant message, which is pure gibberish, is:
Vi(Db(Eb(Sa(M)))) = Vi(Sa(M))
3. Agent B nonetheless follows the protocol and sends agent I
a receipt.
Ei(Sb(Vi(Sa(M))))
4. Agent I can decrypt the message with his private key, verify it with agent B's public key, sign it with his private key, and verify it with agent A's public key to obtain M. The protocol has thus failed.
Va(Si(Vb(Di(Ei(Sb(Vi(Sa(M)))))))) = M
Note that I was able to successfully attack the protocol because he could change the plaintext sender ID of the message A originally sent to B. By altering that field, I was able to fool B into believing that the message came from him (agent I) rather than from A. Below, we present a modification to the DSEC protocol that prevents such attacks by including the sender ID in the encrypted part of transmitted messages.
Schneier [Sch94, page 39,] contends that
The ... attack works because the encrypting operation is the same as the signature-verifying operation, and the decryption operation is the same as the signature operation. If the protocol used even slightly different operation for encryption and digital signatures, this would be avoided.
The above attack, however, shows that this is not true and that privacy can be compromised even if all the operations used in the protocol are different. In fact, the attack we have exhibited is the same as the one presented in [Sch94, page 38,] with the important exception that signature signing and verification operations have not been replaced by their decryption/encryption counterparts (e.g. the message A originally sent to B is Eb(Sa(M)), not Eb(Da(M)) as in Schneier's attack). Moreover, we have in no place assumed that a signature operation is semantically equivalent to the corresponding decryption operation, nor that a signature-verifying operation is semantically equivalent to the corresponding encryption operation.
By preserving the presence of signature-related operations in the attack, we are able to show that the attack is possible, again, even if all the operations used in the protocol are different. Rather, it is the willingness of B to acknowledge the receipt of gibberish that creates the vulnerability to an attack and not the fact that the encryption operation might be the same as the signature-verifying operation, and the decryption operation might be the same as the signature operation.
The attack on DSEC was successful because the intruder was able to alter the sender ID field of a message it overheard. The fix to the protocol involves adding the identity of the sender to both messages of DSEC; these message should now be Eb(Sa(M, A)) and Ea(Sb(M)), respectively. Apart from the sender ID that gets signed and encrypted, the messages in the modified protocol also include the usual plaintext sender ID field.
The new protocol, which we call DSEC', can be stated as follows:
1. Agent A attaches her ID to a message, signs the augmented message with her private key, encrypts it with agent B's public key, and sends it to B.
Eb(Sa(M, A))
2. Agent B decrypts the message with his private key and verifies
the signature with agent A's public key, thereby verifying that
A signed the message and, at the same time, recovering the message.
Va(Db(Eb(Sa(M, A)))) = Va(Sa(M, A)) = (M, A)
3. Agent B checks whether the encrypted sender ID agrees with the plaintext sender ID. If so, B attaches his ID to the message, signs the augmented message with his private key, encrypts it with agent A's public key, and sends it back to A.
Ea(Sb(M, B))
4. Agent A decrypts the message with her private key, and verifies the signature with agent B's public key. If the resultant message is the same one A initially sent to B, agent A knows that B received the message accurately.
Vb(Da(Ea(Sb(M, B)))) = Vb(Sb(M, B)) = (M, B)
If B discovers that the two sender ID fields in step 3 do not match, he can either send a response back to the original sender (the one whose ID is signed and encrypted) using the appropriate encryption key, or not send any response at all. He should not, however, send a response back to the agent whose ID appears in the plaintext sender ID field as this might lead to an attack on the protocol.
We modeled the protocols of Section 3 in the Concurrency Factory using VPL. The VPL source code of the protocols can be found in Appendix A. The agents taking part in the protocols are modeled as VPL processes. Moreover, the intruder is modeled as a process that can perform any attack that we would expect a real-world intruder to be able to perform. The intruder is able to [Low96]:
The intruder has his own private and public keys and can take part in normal runs of the protocol. Other agents may initiate runs of the protocol with him and he may initiate runs of the protocol with other agents. The actions of the intruder are unobservable by other agents when he tries to attack the protocol, but not when he is engaged in a normal run of the protocol.
The only capability of the intruder that we do not model and which the intruder might possess is the ability to store messages the intruder sees for use in future attacks. Also, we only model a single initiator, single responder, and single intruder. Finally, we assume that the encryption and digital signatures algorithms are strong, in that an intruder cannot deduce the plaintext from the ciphertext without knowing the key [Sch94].
To determine if the protocols are secure, i.e. satisfy the privacy and proof of authorship properties, we encoded these properties in the modal mu-calculus, and used the Concurrency Factory's local model checker for the modal mu-calculus [RS97].
Privacy means that only the intended receiver of a message should be able to read its contents. This property can be stated as a conjunction of the two following properties:
AG (not I_read_As_msg_to_B)
AG (I_sent_As_msg_to_B => (not B_reads_Is_msg_first))
where AG is the CTL operator [CE81] meaning ``in every state.'' The first formula expresses the fact that agent I should never read the contents of a message agent A has sent to agent B. The second formula states that whenever I passes A's message to B, B will be able to read that message.
The proof of authorship property cannot be directly translated into CTL since it refers to the past rather than to the future. For example, the simple formula
AG (not A_sent_msg_to_B => AG (not B_read_As_msg))
does not express the property we want and is just false. This property states that in every state if agent A has not sent a message to agent B, B will never reach a state in which he reads a message from A.
To express the property properly we define the following two formulas, where W is the weak until operator of CTL, AX is the ``in all next states'' operator of CTL, and C and D are some events:
C before D = not D W C
C between Ds = AG( D => AX A (not D W C))
The first formula, C before D, states that C should happen before D happens. The second formula, C between Ds, states that between any two D's there should be at least one C. Having these auxiliary formulas, and assuming that intruder I is an intermediary between A and B, we can now state the proof of authorship property as the conjunction of the following four formulas:
Consider the first two formulas. They express the fact that before agent I can pass agent A's message along to agent B, A must have sent a message to B; and after I has passed A's message destined for B to B, A must send another message to B before I can pass another message from A to B. Together, these two formulas mean that whenever agent I passes agent A's message to agent B, A must have sent a message to B. From the model of the protocol we know that the signal I_sent_As_msg_to_B occurs only when I passes the unmodified message he just received from A to B. This implies that whenever I passes A's message along to B the message has indeed been sent by A.
Repeating this reasoning for the last two formulas we get that whenever B receives A's message, the message must have been sent by I. Combining this implication with the previous one we obtain that whenever B receives a message from A the message has been sent by A and therefore has been signed by A. Notice that A did not need to send the message directly to B; rather, A's message might have been relayed to B by some intermediary.
Using the Concurrency Factory's local model checker for the modal mu-calculus, we have obtained the following results:
Figure 1 contains the execution times for these runs (in seconds) along with the size of the state space generated by each protocol's VPL description. These results were obtained on a Sparc 20 with 96 MB of RAM.
| Protocol | Proof of authorship | Privacy | |
|---|---|---|---|
| DSE | state space size | 1623 | 981 |
| execution time (sec) | 40 | 25 | |
| DSEC | state space size | 3663 | 2147 |
| execution time (sec) | 520 | 205 | |
| DSEC' | state space size | 1221 | 836 |
| execution time (sec) | 73 | 47 | |
Table 1: State space sizes and execution times for the verification
runs.
We have analyzed a security protocol that provides privacy and proof of authorship through the use of encryption and digital signatures. Model checking in the Concurrency Factory has shown that, under a certain reasonable set of assumptions, the original protocol is secure while an extension of the protocol to include confirmation messages is vulnerable to a privacy attack. Model checking has also shown that the extended protocol can be rendered secure by including the sender ID in the protocol's encrypted messages.
As future work, we plan to extend the Concurrency Factory's VPL system specification language to directly support cryptographic primitives such as those found in the Spi calculus [AG97]. This should facilitate the encoding and analysis of more sophisticated security protocols.
{ Digital Signatures with Encryption (DSE) }
{ }
{ Comment : original protocol }
{ Author : Tomasz Kozlowski }
{ Date and place: Stony Brook, NY, Aug 1 1997 }
{ File name : ds.vpl }
network digital_signatures( sent_msg_to_B : synch,
sent_msg_to_I : synch,
I_sent_As_msg_to_B : synch,
I_read_As_msg : synch,
B_read_As_msg : synch,
B_read_Is_msg : synch,
error : synch )
begin
value PROCESS_A : 0
value PROCESS_B : 1
value PROCESS_I : 2
type process_ID : 3
value SIGN_A : 0
value SIGN_B : 1
value SIGN_I : 2
type signature : 3
value ENCRYPT_A : 0
value ENCRYPT_B : 1
value ENCRYPT_I : 2
value VERIFY_A : 3
value VERIFY_B : 4
value VERIFY_I : 5
type encryption_verification : 6
type message_len : 3
type message : record
sender : process_ID; { plain-text sender ID }
receiver : process_ID; { plain-text receiver ID }
data1 : signature;
data2 : encryption_verification;
length : message_len;
end
{ sender }
process A( out : message,
sent_msg_to_B : synch,
sent_msg_to_I : synch,
A_sent_msg : synch )
begin
var msg : message
while true = true do
msg.sender := PROCESS_A;
msg.data1 := SIGN_A;
msg.length := 2;
select
{ send message to B }
begin
msg.receiver := PROCESS_B;
msg.data2 := ENCRYPT_B
end
%
{ send message to I }
begin
msg.receiver := PROCESS_I;
msg.data2 := ENCRYPT_I
end
end; { select }
{ Send message }
out!msg;
if msg.receiver = PROCESS_B then
sent_msg_to_B!*
else
sent_msg_to_I!*;
A_sent_msg!*
end { while }
end; { sender A }
{ intruder }
process I( in : message,
out : message,
I_read_As_msg : synch,
I_sent_As_msg_to_B : synch,
A_sent_msg : synch,
I_sent_msg : synch,
error : synch )
begin
var msg : message
while true = true do
select
begin
in?msg;
A_sent_msg?*;
if (msg.receiver = PROCESS_B) then
begin
{ A is sending a message to B. Try to read its contents. }
{ The field data1 always contains a signature and doesn't }
{ need to be checked. }
if (msg.length = 2) & (msg.data2 = ENCRYPT_I) then
I_read_As_msg!*;
select
begin
select
begin
select
{ Pass the message along to B (without tampering with it) }
skip
%
{ Intercept the message, send the message to B pretending }
{ to be the sender. }
msg.sender := PROCESS_I
end; { select }
{ Send the message }
out!msg;
if msg.sender = PROCESS_A then
I_sent_As_msg_to_B!*;
I_sent_msg!*
end { begin }
%
{ Replace A's message with some other message - try }
{ to fool B into believing that this message comes }
{ from A. }
begin
msg.sender := PROCESS_A;
msg.receiver := PROCESS_B;
msg.data1 := SIGN_I;
msg.data2 := ENCRYPT_B;
msg.length := 2;
out!msg;
I_sent_msg!*
end
end { select }
end
%
{ Just drop the message. }
skip
end { select }
end else
begin
{ The message is for I. Since only A can send messages }
{ to I the handling of the message is simple. }
if msg.data2 = ENCRYPT_I then
begin
{ Decrypt the message }
msg.length := msg.length - 1;
{ Verify the message using the sender's public key }
if msg.data1 = SIGN_A then
msg.length := msg.length - 1
end;
if ~(msg.length = 0) then
error!*
end
end
%
{ Send message to B }
begin
msg.sender := PROCESS_I;
msg.receiver := PROCESS_B;
msg.data1 := SIGN_I;
msg.data2 := ENCRYPT_B;
msg.length := 2;
out!msg;
I_sent_msg!*
end
end { select }
end { while }
end; { intruder I }
{ receiver }
process B( in : message,
B_read_As_msg : synch,
B_read_Is_msg : synch,
I_sent_msg : synch,
error : synch )
begin
var msg : message
while true = true do
in?msg;
I_sent_msg?*;
if msg.data2 = ENCRYPT_B then
begin
{ Decrypt the message }
msg.length := msg.length - 1;
{ Verify the message using the sender's public key }
if msg.sender = PROCESS_A then
begin
if msg.data1 = SIGN_A then
begin
msg.length := msg.length - 1;
B_read_As_msg!*
end else
begin
msg.data2 := VERIFY_A;
msg.length := msg.length + 1
end
end else
begin
{ msg.sender = PROCESS_I }
if msg.data1 = SIGN_I then
begin
msg.length := msg.length - 1;
B_read_Is_msg!*
end else
begin
msg.data2 := VERIFY_I;
msg.length := msg.length + 1
end
end; { if }
if ~(msg.length = 0) then
error!*
end else
{ Cannot decrypt the message }
error!*
end { while }
end; { receiver B }
channel A_to_I : message
channel I_to_B : message
channel A_sent_msg : synch
channel I_sent_msg : synch
A( A_to_I, sent_msg_to_B, sent_msg_to_I, A_sent_msg ) |
I( A_to_I, I_to_B, I_read_As_msg, I_sent_As_msg_to_B, A_sent_msg,
I_sent_msg, error ) |
B( I_to_B, B_read_As_msg, B_read_Is_msg, I_sent_msg, error )
end; { digital_signatures }
{ Digital Signatures with Encryption and Confirmation Messages (DSEC) }
{ }
{ Comment : modified protocol }
{ Author : Tomasz Kozlowski }
{ Date and place: Stony Brook, NY, Aug 1 1997 }
{ File name : dsm.vpl }
network digital_signatures( sent_msg_to_B : synch,
sent_msg_to_I : synch,
I_sent_As_msg_to_B : synch,
I_read_As_msg : synch,
B_read_As_msg : synch,
B_read_Is_msg : synch,
error : synch )
begin
value PROCESS_A : 0
value PROCESS_B : 1
value PROCESS_I : 2
type process_ID : 3
value SIGN_A : 0
value SIGN_B : 1
value SIGN_I : 2
type signature : 3
value ENCRYPT_A : 0
value ENCRYPT_B : 1
value ENCRYPT_I : 2
value VERIFY_A : 3
value VERIFY_B : 4
value VERIFY_I : 5
type encryption_verification : 6
type message_len : 5
type message : record
sender : process_ID; { plain-text sender ID }
receiver : process_ID; { plain-text receiver ID }
data1 : signature;
data2 : encryption_verification;
data3 : signature;
data4 : encryption_verification;
length : message_len;
end
{ sender }
process A( out : message,
ack : message,
sent_msg_to_B : synch,
sent_msg_to_I : synch )
begin
var msg : message
while true = true do
msg.sender := PROCESS_A;
msg.data1 := SIGN_A;
msg.length := 2;
select
{ Send message to B }
begin
msg.receiver := PROCESS_B;
msg.data2 := ENCRYPT_B;
sent_msg_to_B!*;
out!msg
end
%
{ Send message to I }
begin
msg.receiver := PROCESS_I;
msg.data2 := ENCRYPT_I;
sent_msg_to_I!*;
out!msg
end
%
{ Wait for acknowledgement }
ack?msg
end { select }
end { while }
end; { sender A }
{ intruder }
process I( in : message,
in_ack : message,
out : message,
out_ack : message,
I_read_As_msg : synch,
I_sent_As_msg_to_B : synch,
error : synch )
begin
var msg : message
while true = true do
select
begin
in?msg;
if (msg.receiver = PROCESS_B) then
begin
{ A is sending a message to B. Try to read its contents. }
{ The field data1 always contains a signature and doesn't }
{ need to be checked. }
if (msg.length = 2) & (msg.data2 = ENCRYPT_I) then
I_read_As_msg!*;
select
begin
select
begin
select
{ Pass the message along to B (without tampering with it) }
skip
%
{ Intercept the message, send the message to B pretending }
{ to be the sender }
msg.sender := PROCESS_I
end; { select }
{ Send the message }
if msg.sender = PROCESS_A then
I_sent_As_msg_to_B!*;
out!msg;
out_ack?msg;
{ Try to read the contents of the confirmation message B is }
{ sending back. Only fields data2 and data4 need to be }
{ checked for readability by I since fields data1 and data3 }
{ always contain signatures, which can be verified by }
{ everybody. }
if (msg.length = 2) & (msg.data2 = ENCRYPT_I) then
I_read_As_msg!*;
if (msg.length = 4) & (msg.data4 = ENCRYPT_I) then
if ~(msg.data2 = ENCRYPT_A) then
if ~(msg.data2 = ENCRYPT_B) then
I_read_As_msg!*
end { select }
%
{ Replace A's message with some other message - try }
{ to fool B into believing that this message comes }
{ from A. }
begin
msg.sender := PROCESS_A;
msg.receiver := PROCESS_B;
msg.data1 := SIGN_I;
msg.data2 := ENCRYPT_B;
msg.length := 2;
out!msg;
out_ack?msg
end
end; { select }
in_ack!msg
end
%
{ Just drop the message. }
skip
end { select }
end else
begin
{ The message is for I. Since only A can send messages }
{ to I the handling of the message is simple. }
if msg.data2 = ENCRYPT_I then
begin
{ Decrypt the message }
msg.length := msg.length - 1;
{ Verify the message using the sender's public key }
if msg.data1 = SIGN_A then
msg.length := msg.length - 1
end;
if ~(msg.length = 0) then
error!*;
{ send a receipt back to the sender }
msg.sender := PROCESS_I;
msg.receiver := PROCESS_A;
msg.data1 := SIGN_I;
msg.data2 := ENCRYPT_A;
msg.length := 2;
in_ack!msg
end
end
%
{ Send message to B }
begin
msg.sender := PROCESS_I;
msg.receiver := PROCESS_B;
msg.data1 := SIGN_I;
msg.data2 := ENCRYPT_B;
msg.length := 2;
out!msg;
out_ack?msg
end
end { select }
end { while }
end; { intruder I }
{ receiver }
process B( in : message,
ack : message,
B_read_As_msg : synch,
B_read_Is_msg : synch,
error : synch )
begin
var msg : message
while true = true do
in?msg;
if msg.data2 = ENCRYPT_B then
begin
{ Decrypt the message }
msg.length := msg.length - 1;
{ Verify the message using the sender's public key }
if msg.sender = PROCESS_A then
begin
if msg.data1 = SIGN_A then
begin
msg.length := msg.length - 1;
B_read_As_msg!*
end else
begin
msg.data2 := VERIFY_A;
msg.length := msg.length + 1
end
end else
begin
{ msg.sender = PROCESS_I }
if msg.data1 = SIGN_I then
begin
msg.length := msg.length - 1;
B_read_Is_msg!*
end else
begin
msg.data2 := VERIFY_I;
msg.length := msg.length + 1
end
end; { if }
{ Send a receipt back to the sender }
if msg.length = 0 then
begin
msg.data1 := SIGN_B;
if (msg.sender = PROCESS_A) then
msg.data2 := ENCRYPT_A
else
msg.data2 := ENCRYPT_I
end else
begin
msg.data3 := SIGN_B;
if (msg.sender = PROCESS_A) then
msg.data4 := ENCRYPT_A
else
msg.data4 := ENCRYPT_I
end;
msg.receiver := msg.sender;
msg.sender := PROCESS_B;
msg.length := msg.length + 2;
ack!msg
end else
{ Cannot decrypt the message }
error!*
end { while }
end; { receiver B }
channel A_to_I : message
channel I_to_A : message
channel I_to_B : message
channel B_to_I : message
A( A_to_I, I_to_A, sent_msg_to_B, sent_msg_to_I, ) |
I( A_to_I, I_to_A, I_to_B, B_to_I, I_read_As_msg, I_sent_As_msg_to_B,
error ) |
B( I_to_B, B_to_I, B_read_As_msg, B_read_Is_msg, error )
end; { digital_signatures }
DSEC'
{ Digital Signatures with Encryption and Confirmation Messages (DSEC') }
{ }
{ Comment : modified corrected protocol }
{ Author : Tomasz Kozlowski }
{ Date and place: Stony Brook, NY, Aug 1 1997 }
{ File name : dsmc.vpl }
network digital_signatures( sent_msg_to_B : synch,
sent_msg_to_I : synch,
I_sent_As_msg_to_B : synch,
I_read_As_msg : synch,
B_read_As_msg : synch,
B_read_Is_msg : synch,
error : synch )
begin
value PROCESS_A : 0
value PROCESS_B : 1
value PROCESS_I : 2
type process_ID : 3
value SIGN_A : 0
value SIGN_B : 1
value SIGN_I : 2
type signature : 3
value ENCRYPT_A : 0
value ENCRYPT_B : 1
value ENCRYPT_I : 2
value VERIFY_A : 3
value VERIFY_B : 4
value VERIFY_I : 5
type encryption_verification : 6
type message_len : 3
type message : record
sender : process_ID; { plain-text sender ID }
receiver : process_ID; { plain-text receiver ID }
data0 : process_ID; { signed and encryped sender ID }
data1 : signature;
data2 : encryption_verification;
length : message_len;
end
{ sender }
process A( out : message,
ack : message,
sent_msg_to_B : synch,
sent_msg_to_I : synch )
begin
var msg : message
while true = true do
msg.sender := PROCESS_A;
msg.data0 := PROCESS_A;
msg.data1 := SIGN_A;
msg.length := 2;
select
{ Send message to B }
begin
msg.receiver := PROCESS_B;
msg.data2 := ENCRYPT_B;
sent_msg_to_B!*;
out!msg
end
%
{ Send message to I }
begin
msg.receiver := PROCESS_I;
msg.data2 := ENCRYPT_I;
sent_msg_to_I!*;
out!msg
end
%
{ Wait for acknowledgement }
ack?msg
end { select }
end { while }
end; { sender A }
{ intruder }
process I( in : message,
in_ack : message,
out : message,
out_ack : message,
I_read_As_msg : synch,
I_sent_As_msg_to_B : synch,
error : synch )
begin
var msg : message
while true = true do
select
begin
in?msg;
if (msg.receiver = PROCESS_B) then
begin
{ A is sending a message to B. Try to read its contents. }
{ The field data1 always contains a signature and doesn't }
{ need to be checked. }
if (msg.length = 2) & (msg.data2 = ENCRYPT_I) then
I_read_As_msg!*;
select
begin
select
begin
select
{ Pass the message along to B (without tampering with it) }
skip
%
{ Intercept the message, send the message to B pretending }
{ to be the sender }
msg.sender := PROCESS_I
end; { select }
{ Send the message }
if msg.sender = PROCESS_A then
I_sent_As_msg_to_B!*;
out!msg;
out_ack?msg;
{ Try to read the contents of the confirmation message B is }
{ sending back. Only field data2 need to be checked for }
{ readability by I since field data1 always contains }
{ a signature, which can be verified by everybody. }
if (msg.length = 2) & (msg.data2 = ENCRYPT_I) then
I_read_As_msg!*
end { select }
%
{ Replace A's message with some other message - try }
{ to fool B into believing that this message comes }
{ from A. }
begin
msg.sender := PROCESS_A;
msg.receiver := PROCESS_B;
msg.data0 := PROCESS_A;
msg.data1 := SIGN_I;
msg.data2 := ENCRYPT_B;
msg.length := 2;
out!msg;
out_ack?msg
end
end; { select }
in_ack!msg
end
%
{ Just drop the message. }
skip
end { select }
end else
begin
{ The message is for I. Since only A can send messages }
{ to I the handling of the message is simple. }
if msg.data2 = ENCRYPT_I then
begin
{ Decrypt the message }
msg.length := msg.length - 1;
{ Verify the message using the sender's public key }
if msg.sender = PROCESS_A then
msg.length := msg.length - 1
end;
if ~(msg.length = 0) then
error!*;
{ Send a receipt back to the sender }
msg.sender := PROCESS_I;
msg.receiver := PROCESS_A;
msg.data0 := PROCESS_I;
msg.data1 := SIGN_I;
msg.data2 := ENCRYPT_A;
msg.length := 2;
in_ack!msg
end { else }
end
%
{ Send message to B }
begin
msg.sender := PROCESS_I;
msg.receiver := PROCESS_B;
msg.data0 := PROCESS_I;
msg.data1 := SIGN_I;
msg.data2 := ENCRYPT_B;
msg.length := 2;
out!msg;
out_ack?msg
end
end { select }
end { while }
end; { intruder I }
{ receiver }
process B( in : message,
ack : message,
B_read_As_msg : synch,
B_read_Is_msg : synch,
error : synch )
begin
var msg : message
while true = true do
in?msg;
if msg.data2 = ENCRYPT_B then
begin
{ Decrypt the message }
msg.length := msg.length - 1;
{ Check who the real sender of the message is. Verify the }
{ message with the real sender's public key. }
if msg.sender = PROCESS_A then
begin
if msg.data1 = SIGN_A then
if msg.data0 = PROCESS_A then
begin
msg.length := msg.length - 1;
B_read_As_msg!*
end
end else
begin
if msg.data1 = SIGN_I then
if msg.data0 = PROCESS_I then
begin
msg.length := msg.length - 1;
B_read_Is_msg!*
end
end
end; { if }
if ~(msg.length = 0) then
error!*;
{ Send an acknowledgement (even if the message has been forged) }
{ to the original sender. }
msg.sender := PROCESS_B;
msg.receiver := msg.data0;
msg.data0 := PROCESS_B;
msg.data1 := SIGN_B;
if msg.receiver = PROCESS_A then
msg.data2 := ENCRYPT_A
else
msg.data2 := ENCRYPT_I;
msg.length := 2;
ack!msg
end { while }
end; { receiver B }
channel A_to_I : message
channel I_to_A : message
channel I_to_B : message
channel B_to_I : message
A( A_to_I, I_to_A, sent_msg_to_B, sent_msg_to_I, ) |
I( A_to_I, I_to_A, I_to_B, B_to_I, I_read_As_msg, I_sent_As_msg_to_B,
error ) |
B( I_to_B, B_to_I, B_read_As_msg, B_read_Is_msg, error )
end; { digital_signatures }
Scott Smolka
Mon Aug 4 15:21:05 EDT 1997