LINEBURG

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.

84

(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

85

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

F2ma

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.

86

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 — {} ’

e

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

v

P KA

output

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

A

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

e

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

v

B KP

S ⊥ — B, P {|B|RP |}K e — message —

P

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

2

This de¬nition is based upon a variant of the SPLICE protocol proposed by Clark and Jacob [20], as

presented in [10].

87

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,

A

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

B

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

v

B KA

symbol {|A, RA |}K e , then that message would have been of the wrong form. Since B has

B

e

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

v

B KA

e

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).

88

Chapter 8

Future Research Directions

8.1 An EUF-ACMA Realizable Ideal Signature Functional-

ity

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

sig

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Σ .

sig

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

89

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.

90

Bibliography

[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-

±n

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-

±n

putational soundness of formal encryption). Journal of Cryptology, 15(2):103“127,

2002.

[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,

http://eprint.iacr.org/2003/240. 2003.

[7] Michael Backes, Brigit P¬tzmann, and Michael Waidner. Reactively Secure Signature

Schemes. In Proceedings of the 6th Information Security Conference, 2003.

91

[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, http://eprint.iacr.org/2003/239, 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, http://eprint.iacr.org/2004/334. 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.

92

[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

2004.

[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.

93

[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

192“202.

94

Copyright Design by: Sunlight webdesign