LINEBURG

 << Пред. стр. страница 2(всего 9)ОГЛАВЛЕНИЕ След. стр. >>
lenger picks b randomly from {0, 1} and sets cв€— в†ђ enc(kpub , mb ); it then hands c to both D
and A. A may now resume querying D, but is not allowed to ask for the decryption of cв€— .

15
After a polynomial number of queries, the A outputs a guess g. If g = b, the adversary wins.
A scheme is considered IND-CCA2 secure if no adversary wins with probability signiп¬Ѓcantly
better than it could achieve by just guessing a random g to begin with. More formally:

Deп¬Ѓnition 2 (IND-CCA2) A public key encryption scheme consisting of three algorithms,
S = (gen, enc, dec), is called indistinguishable against adaptive chosen ciphertext attack if
the following properties hold for any negligible function neg() and all large enough values of
the security parameter k with corresponding message space Mk :

Completeness: For all m в€€ Mk ,

Pr[ (kpub , kpriv ) в†ђ gen(1k );
c в†ђ enc(kpub , m);
m = dec(kpriv , c) ] > 1 в€’ neg(k)

oracle D,

Pr[ (kpub , kpriv ) в†ђ gen(1k );
(m0 , m1 ) в†ђ AD(kpriv ,В·) (kpub , 1k );
R
b в†ђ {0, 1} ;
cв€— = enc(kpub , mb )
в€— ,В·)
(kpub , cв€— , 1k ) :
1
b=g ]< + neg (k)
2

The extra completeness property ensures that a message remains the same after under-
going encryption and decryption. We deп¬Ѓne negligible functions as follows:

Deп¬Ѓnition 3 (Negligible Functions) A function f : N в†’ R is negligible in k if, for
1
any polynomial q, f (k) в‰¤ for all suп¬ѓciently large k. If f is negligible in k, we write
q(k)

f в‰¤ neg(k).

2.2.2 Digital Signatures

Digital signatures are used when a party wants to indicate they have originated a message
m. A digital signature Пѓ is dependent on some secret known only to the signer and on

16
the message being signed. The recipient of (m, Пѓ) can then run a public veriп¬Ѓcation algo-
rithm that will conп¬Ѓrm or reject the messageвЂ™s signature without requiring knowledge of
the signerвЂ™s secret. In this thesis, we will restrict our attention to schemes that accomplish
this using signing and veriп¬Ѓcation keys.
We also restrict our attention to party behavior or signature schemes that somehow bind
signatures to their messages вЂ“ this may be through the use of message revealing signatures
(where one can derive m from Пѓ) or by treating a non-message revealing signature as invalid
unless explicitly attached to a particular message. For clarity of expression, we adopt the
latter practice and will always pair signatures with their messages in our examples.
More formally, we deп¬Ѓne a digital signature scheme as follows:

Deп¬Ѓnition 4 (Digital Signatures) A digital signature scheme consists of three algorithms
(gen, sig, ver):

вЂў gen : 1k в†’ K Г— K , is a key generation algorithm. K and K are the sets of possible
signing and veriп¬Ѓcation keys, respectively.

вЂў sig : K Г— M в†’ S, is a signing algorithm. M and C are the sets of possible messages
and signatures, respectively.

вЂў ver : K Г— M Г— S в†’ B, is a veriп¬Ѓcation algorithm. It outputs a boolean bit indicating
whether it accepts or rejects the message signature pair.

A common deп¬Ѓnition for signature security is existential unforgeability under adaptive
chosen message attack (EUF-ACMA). As with IND-CCA2, we can describe the security
condition as a game between the adversary and the environment/challenger (Figure 2-2).
The challenger runs (ks , kv ) в†ђ gen(1k ) and hands veriп¬Ѓcation key kv to A, the adversary.
The challenger then gives ks to a signing oracle S. A can (adaptively) query S with messages
mi and receive back the corresponding signatures Пѓi в†ђ sig(ks , mi ). After some polynomial
number of queries, the adversary outputs a new message m that was never submitted as
a query to S, and a signature forgery Пѓ. If ver(kv , m, Пѓ) = 1, then the adversary wins.
A scheme is considered EUF-ACMA if no adversary is able to win with non-negligible
probability. We call the interaction between the adversary and the signing oracle an adaptive
chosen message attack (ACMA)

17
Existentially unforgeable under adaptive chosen message attack (EUF-ACMA)
1k time
-
gen
 (ks , kv )
kv -
mi
ks- 
(m0 , Пѓ0 )
Challenger -
... A
S
mpoly(k)

(mpoly(k) , Пѓpoly(k) )
-
(m, Пѓ)


? ?
?
m = mi , for all 0 в‰¤ i в‰¤ poly(k)
& ver(kv , m, Пѓ) = 1

Figure 2-2: The EUF-ACMA game

Deп¬Ѓnition 5 (EUF-ACMA) A signature scheme consisting of three algorithms, ОЈ =
(gen,sig,ver), is called existentially unforgeable under adaptive chosen message attack (EUF-
ACMA) if the following properties hold for any negligible function neg() and all large enough
values of the security parameter k with corresponding message space Mk :

