LINEBURG

ńņšąķčöą 8 |

v

P0 KP 0

1

v

R1 | {|P1 |}K e |R2 KP0 e

KP

v

P0 KP 0

1

e

v KP0

v KP0

R1 | {|P1 |}K e |R2 KP1

P0

R1 | {|P1 |}K e R2

P0

{|P1 |}K e

R1 P0

e

KP0

P1

Figure 7-2: Example Dolev-Yao parse tree with signatures

76

ā¢ an adversary event (where j, k < i) of the form

ā“ [āencā, j, k, mi ], in which case mk ā KP ub and mi = {|mj |}mk ,

e

ā“ [ādecā, j, k, mi ], in which case mk ā KAdv , and mj = {|mi |}mk ,

v

ā“ [āsignā, j, k, mi ], in which case mk ā KAdv and mi = [mj ] mk ,

ā“ [āpairā, j, k, mi ], in which case mi = mj |mk

ā“ [āextract-lā, j, mi ], in which case mj = mi |mk for some mk ā A,

ā“ [āextract-rā, j, mi ], in which case mj = mk |mi for some mk ā A,

ā“ [ārandomā, mi ], in which case mi = R for some R ā RAdv ,

ā“ [ānameā, mi ], in which case mi = A for some A ā M,

ā“ [āpubkeyā, mi ], in which case mi = K for some K ā KP ub ,

ā“ [ādeliverā, j, Pi ], in which case the message mj is delivered to party Pi .

ā¢ or a participant event of the form [āoutputā, Pi , mi ] or [āmessageā, Pi , mi ], in that case

[ādeliverā, k, pi ] is the most recent adversary event in the trace (for some k) and the

protocol action for Pi in its current role and internal state, upon receiving mk , is to

output/send message mi . ( P(Sj , oi , mk , Pi ) ā’ (Si , mi , {output, message}) ).

Note that there is no adversarial action for signature veriļ¬cation, this is because in the

symbolic world, an adversary is either able to create the signature symbol or not ā“ there is

no need to verify that a signature symbol is a signature symbol.

7.2 Simple Protocols

Simple protocols and their mappings are redeļ¬ned to allow signing capabilities.

Deļ¬nition 24 (Simple protocols) A simple protocol is a pair of interactive Turing ma-

chines (ITMs) {M1 , M2 }, one for each role, where each machine Mi implements an algorithm

described by a pair (Ī£, Ī ):

ā¢ Ī£ is a store, a mapping from variables to tagged values (explained further below) and

ā¢ Ī is a program that expects as input

ā“ The security parameter k,

77

Ī ::= begin; statementlist

::= input(SID, RID, PID0 , PID1 , RID2 , ...);

begin

