<< . .

( 9)


1. [“deliver”, k, Pi ] for some k is the most recent adversary event in t.

2. m is the second element in the kth adversary event in the current trace.

3. Sj is the sequence of inputs and messages received by Pi before this event in t.

4. oi is Pi ™s role according to t.

These facts follow directly from the de¬nition for the symbolic counterpart of simple pro-
tocols (De¬nition 14). By its very nature, P is mimicking concrete protocol p, so the
only di¬erence between protocol traces is the naming of variables “ the structure of simple
protocols ensures that this renaming does not a¬ect protocol messages or outputs.

(2) Assume there exists an event of the form [“fail”, m]. Let M = m1 , m2 , ..., denote the
messages that are communicated by Dolev Yao parties prior to the failure event, i.e. those
that appear in the [“message”, ...] events preceding [“fail”, m] in t.
The failure event implies the concrete adversary created a message m that is translated to
a Dolev-Yao element m not in the closure of the adversary™s knowledge (f (m) = m ∈ C[M ]).
We show that the odds of such an event occurring are negligible.
Examine the parse tree of m. The only three operations available for creating compound
messages are pairing, encryption, and signatures. By de¬nition, membership in C[M ] is
closed under pairing and encryption; that is, if two siblings in the parse tree are both in
C[M ], then so is their parent. The exception is signatures “ an adversary who knows a
veri¬cation key and a message does not necessarily know the signature for the message
under that veri¬cation key.
Consequently, if every leaf or signature in the parse tree of m has a path to the tree root
with a node in C[M ], then m ∈ C[M ]. Since m ∈ C[M ], it must be the case that there is a
leaf or signature m— that has no such path node.
We thus have an adversary A that generates an m that maps to m. Using A, we construct
adversary A that will produce a bit string m— that will map to m— . A simulates A to produce
m then walks down the parse tree of m to m— while recursively applying the appropriate
deconstructors to m.

• If m is a pair ml |mr , then A separates m = “pair”, ml ||mr into ml and mr , then
walks down the parse tree to the symbol containing m— and recursively operates on
the corresponding bitstring ml or mr .

• If m is an encryption {|mc |}K , then A must decrypt [“ciphertext”, m ], i.e. produce
what Fcpke would return to the appropriate party when called with (Decrypt, m ).
Because m ∈ C[M ], the probability A could have independently produced m is
negligible, due to the statistical unpredictability of E. Thus, if there is a pair (m , mc )
stored in Fcpke , it must be that A initiated the request (Encrypt, mc ) to Fcpke . Because
A is simulating A it must have passed this request along, and so it knows what message
mc is the decryption of m . On the other hand, if there is no pair (m , mc ) stored in
Fcpke , then the decryption of m is D(m ), where D was an algorithm provided by A.
A can run D(m ) itself to obtain mc . A then walks down the parse tree to symbol mc

and recursively operates on mc .

By recursively applying the deconstruction operations, A eventually produces a string m—
that maps to an atomic symbol or signature m— . Notice that the only atomic symbols not
in the adversary™s initial view are those random nonces that were not generated by the
adversary (R \ RAdv ). If m— is a random nonce not in the closure of the adversary, then
m— was generated by an honest protocol participant and chosen uniformly from {0, 1}k ,
independent from the view of A . The probability A could generate the string m— is 2’k ;
since there are at most a polynomial number of k-bit strings that are valid nonces in this
protocol execution, the overall probability that A generates a string that maps to a valid
nonce is poly(k)2’k , which is negligible.
It must then be that m— is an honest party signature. If Fcert created m— for an honest
party, but m— ∈ C[M ], then by the statistical unpredictability of S, A can only guess the
signature with negligible probability. A couldn™t have forged a new signature for an honest
party™s key since, under the ideal functionality, honest party signatures not generated by
Fcert never verify. This means the overall probability that A produces a signature that
maps to a symbolic signature outside of C[M ] is negligible.
Thus the probability that t includes an event of form [“fail”, m] must be negligible.

7.4 Dolev-Yao Back to UC: DY Mutual Authentication and

For self-containment, we restate the mutual authentication equivalence theorem (Theorem
3) here.