Completeness: For all m в€€ Mk ,

Pr[ (ks , kv ) в†ђ gen(1k );
Пѓ в†ђ sig(s, m);
0 в†ђ ver(m, Пѓ, v) ] < neg(k)
.

Unforgeability: For any PPT forger A with access to signing oracle S,

Pr[ (ks , kv ) в†ђ gen(1k );
(m, Пѓ) в†ђ AS(ks ,В·) :
1 в†ђ ver(m, Пѓ, kv ) and A never asked S to sign m ] < neg(k)

EUF-ACMA security allows for multiple valid signatures on the same message вЂ“ there
are some situations that require a stronger deп¬Ѓnition of security. For example, there are

18
non-malleable unique signature schemes, which are schemes resilient to an ACMA with
only one valid signature for a given message and veriп¬Ѓcation key. Even stricter are one-time
signature schemes, schemes that only sign one message once for a given veriп¬Ѓcation key.
There is, however, a security deп¬Ѓnition that is stronger than EUF-ACMA but weaker
than unique signatures. Schemes that meet this alternative security deп¬Ѓnition are called
1
вЂњstrongвЂќ [31, 5] or вЂњsuper-secureвЂќ . Usage of strong signatures are not as common as
EUF-ACMA or one-time signatures, but there are situations where one-time signatures are
used when only strong signatures are necessary .
Strong security is very similar to EUF-ACMA вЂ“ in fact, their deп¬Ѓnitions diп¬Ђer only
slightly. In the deп¬Ѓnition of EUF-ACMA, the adversary is required to output a valid
message/signature pair (m, Пѓ) where m was never a query to the signing oracle. For strong
security, we make the adversaryвЂ™s game easier: in order to win, it must output a valid pair
(m, Пѓ), where (m, Пѓ) itself was never a response from the oracle. Referring back to the
EUF-ACMA game in Figure 2-2, the strong signature game is the same as replacing the
second-to-last line with вЂњ(m, Пѓ) = (mi , Пѓi ) for all 0 в‰¤ i в‰¤ poly(k).вЂќ We consider this to be an
easier game since any adversary that wins the EUF-ACMA game wins the strong signature
game as well. By making the game easier, we make our security deп¬Ѓnition stronger. A
strong signature scheme not only guarantees that past signatures donвЂ™t help for forging
signatures on new messages, but that they also donвЂ™t help for forging new signatures on old
messages.

Deп¬Ѓnition 6 (Strong Signature Schemes) A signature scheme consisting of three algo-
rithms, ОЈ = (gen,sig,ver), is called strong if the following properties hold for any negligible
function neg() and all large enough values of the security parameter k with corresponding
message space Mk :

Completeness: For any m в€€ Mk ,

Pr[ (s, v) в†ђ gen(1k );
Пѓ в†ђ sig(s, m);
0 в†ђ ver(m, Пѓ, v) ] < neg(k)
.
1
This is a diп¬Ђerent deп¬Ѓnition of вЂњsecure signaturesвЂќ than the one presented by Goldwasser, Micali, and
Yao in 1983  which was eventually renamed EUF-ACMA security

19
Strict Unforgeability: For any PPT forger F with access to signing oracle S,

Pr[ (s, v) в†ђ gen(1k );
(m, Пѓ) в†ђ F S(s,В·) :
1 в†ђ ver(m, Пѓ, v) and F never received (m, Пѓ) from S ] < neg(k)

2.3 Formal Cryptography

Formal cryptography uses mathematical or logical systems to analyze protocols. The results
of such analysis, however, do not directly apply to real protocols because of the high level of
abstraction used. For the purpose of this thesis, we will focus on symbolic analysis and the
Dolev-Yao model. We п¬Ѓrst describe symbolic analysis and its importance in general terms,
before describing the speciп¬Ѓcs of the Dolev-Yao model.

2.3.1 Symbols and Rules

In symbolic analysis, we think of messages as symbols and cryptographic operations as sym-
bolic operations on these messages. For example, if we had a message that we represented
with the symbol m, then the ciphertext of m encrypted under a public key K would be
the symbol {|m|}K , where we let {|В·|} represent encryption. If we have an entity, we can
represent the entityвЂ™s initial knowledge as a set S of symbols. We can then write rules
governing the way new symbols are formed and handled based on what the entity knows
already. Given this initial set S , we can talk about the closure of S (denoted as C[S ]) which
is the result of applying these rules. Continuing with public key encryption, we might write
the following rules:

1. S вЉ† C[S ]

2. If m в€€ C[S ] and K в€€ C[S ], then {|m|}K в€€ C[S ]

3. If {|m|}K в€€ C[S ] and K в€’1 в€€ C[S ], then m в€€ C[S ] (where K в€’1 is K вЂ™s corresponding
secret key)

