6. Mihir Bellare & Phillip Rogaway 1993. Entity Authentication and Key Distribution, in Dou-

glas R. Stinson (ed), Proceedings of Advances in Cryptology - CRYPTO 1993. Lecture Notes

in Computer Science 773/1993: 110“125

7. Bruno Blanchet 2006. A Computationally Sound Mechanized Prover for Security

Protocols. Proceedings of IEEE Symposium on Research in Security and Privacy

2006. IEEE Computer Society Press: 140“154. Extended version available from

http://eprint.iacr.org/2005/401

8. Bruno Blanchet & David Pointcheval 2006. Automated Security Proofs with Sequences of

Games, in Cynthia Dwork (ed), Proceedings of Advances in Cryptology “ CRYPTO 2006.

Lecture Notes in Computer Science 4117/2006: 537“554

9. Ran Canetti 2000. Universally Composable Security: A New Paradigm

for Cryptographic Protocols. Cryptology ePrint Archive, Report 2000/067.

http://eprint.iacr.org/2000/067/

10. Ran Canetti & Marc Fischlin 2001. Universally Composable Commitments, in Joe Kilian

(ed), Proceedings of Advances in Cryptology “ CRYPTO 2001. Lecture Notes in Computer

Science 2139/2001: 19“40

References 203

11. Hao Chen, John A. Clark & Jeremy L. Jacob 2004. Synthesising Ef¬cient and Effective Se-

curity Protocols, in Alessandro Armando and Luca Vigan´ (eds), Proceedings of 2nd In-

o

ternational Joint Conference on Automated Reasoning “ ARSPA 2004. Electronic Notes in

Theoretical Computer Science 125(1): 25“41

12. John A. Clark & Jeremy L. Jacob 2000. Searching for a Solution: Engineering Tradeoffs and

the Evolution of Provably Secure Protocols, in Proceedings of IEEE Symposium on Security

and Privacy 2000. IEEE Computer Society Press: 82“95

13. John A. Clark & Jeremy L. Jacob 2001. Protocols are Programs too: The Meta-Heuristic

Search for Security Protocols. Information & Software Technology 43(14): 891“904

14. Vladimir Lifschitz 1999. Answer Set Planning, in Michael Gelfond, Nicola Leone & Ger-

ald Pfeifer (eds), Proceedings of 5th International Conference on Logic Programming and

Nonmonotonic Reasoning “ LPNMR 1999. Lecture Notes in Computer Science 1730/1999:

373“374

15. Hoon Wei Lim & Kenneth G Paterson 2006. Secret Public Key Protocols Revisited, in Pro-

ceedings of Security Protocols Workshop 2006. Lecture Notes in Computer Science. Avail-

able from http://www.isg.rhul.ac.uk/˜hwlim/

16. Alfred J Menezes, Paul C van Oorschot & Scott A Vanstone 1997. Handbook of Applied

Cryptography. CRC Press

17. Ik Rae Jeong, Jonathan Katz & Dong Hoon Lee 2004. One-Round Protocols for Two-Party

Authenticated Key Exchange, in Markus Jakobsson, Moti Yung & Jianying Zhou (eds), Pro-

ceedings of Applied Cryptography and Network Security - ACNS 2004. Lecture Notes in

Computer Science 3089/2004: 220“232

18. Hugo Krawczyk 2005. HMQV: A High-Performance Secure Dif¬e“Hellman Protocol,

in Victor Shoup (ed), Proceedings of Advances in Cryptology - CRYPTO 2005. Lec-

ture Notes in Computer Science 3621/2005: 546“566. Extended version available from

http://eprint.iacr.org/2005/176/

19. Caroline Kudla & Kenneth G Paterson 2005. Modular Security Proofs for Key Agreement

Protocols, in Bimal Roy (ed), Proceedings of Advances in Cryptology - ASIACRYPT 2005.

Lecture Notes in Computer Science 3788/2005: 549“569

20. Peter Ochsenschl¨ ger, Jurgen Repp, Roland Rieke & U Nitsche 1998. The SH-Veri¬cation

a

Tool - Abstraction-Based Veri¬cation of Co-operating Systems. Journal of Formal Aspects of

Computing 10(4): 381“404

21. Phillip Rogaway 2004. MOn the Role De¬nitions in and Beyond Cryptography, in Michael J

Maher (ed), Proceedings of 9th Asian Computing Science Conference - ASIAN 2004. Lecture

Notes in Computer Science 3321/2004: 13“32