Theorem 7 Let p be a simple two-party protocol. Then p realizes F2ma if and only if the
corresponding symbolic protocol p satis¬es Dolev-Yao 2-party mutual authentication

Canetti and Herzog proved Theorem 7 speci¬cally for protocols in a Fcpke -hybrid, but
made no use of the ideal functionality™s speci¬c nature. Their proof can be trivially ex-
tended to apply to protocols in any F-hybrid model containing multiple, composable ideal
functionalities, such as the ones we have de¬ned in this thesis. Thus, Theorem 7 concerning
Dolev-Yao 2-party mutual authentication (De¬nition 17) and F2ma (Figure 3-5) still holds
for our new construction of the UCSA framework.

7.5 Using The Framework

Having stepped through and proved the di¬erent components of the universally composable
symbolic analysis framework, we illustrate how it can be used by giving an informal security
proof for a variation of the SPLICE authentication protocol (Figure 7-4).2

A ’ B : A, encB (A, RA ), sigA (A, encB (A, RA ))
A←B: B, A, encB (B, RA )

Figure 7-4: The SPLICE authentication protocol

As you can see, the SPLICE protocol has the basic form required of a simple protocol
with a very natural translation to a symbolic protocol (Figure 7-5). We now show that

Let DP represent the initial input/state of party P , let — denote a wildcard which
can be used to match anything, and let P be a place holder for the party identity
each party thinks it is engaged with. We de¬ne PSP LICE to be the mappings:

• {DA } — A — Initiator — {} ’

{DA ∪ {RA }} — A| {|A|RA |}K e — message — Starting|A|P |KP —

• {DA ∪ {RA }} — A — Initiator — P |A| {|P, RA |}K e ’

S ⊥ — F inished|A|P |KP — output

• {DB } — B — Responder — P, {|P |RP |}K e ’

S ⊥ — B, P {|B|RP |}K e — message —
e |F inished|B|P |K e — output
Starting|B|P |KP P

• S⊥ — — — — — — ’

S — — ⊥ —output

Figure 7-5: The SPLICE symbolic protocol, PSP LICE
This de¬nition is based upon a variant of the SPLICE protocol proposed by Clark and Jacob [20], as
presented in [10].

PSP LICE achieves Dolev-Yao 2-party mutual authentication (as stated in De¬nition 17).
If A outputs that it has ¬nished PSP LICE with party B, this means it must have received
symbolic message B|A| {|B, RA |}K e . By the security o¬ered by public key encryption,

this could have only happened if B received (and decrypted) the symbol {|A, RA |}K e .

Thanks to the underlying universally composable framework, if B is honest then the only
way B would have produced a message containing the string RA is if it had received the
entire message A| {|A|RA |}K e . If it had received any other message containing

symbol {|A, RA |}K e , then that message would have been of the wrong form. Since B has
received this message, B has output F inished|B|A|KA .
Similarly if B outputs that it has ¬nished the PSP LICE protocol with A, this means
it must have received symbolic message A| {|A|RA |}K e . If A is honest, then only A
could have created this message, which implies the trace contains the event Starting|A|B|KB .
Thus both the Initiator and Responder in this protocol will only produce a successful
F inished output if the other has produced the proper Starting output. This means the
symbolic version of SPLICE (PSP LICE ) meets the Dolev-Yao 2-party mutual authentication
criteria. Now, thanks to the UCSA framework, we can further assert that the real world
SPLICE protocol “ implemented using a su¬ciently secure key distribution system, strong
signatures, and IND-CCA2 public key encryption “ securely realizes ideal 2-party mutual
authentication (Figure 3-5).

Chapter 8

Future Research Directions

8.1 An EUF-ACMA Realizable Ideal Signature Functional-

The previous de¬nition of Fsig [15] showed equivalence with EUF-ACMA and intuitively
there does not appear to be a compelling reason why the introduction of an ideal encryption
functionality should change this. The attack described in Section 4.3.3 is certainly valid,
but it seems like an ideal functionality should be able to protect against such an attack
without heightening the security needed to realize it. Here are two possible ways to de¬ne
variants of Fsig which might achieve this goal:

1. The level of abstraction used in Fsig is lessened by parameterizing it with a speci¬c
signature scheme Σ in order to obtain a FΣ which still enforces the core ideal signature