Rule 1 says that anything the entity knows, it can derive. Rule 2 says that if the entity
can derive a message and a public key, then the entity can derive the ciphertext of the
message under the key. Lastly, Rule 3 says that if the entity can derive a ciphertext under

20
a particular public key and can also derive the corresponding private key, then the entity
can derive the ciphertextвЂ™s plaintext.
We generally think of the formal model adversary as being in complete control of the
network it is a part of. The ability to represent the knowledge of an adversary during
a protocol run is important for this allows an analyzer to determine what messages an
adversary is capable of creating when trying to attack the protocol. The closure operation
does this, allowing a protocol checker to iterate all plausible attacks.

2.3.2 The Dolev-Yao Model

The Dolev-Yao model is a popular model for symbolic analysis which serves as the founda-
tion for a number of formal methods. There are many variants on the Dolev-Yao model and
we deп¬Ѓne one that serves our purpose of analyzing public key encryption. We also include
the notion of a local output as proposed in .
The п¬Ѓrst thing to deп¬Ѓne is the set of atomic symbols from which the Dolev-Yao algebra
is constructed.

Deп¬Ѓnition 7 (The Dolev-Yao Message Algebra) Messages in the Dolev-Yao algebra
A are composed of atomic elements of the following types:

вЂў Party identiп¬Ѓers (M) вЂ“ These are denoted by symbols P1 , P2 , .. for a п¬Ѓnite number
of names in the algebra. These are public and are associated with a role of either
Initiator or Responder.

вЂў Nonces (R) вЂ“ These can be thought of as a п¬Ѓnite number of private, unpredictable
random-strings. These symbols are denoted by R1 , R2 , ... and so on.

e e
вЂў Public keys (KP ub ) вЂ“ These are denoted by symbols KP1 , KP2 , ... which are public and
each associated with a particular party identiп¬Ѓer.

вЂў A garbage term, written G, to represent ill-formed messages,

вЂў вЉҐ, to represent an error or failure,

вЂў Starting , to indicate that a protocol execution has begun, and

вЂў Finished , to indicate that a protocol execution has ended.

21
Messages in the algebra can be compounded by the following symbolic operations:

вЂў pair: A Г— A в†’ A. When messages m and m are paired, we write m|m .

e
вЂў encrypt : KP ub Г— A в†’ A. When message m is encrypted with public key KP , we write
{|m|}K e
P

.
The Dolev-Yao algebra is free, meaning that no two distinct symbols represent the same
message. An important consequence of this is that we can deп¬Ѓne a parse tree for each
message which describes the unique symbolic structure of the message (see Figure 2-3).

e
R1 | {|P1 |}K e |R2 | KP0 e
KP
e
P0 KP 0 e
KP
1
1

e
R1 | {|P1 |}K e |R2 | KP0 e
KP1
e
KP
e
P0 KP 0
1

v
R1 | {|P1 |}K e |R2 KP0 e
KP
e
P0 KP 0
1

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

R1 | {|P1 |}K e R2
P0

{|P1 |}K e
R1 P0

e
KP0
P1

Figure 2-3: Example Dolev-Yao parse tree

22
As mentioned in Section 2.3.1, one of the major beneп¬Ѓts of describing the world using
symbols is that we can enumerate the messages it is possible for an entity to make, based
on the symbols it already knows. In particular, we assume that the adversary completely
controls the network, but that any message delivered by the adversary must be derivable
from the adversaryвЂ™s initial knowledge and the messages communicated by honest parties.
The adversaryвЂ™s initial knowledge consists of all public keys (KP ub ), all identiп¬Ѓers (M),
and those nonces that the adversary itself generates (RAdv ). To derive new messages, the
adversary has only a few symbolic operations available to it: pairing two known elements,
separating a pair, encrypting with public keys, and decrypting messages whose keys belong
to corrupted parties (MAdv вЉ‚ M).
This restriction on the adversaryвЂ™s ability to derive messages is captured by the Dolev-
Yao closure operation:

Deп¬Ѓnition 8 (Closure) Let

вЂў RAdv вЉ‚ R be the set of nonces associated with the adversary,

e e
вЂў KAdv = {KP : P в€€ MAdv } be the set of encryption keys belonging to corrupted parties
e
(KAdv вЉ‚ KP ub ), and

Then the closure of a set S в€€ A, written C[S ], is the smallest subset of A such that:

1. S вЉ† C[S ],

2. M в€Є KP ub в€Є RAdv вЉ† C[S ],

e
3. If {|m|}K в€€ C[S ] and K в€€ KAdv , then m в€€ C[S ],

4. If m в€€ C[S ] and K в€€ KP ub , then {|m|}K в€€ C[S ],

5. If m|m в€€ C[S ], then m в€€ C[S ] and m в€€ C[S ], and

6. If m в€€ C[S ] and m в€€ C[S ], then m|m в€€ C[S ].

Symbolic Protocols
 << Пред. стр. страница 2(всего 9)ОГЛАВЛЕНИЕ След. стр. >>