22. Stuart Russell & Peter Norvig 1995. Arti¬cial Intelligence: A Modern Approach. Prentice

Hall

23. Daniel S Weld 1999. Recent Advances in AI Planning. AI Magazine 20(2): 93“123

Chapter 12

Conclusion and Future Work

In this ¬nal chapter, a summary of the book and a discussion of open problems and

possible research directions are presented.

12.1 Research Summary

In this book, we have achieved all the four research goals identi¬ed in Chapter 1.2.3

as explained below.

1: To examine the computational complexity models critically.

• In Chapter 3, we studied the BR95 model and revealed that its partnership

function used in the 3PKD protocol [8] is ¬‚awed, which invalidates the proof

for the 3PKD protocol.

• In Chapter 4, we studied the Bellare“Rogaway models and the CK2001 model

and identi¬ed several variants of the key sharing requirement.

• In Chapter 5, we presented a comparison of the relative strengths of the no-

tions of security between the variants of the Bellare“Rogaway models and the

CK2001 model. We then demonstrated that protocol 3PAKE of Abdalla and

Pointcheval [1], though proven secure in the BPR2000 model, is vulnerable

to an unknown key share attack. This attack illustrated the drawback of the

BPR2000 model.

• In Chapter 6, we extended the BR93 model to model the compromise of long-

term keys, not currently captured in the existing model.

2: To analyse published protocols in the literature.

• In Chapters 3, 4, and 8, we revealed new ¬‚aws in several published protocols

and a message authenticator of Bellare, Canetti, and Krawczyk [7]. We then

pointed out the corresponding ¬‚aws in their proofs and proposed solutions to

these protocols and their proofs. We also identi¬ed three areas where protocol

proofs are likely to fail; namely an inappropriate proof model environment,

205

206 12 Conclusion and Future Work

Send, Reveal and Corrupt queries not adequately considered in the proof sim-

ulations, and the omission of proof simulations in Chapter 8.

• In Chapters 10 and 11, we used our formal framework to reveal new ¬‚aws in

several protocols.

3: To contribute towards the design principles.

• In Chapter 9, we proposed a way to construct session keys in protocols which

can result in signi¬cant bene¬ts for the security of the protocols. We pro-

pose keying materials, comprising the identities of the participants and roles,

unique session identi¬ers (SIDs), and some other ephemeral shared secrets

and/or long-term (static) shared secrets, to be included in the key derivation

function.

Note that our observation on the session key construction is cited in a special

publication (SP 800-56A) “ Recommendation for Pair-Wise Key Establish-

ment Schemes Using Discrete Logarithm Cryptography by National Institute

of Standards and Technology (NIST) [6].

• In Chapter 10, we provided a formal speci¬cation and machine analysis of the

BPR2000 model that can be used to reveal structural ¬‚aws in protocols. Such

an approach is complementary to the computational complexity approach. We

then extend this framework to automatically repair protocols found to be in-

secure in Chapter 11.

4: To design new provably secure and ef¬cient protocols.

• In Chapters 3 and 4, we presented improved provably-secure 3PKD protocols

and an improved Protocol T S 2. The improved 3PKD protocol proposed in

Chapter 4 is included in a submission to the IEEE 802.11, the working group

setting the standards for wireless LANs [2].

• In Chapter 6, we proved a revised protocol of Boyd [11] secure in the BR93

model. We also proposed an alternative protocol that is ef¬cient in both rounds

and messages, and proved it secure in the BR93 extended model.

In our results, we demonstrated the importance of rigorous proofs of security against

active attacks in a well-de¬ned and robust model and that specifying correct proofs

for protocols remains a hard problem. More importantly, we believe the techniques

and methods outlined in this book represent a step toward a better understanding in

the construction of provably-secure key establishment protocols.

12.2 Open Problems and Future Directions

Much work in this area remains to be done. We list several interesting dimensions

on how this research can be extended.

12.2 Open Problems and Future Directions 207

Extending our work in Chapter 5. While our studies in Chapter 5 focus only on

the Bellare“Rogaway and Canetti“Krawczyk models, it would be interesting to

extend our work to other computational complexity proof models (e.g., the proof

model due to Shoup [18]) or other simulation-based proof models (e.g., the uni-

versal composability approach and the black-box simulatability approach due to

Canetti et al. [12, 13, 14] and Backes et al. [3, 4, 5] respectively).

Extending our work in Chapter 6 While our work in Chapter 6 allows us to de-

tect a known weakness of key agreement protocol of Boyd [11] that cannot be