functionality, but behaves in a manner consistent with Σ for extraneous cases (like
handling forged signatures for messages that have existing signatures). While it may
lead to more ¬‚exible secure realizations, this solution is somewhat undesirable in the
UCSA framework since it would necessitate reproving the Mapping Lemma for each
distinct instance of FΣ .

2. We take advantage of the fact that, in the UCSA framework, the actions of honest
parties are limited to those allowed under simple protocols. This limits the power of
the environment when trying to distinguish between interactions in the real and ideal
worlds. In our Chapter 6 proofs, we protected against an environment which could
perform any e¬ciently computable operation messages “ it may be possible to de¬ne a

weaker ideal signature scheme (Fsig|SP ) which can be securely realizes by EUF-ACMA
in an environment hampered by the restrictions of simple protocols.

8.2 Other primitives and protocol goals

As this thesis shows, the UCSA framework can be extended to include protocols that use
multiple cryptographic primitives. We are now limited to protocols using public key en-
cryption and digital signatures, but as more primitives are added to the framework, the set
of analyzable protocols will become richer. New protocol goals can also be added, allowing
analysis of protocols with goals other than 2-party mutual authentication and key exchange.

8.3 Mixing Ideal Functionalities

Part of what makes the UC framework so powerful is the ability to abstract concrete schemes
and protocols into ideal functionalities which can be used by other protocols as subroutines,
secure in the knowledge that there are no potential problems arising from the composing
of multiple lower-level components. There is, however, a lack of assured compatibility for
di¬erent ideal functionalities used in the same protocol. In general, ideal functionalities
have been formulated with the mentality that they are the sole functionality being used by
a protocol or that they are being used in conjunction with other functionalities with which
no con¬‚ict could arise. As Chapter 4 showed, this is not the case “ ideal functionalities can
run into problems when combined with other functionalities within a protocol. The UC
and UCSA frameworks would both be greatly empowered by a methodology for assuring
the compatibility of ideal functionalities within a protocol.


[1] Proceedings of the 12th IEEE Computer Security Foundations Workshop (CSFW 12).
IEEE Computer Society, June 1999.

[2] Mart´ Abadi and Jan J¨rjens. Formal eavesdropping and its computational interpre-
±n u
tation. In Naoki Kobayashi and Benjamin C. Pierce, editors, Proceedings, 4th Interna-
tional Symposium on Theoretical Aspects of Computer Software TACS 2001, volume
2215 of Lecture Notes in Computer Science, pages 82“94. Springer, 2001.

[3] Mart´ Abadi and Phillip Rogaway. Reconciling two views of cryptography (the com-
putational soundness of formal encryption). IFIP International Conference on Theo-
retical Computer Science (IFIP TCS2000), volume 1872 of Lecture Notes in Computer
Science, pages 3“22, August 2000.

[4] Mart´ Abadi and Phillip Rogaway. Reconciling two views of cryptography (the com-
putational soundness of formal encryption). Journal of Cryptology, 15(2):103“127,

[5] Jee Hea An, Yevgeniy Dodis, Tal Rabin. On the Security of Joint Signature and
Encryption. Lecture Notes in Computer Science, page 83. Volume 2332, Jan 2002,

[6] Michael Backes and Dennis Hofheinz. How to Break and Repair a Uni-
versally Composable Signature Functionality. Cryptology ePrint Archive, 2003.

[7] Michael Backes, Brigit P¬tzmann, and Michael Waidner. Reactively Secure Signature
Schemes. In Proceedings of the 6th Information Security Conference, 2003.

[8] M. Bellare, R. Canetti, and H. Krawczyk. A modular approach to the design and
analysis of authentication and key exchange protocols. In Proc. 30th Annual ACM
Symposium on Theory of Computing (STOC), pages 419“428, 1998.

[9] Bruno Blanchet. Automatic proof of strong secrecy for security protocols. In Proceed-
ings, 2004 IEEE Symposium on Security and Privacy, pages 86“102, 2004.

[10] Colin Boyd and Anish Mathuria. Protocols for Authentication and Key Establishment.
Springer, 2003.

[11] Dan Boneh, editor. Advances in Cryptology - CRYPTO 2003, volume 2729 of Lecture
Notes in Computer Science. Springer-Verlag, August 2003.