(Store āroleā, RID , ānameā, PID0 , ānameā, PID1 , ānameā, PID2 ,...

in local variables MyRole, MyName, PeerName, OtherName2 ,...

respectively.

::=

statementlist statement statementlist

| finish

::=

statement newrandom(v)

(generate a k-bit random string r and store ārandomā, r in v)

| encrypt(v1, v2, v3)

(Send (Encrypt, PID, SID , v2) to Fcpke where v1 = āpidā, PID ,

receive c, and store āciphertextā, c, PID1 , SID in v3)

| decrypt(v1, v2)

(If the value of v1 is āciphertextā, c then send

(Decrypt, PID0 , SID , c ) to Fcpke instance PID0 , SID ,

receive some value m, and store m in v2 Otherwise, end.

| sign(v1, v2, v3)

(Send (Sign, PID, SID , v2) to Fcert where v1 = āpidā, PID ,

receive Ļ, and store āsignatureā, Ļ, PID1 , SID in v3)

| verify(v1, v2, v3)

(If the value of v1 is āsignatureā, Ļ then send

(Verify, PID0 , SID , Ļ , v2) to Fcert instance PID0 , SID ,

receive some value b, and store b in v3

Otherwise, end.

| send(v)

(Send value of variable v)

| receive(v)

(Receive message, store in v)

| output(v)

(send value of v to local output)

| pair(v1, v2, v3)

(Store āpairā, Ļ1 , Ļ2 in v3, where Ļ1 and Ļ2 are the values of

v1 and v2, respectively.)

| separate(v1, v2, v3)

(if the value of v1 is ājoinā, Ļ1 , Ļ2 , store Ļ1 in v2

and Ļ2 in v3 (else end))

| if (v1 == v2 then statementlist else statementlist

(where v1 and v2 are compared by value, not reference)

::= output( āļ¬nishedā, v ); end.

finish

The symbols v, v1, v2 and v3 represent program variables. It is assumed that āpairā, Ļ1 , Ļ2

encodes the bit-strings Ļ1 and Ļ2 in such a way that they can be uniquely and eļ¬ciently

recovered. A partyā™s input includes its own PID, the PID of its peer, and other PIDs in the

system. Recall that the SID of an instance of Fcpke is an encoding PID, SID of the PID

and SID of the legitimate recipient.

Figure 7-3: The grammar of simple protocols

78

ā“ Its SID SID, its PID PID, and its RID RID,

ā“ PID1 that represents the name for the other participant of this protocol execution.

The programs tags the input values, binds them to variables in the store, and then acts

according to a sequence of commands consistent with the grammar in Figure 3-2.

Deļ¬nition 25 (Mapping of simple protocols to symbolic protocols) Let p = {M0 , M1 }

be a simple protocol. Then p is the Dolev-Yao protocol

Pi : S Ć— M Ć— O Ć— A ā’ S Ć— A Ć— message Ć— A Ć— output

that implements ITM M, except that:

ā¢ The variables of M are interpreted as elements of the symbolic message algebra A.

ā¢ Instead of receiving as input SID, PID0 , PID1 , RID, the store is initialized with its

e v v

own name P0 , its own keys KP0 |KP0 , and a name P1 and keys KP1 |KP1 of the other

e

participant. The symbols P0 and P1 represent PID0 and PID1 , respectively. Similarly,

the symbols K0 and K1 represent PID0 , SID and PID1 , SID , respectively.

ā¢ Instead of creating a new random bit-string, the symbolic protocol returns R(i,n) and

increments n (which starts at 0),

ā¢ Instead of sending (Encrypt, PID, SID , M) to Fcpke and storing the result, the com-

posed symbol {|Ī£(M)|}KP is stored instead (where Ī£(M) is the value bound to the

1

variable M in the store Ī£).

ā¢ Instead of sending (Decrypt, PID0 , SID , C) to Fcpke and storing the result, the value

stored depends on the form of Ī£(C). If Ī£(C) is of the form {|M |}KP then the value

0

M is stored. Otherwise, the garbage value G is stored instead.

ā¢ Instead of sending (Sign, PID, SID , M) to Fcert and storing the result, the composed

symbol [Ī£(M)] KP is stored instead (where Ī£(M) is the value bound to the variable M

0

in the store Ī£).

ā¢ Instead of sending (Verify, PID0 , SID , S, M) to Fcert and storing the result, the value

stored depends on the form of Ī£(S). If Ī£(S) is of the form [M ] KP then the value 1

1

is stored. Otherwise, 0 is stored instead.

79

ā¢ Pairing and separation use the symbolic pairing operator.

ā¢ Lastly, the bit-strings āstartingā and āļ¬nishedā are mapped to the Dolev-Yao symbols

Starting and Finished , respectively.

7.3 UC to Dolev-Yao: The Revised Mapping Lemma

Deļ¬nition 26 (Traces of concrete protocols) Let p be a F-hybrid protocol. Inductively

deļ¬ne tracep,A,Z (k, z, r), as the trace of protocol p in conjunction with adversary A and

environment Z with inputs z, r, and security parameter k. Initially, the trace is the null

string. The trace then grows as the protocolā™s execution progresses.

ā¢ If the environment provides input m to a party with id (SID, RID), then

āinputā, (SID, RID), m is appended to the end of t.

ā¢ If the adversary provides input m to a party with id PID, then āadvā, PID, m is

appended to the end of t.

ā¢ If a party PID generates a new random string r, then ārandomā, r is appended to t.

ā¢ If a party pairs values m1 and m2 to form (m1 , m2 ), then āpairā, m1 , m2 is appended

to t.

ā¢ If a party PID writes a message m, it does so in one of two ways

ā“ if it writes m on its local output tape, then āoutputā, PID, m is appended to t.

ā“ if it writes m on its outgoing communication tape, then āmessageā, PID, m is

appended to t.

ā¢ If Fcpke is activated by party PID with call (Encrypt, PID, SID , m) and Fpke responds

with ciphertext c, then āciphertextā, PID, SID , m, c is appended to t. (If Fcpke

returns, ā„ then nothing is appended to t).

ā¢ If Fcpke is activated by party PID with call (Decrypt, PID, SID , c) and Fcpke responds

with plaintext m, then ādecā, PID, SID , c, m is appended to t. (If Fcpke returns, ā„

then nothing is appended to t).

80

ā¢ If Fcert is activated by party PID with call (Sign, PID, SID , m) and Fcpke responds

with signature Ļ, then āsignatureā, PID, SID , m, Ļ is appended to t. (If Fcert re-

turns, ā„ then nothing is appended to t).

ā¢ If Fcert is activated by party PID with call (Verify, PID, SID , m, Ļ) and Fcert responds

with boolean bit b, then āverā, PID, SID , m, Ļ, b is appended to t. (If Fcert returns,

ā„ then nothing is appended to t).

tracep,A,Z (k, z, r) denotes t upon completion of the protocol execution. Let tracep,A,Z (k, z)

denote the random variable for tracep,A,Z (k, z, r) when r is uniformly chosen. Let tracep,A,Z

denote the probability ensemble {tracep,A,Z (k, z)}kāN,zā{0,1}ā—

Deļ¬nition 27 (The mapping from concrete traces to symbolic traces) Let p be a

concrete Fcpke /Fcert -hybrid protocol and let t be a trace of an execution of p with security

parameter k, environment Z with input z, and random input vector r. We determine the

mapping of t to a Dolev-Yao trace in two steps. (These steps can be thought of as two

āpassesā on the string t.)

(I.) First, we read through the string t character by character, in order, and inductively

deļ¬ne the following partial mapping f from {0, 1}ā— to elements of the algebra A. (Note that

the patterns in t addressed below may be nested and overlapping. That is, the same substring

may be part of multiple patterns. A pattern is recognized as soon as the last character in

the pattern is read.)

ā¢ Whenever we encounter a pattern of the form ānameā, Ī² for some string Ī² and

f ( ānameā, Ī² )is not yet deļ¬ned then set f ( ānameā, Ī² ) = P for some new symbol

P ā M not in the range of f so far.

ā¢ Whenever we encounter a pattern of the form ābooleanā, Ī² for some string Ī² and

f ( ābooleanā, Ī² ) is not yet deļ¬ned then set f ( ābooleanā, Ī² ) = P for some new symbol

P ā B not in the range of f so far.

ā¢ Whenever we encounter in some event a pattern of the form ārandomā, Ī² for some

string Ī² and f ( ārandomā, Ī² ) is not yet deļ¬ned then set f ( ārandomā, Ī² ) = N for

some new symbol N ā R that is not in the range of f so far.

ā¢ Whenever we encounter a pattern of the form āpidā, PID , āsidā, SID for some

strings PID, SID, with f ( āpubkeyā, PID, SID ) and/or f ( āverkeyā, PID, SID ) not

81

yet deļ¬ned, then set f ( āpubkeyā, PID, SID ) = K and/or f ( āverkeyā, PID, SID ) =

K for some new K ā KP ub and K ā KV er not already in the range of f .

ā¢ Whenever we encounter a pattern of the form āpairā, Ī²1 , Ī²2 , then proceed as fol-

lows. First, if f (Ī²1 ) is not yet deļ¬ned then set f (Ī²1 ) = G, where G is the garbage

symbol. Similarly, if f (Ī²2 ) is not yet deļ¬ned then set f (Ī²2 ) = G. Finally, set

f ( āpairā, Ī²1 , Ī²2 ) = f (Ī²1 )|f (Ī²2).

ā¢ Whenever we encounter a pattern of the form āciphertextā, PID, SID , m, c for some

strings PID, SID, m, c, then f is expanded so that f ( āciphertextā, PID, SID , c ) =

{|f (m)|}f ( āpubkeyā, PID,SID ) . (Recall that such a pattern is generated whenever an

encryption call to Fcpke is made. Also, at this point both f (m) and f ( āpubkeyā, PID, SID )

must already be deļ¬ned, since this is an encryption call made by a party running a

simple protocol.)

ā¢ Whenever we encounter a pattern of the form ādecā, PID, SID , c, m , then proceed

as follows. First, if f (m) is not yet deļ¬ned, then set f (m) = G, where G is the garbage

symbol. Next, set f ( ādecā, PID, SID , c ) = {|f (m)|}f ( āpubkeyā, PID,SID ) . (Recall

that such a pattern is generated whenever a decryption call to Fcpke is made. The

case where f (m) = G occurs when a ciphertext was not generated via the encryption

algorithm. It includes both the case where the decryption algorithm fails and the case

where the decryption algorithm outputs a message that cannot be parsed by simple

protocols.)

ā¢ Whenever we encounter a pattern of the form āsignatureā, PID, SID , m, Ļ for some

strings PID, SID, m, Ļ, then f is expanded so that f ( āsignatureā, PID, SID , Ļ ) =

[f (m)] f ( āverkeyā, PID,SID ) . (Recall that such a pattern is generated whenever a sig-

nature call to Fcert is made. Also, at this point both f (m) and f ( āverkeyā, PID, SID )

must already be deļ¬ned, since this is a signing call made by a party running a simple

protocol.

ā¢ Whenever we encounter a pattern of the form āveriļ¬cationā, PID, SID , Ļ, m, b , then

proceed as follows. First, if f (m) is not yet deļ¬ned, then set f (m) = G, where G is the

garbage symbol. Next, if b = 1, set f ( āverifyā, PID, SID , Ļ ) = [f (m)] f ( āverkeyā, PID,SID ) ,

else set f ( āverifyā, PID, SID , Ļ ) = G. (Recall that such a pattern is generated

82

whenever a signature call to Fcert is made. The case where f (m) = G occurs when a

signature was not generated via the signing algorithm. If the signature is valid, Ļ is

made a valid signature symbol, if it isnā™t valid, it is set to garbage)

(II.) In the second step, we construct the actual Dolev-Yao trace. Let t = G1 ||G2 || . . . tn

be the concrete trace. Then construct the Dolev-Yao trace t by processing each G in turn,

as follows:

ā¢ If Gi = āinputā, (SID, RID), m , then we ļ¬nd m = f (m), and generate the symbolic

event H = [āinputā, P , m] (where P is the symbolic name of the input recipient).

ā¢ If Gi = āciphertextā, PID, SID , m, c or Gi = ādecā, PID, SID , c, m , then no sym-

bolic event is generated.

ā¢ If Gi = āsignatureā, PID, SID , m, Ļ or Gi = āverā, PID, SID , Ļ, m, b , then no

symbolic event is generated.

ā¢ If Gi = āoutputā, PID, m then Gi is mapped to the symbolic participant event

(f ( ānameā, PID ), output , f (m)).

ā¢ If Gi = āmessageā, PID, m then Gi is mapped to the symbolic participant event

(f ( ānameā, PID ), message , f (m)).

ā¢ If G = āadvā, PID, m , let m = f (m). Then there are two cases:

1. m is in the closure of the symbolic interpretations of the messages sent by the

parties in the execution so far, i.e.

māC m : m = f (m ) and the event āmessageā, PID, m is a prior event in t .

In this case there exists a ļ¬nite sequence of adversary events that produces mi .

Then G is mapped to this sequence of events Hi1 , Hi,2 . . . Hi,n so that the message

of Hi,n ā’1 is mi and Hi,n = [ādeliverā, (i, n ā’ 1), P ] (where P is the Dolev-Yao

name of the concrete participant who received the message from the concrete

adversary).

83

2. Otherwise, m is not in the above closure. In this case, G maps to the Dolev-Yao

event [āfailā, mi ].

We now prove the Mapping Lemma for public key encryption and digital signatures

using the reformulated ideal functionalities of Chapter 5.

Lemma 6 (The Revised Mapping Lemma) Let F denote both ideal functionalities Fcpke

and Fcert . For all simple F-hybrid protocols p, adversaries A, environments Z, and inputs

z of length polynomial in the security parameter k,

Pr t ā traceF (k, z) : t is a valid DY trace for p ā„ 1 ā’ neg(k)

p,A,Z

Proof. Let t be the trace of a simple protocol p. We will show two things: (1) if t

does not contain the event [āfailā, mi ], then it is a valid DY trace of protocol p and (2) the

probability that t includes such an event is negligible. The lemma trivially follows from

these two assertions.

(1) By the deļ¬nition of the fail event, if such an event does not occur, then we have

that all adversary events in t are valid. It then remains to show that the participant events

in t are valid as well. For a given participant event of the form (Pi , Li , mi ), we need to show

that

P(Sj , oi , m, Pi ) = (Si , m , Li )

ńņšąķčöą 8 |

Copyright © Design by: Sunlight webdesign