LINEBURG


<< . .

 8
( 9)



. . >>

KP
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
( 9)



. . >>

Copyright Design by: Sunlight webdesign