[12] Ran Canetti. Security and composition of multiparty cryptographic protocols. Journal
of Cryptology, 13(1):143“202, 2000.

[13] Ran Canetti. Universal composable security: A new paradigm for cryptographic pro-
tocols. In 42nd Annual Syposium on Foundations of Computer Science (FOCS 2001),
pages 136“145. IEEE Computer Society, October 2001.

[14] Ran Canetti. Universally composable signatures, certi¬cation, and authentication.
Cryptology ePrint Archive,, 2003.

[15] Ran Canetti. Universally composable signature, certi¬cation, and authentication. In
Proceedings of the 17th IEEE Computer Security Foundations Workshop (CSFW 16),
pages 219“233. IEEE Computer Society, June 2004.

[16] Ran Canetti and Jonathon Herzog Universally Composable Symbolic Analysis of Cryp-
tographic Protocols (The Case of Encryption-Based Mutual Authentication and Key
Exchange) Cryptology ePrint Archive, 2004.

[17] Ran Canetti and Hugo Krawczyk. Analysis of key-exchange protocols and their use
for building secure channels. In Birgit P¬tzmann, editor, Advances in Cryptology -
Eurocrypt 2001, volume 2045 of Lecture Notes in Computer Science, pages 453“474.
Springer-Verlag, May 2001.

[18] Ran Canetti, Hugo Krawczyk, and Jesper Buus Nielsen. Relaxing chosen-ciphertext
security. In Boneh [11], pages 565“582.

[19] Ran Canetti and Tal Rabin. Universal composition with joint state. In Boneh [11],
pages 265“281.

[20] John Clark and Jeremy Jacob. On the security of recent protocols. Information Process-
ing Letters, 56(3):151-155, November 1995.

[21] D. Dolev, C. Dwork, and M. Naor. Non-malleable cryptography. SIAM Journal of
Computing, 30(2):391“437, 2000.

[22] D. Dolev and A. Yao. On the security of public-key protocols. Proceedings of the IEEE
22nd Annual Symposium on Foundations of Computer Science, pages 350“357, 1981.

[23] Oded Goldreich. Foundations of Cryptography”Volume II (Basic Applications). Cam-
bridge University Press, 2004.

[24] Sha¬ Goldwasser, Silvio Micali, Andy Yao Strong signature schemes. Proceedings of the
15th Annual ACM symposium on Theory of Computing (STOC ™83), pages 431“439.
ACM Press, 1983

[25] Jonathan Herzog. Computational Soundness for Standard Assumptions of Formal
Cryptography. PhD thesis, Massachusetts Institute of Technology, May 2004.

[26] Gavin Lowe. An attack on the Needham“Schroeder public-key authentication protocol.
Information Processing Letters, 56:131“133, 1995.

[27] Gavin Lowe. Breaking and ¬xing the Needham“Schroeder public-key protocol using
FDR. In Margaria and Ste¬en, editors, Tools and Algorithms for the Construction
and Analysis of Systems, volume 1055 of Lecture Notes in Computer Science, pages
147“166. Springer“Verlag, 1996.

[28] Daniele Micciancio and Bogdan Warinschi. Soundness of formal encryption in the
presence of active adversaries. In Proceedings, Theory of Cryptography Conference,
number 2951 in Lecture Notes in Computer Science, pages 133“151. Springer, February

[29] John C. Mitchell, Mark Mitchell, and Ulrich Stern. Automated analysis of crypto-
graphic protocols using Mur•. In Proceedings, 1997 IEEE Symposium on Security and
Privacy, pages 141“153. IEEE, Computer Society Press of the IEEE, 1997.

[30] Roger Needham and Michael Schroeder. Using encryption for authentication in large
networks of computers. Communications of the ACM, 21(12):993“999, 1978.

[31] Amit Sahai Non-Malleable Non-Interactive Zero Knowledge and Adaptive Chosen-
Ciphertext Security In Proceedings of 40th Annual IEEE Symposium on Foundations
of Computer Science (FOCS), 1999.

[32] D. Song. Athena, an automatic checker for security protocol analysis. In Proceedings
of the 12th IEEE Computer Security Foundations Workshop (CSFW 12) [1], pages


<< . .

( 9)

Copyright Design by: Sunlight webdesign