現今有許多公司需要強而有力的鑑別方案，此方案要能夠易於安裝、部署及管理，並能提供可靠的安全性來應變不斷變化的需求。除此之外，在目前的趨勢看來，相對於昂貴的硬體解決方案，基於軟體閘道器在企業已成為非常受歡迎的解決方案。基於軟體閘道器可以提供相當大的益處，它使得用戶端的配置不會牽涉到額外的軟體，並相容於各個終端使用者。
另外，某些協議可能會部署在基於軟體閘道器，以滿足強大的鑑別方案。來自竊聽者的欺詐及安全問題皆是待解決的問題，而解決的辦法即是藉由基於軟體閘道器安全協議的執行，但這對於安全性難以去通則化及自動化的去做分析，由於密碼協議的問題，只有透過非正規的推理與人工的努力去做分析。此外，在密碼協議的設計和分析中正規化的分析方法已成為重要手段及工具，以評估安全強度並找到在協議中的缺陷或多餘的部分。
在本論文中，我們採用BAN邏輯方法來評估SSL協議之安全性是最常見部署在基於軟體閘道器。在結論的部分得出關於SSL鑑別的可行性、實用性及安全性，它顯示出在SSL鑑別協議中證明伺服器具匿名性和身分鑑別性BAN邏輯完整性中的不足。

Many companies require strong authentication solutions that provide reliable security and easy to install and deploy, simple to manage, and adaptable for the changing needs. Furthermore, current trends indicate that software-based gateway has become extremely popular for companies instead of going for expensive hardware solutions. Software-based gateway can provide a lot of clear benefits. It enables the client configuration involves no additional software and compatible with various user terminals.
There are some protocols that are possible to be deployed in software-based gateway to meet the strong authentication solutions. The problems of fraud and security from eavesdropper need to be resolved. The solution lies in the implementation of the security protocols over software-based gateway. However, it is hard to generalize and automate the analysis for security features only by informal reasoning and manual efforts due to the subtle problems of cryptographic protocol. Furthermore, formal analysis methods have become the important means and tools in cryptographic protocol design and analysis to assess the security strength and find the flaws or redundancies in the protocol.
In this thesis we evaluate the security of SSL protocol which is the most popular deployed in software-based gateway using BAN Logic. Conclusions are then drawn about the viability, practicability and security of the mutual SSL authentication. It also shows the lack of completeness of the BAN Logic for proving the anonymous and authenticated server in SSL authentication protocol.

[1] A. Balikov, "Design and Analysis of Cryptographic Protocols," CSE P
590TU: Practical Aspects of Modern Cryptography, Winter 2006.
[2] C. Boyd and A. Mathuria, Protocols for Authentication and Key
Establishment, New York: Springer-Verlag Berlin Heidelberg, 2003.
[3] M. Burrows, M. Abadi and R. Needham, "A logic of authentication,"
ACM Transactions on Computer Systems, vol. 8, pp. 18-36, February
1990.
[4] M. Burrows, M. Abadi and R. Needham, "A Logic of Authentication,"
Palo Alto CA: Digital Equipment Corporation Systems Research Center,
1989.
[5] "COMPUTER NETWORKING PRIMER," [Online]. Available:
http://www.novell.com/info/primer/primer.pdf. [Accessed 20 May 2014].
[6] C. M. Chernick, C. Edington III, M. J. Fanto and R. Rosenthal,
"Guidelines for the Selection and Use of Transport Layer Security (TLS)
Implementations," Computer Security, NIST Special Publication 800-52,
2005.
[7] D. Cooper, S. Santesson, S. Farrell, S. Boeyen, R. Housley and W. Polk,
"Internet X.509 Public Key Infrastructure Certificate and Certificate
Revocation List (CRL) Profile," RFC 5280, May 2008.
[8] G. Coulouris, J. Dollimore and T. Kindberg, "Logic of Authentication,"
Distributed Systems, Ed. 2, pp. 503-9, 1994.
[9] D. Dolev and A. C. Yao, "On the security of public key protocols," IEEE
Trans. Information Theory, CA, 1983.
[10] L. Dong and K. Chen, Cryptographic Protocol: Security Analysis Based
on Trusted Freshness, Beijing and Springer-Verlag Berlin Heidelberg:
Higher Education Press, 2012.
[11] L. Du, X. Hu, Y. Li and G. Zhao, "A CSK based SSL handshake
60
protocol," in IC-NIDC 2009, Beijing, 2009.
[12] A. Freier, P. Karlton and P. Kocher, "The Secure Sockets Layer (SSL)
Protocol Version 3.0," RFC 6101, August 2011.
[13] M. Georgiev, S. Iyengar, S. Jana, R. Anubhai, D. Boneh and V.
Shmatikov, "The most dangerous code in the world: validating SSL
certificates in non-browser software," in Proceedings of the 2012 ACM
conference on Computer and communications security, 2012.
[14] A. Godber and P. Dasgupta, "Secure wireless gateway," in WiSE '02
Proceedings of the 1st ACM workshop on Wireless security, New York,
2002.
[15] J. Godfrey, A Comparison of Security Protocols in a Wireless Network
Environment, Ontario: University of Waterloo, 1995.
[16] S. Gupta and S. Dhir, "An Enhanced Approach to Use SSL for End To
End Security," International Journal of Computer Science and
Information Technologies, vol. 5 (2), pp. 1053-1057, 2014.
[17] S. Gurgens, "A Formal Analysis Technique for Authentication
Protocols," 1996.
[18] ISO/IEC 7498-1, "Information Technology - Open Sistem
Interconnectionl - Basic Reference Model: The Basic Model," ITU-T
Recommendation X.200, July 1994.
[19] W. Huifang and G. Jiggeng, "BAN Logic Analysis of SSL 3.0 Protocol,"
China Academic Journal Electronic Publishing House, 2001.
[20] W. H. Kao, "Security gateway utilizing ssl protocol protection and
related method". United States of America Patent US 10/904,470, July
2004.
[21] Y. J. Ma, L. P. Xiao, W. C. He and Y. B. Li, "BAN Logic Analysis of
TLS Protocol," China Academic Journal Electronic Publishing House,
2004.
[22] C. Meadows, "Formal methods for cryptographic protocol analysis:
emerging issues and trends," IEEE Journal on Selected Areas in
61
Communications, vol. 21 (1), 2003.
[23] SafeNet ASIA LTD, "Hardware and Software Authentication: Choosing
the Right Approach Decision Guide," 2010.
[24] L. Tobarra, D. Cazorla, J. J. Pardo and F. Cuartero, "Formal verification
of the secure sockets layer protocol," in 10th Int. Conf. on Enterprise
Information Systems (ICEIS’08), 2008.
[25] M. Warnier, "Bilateral Key Exchange analysed in BAN logic," February
2002. [Online]. Available: http://homepage.tudelft.nl/68x7e/Papers/
bke.pdf. [Accessed 18 May 2014].
[26] Y. Watanabe, M. Otani, H. Eto, K. Watanabe and S.-i. Tadaki, "Control
of users’ sessions and IP dual stack for captive portal type of
authentication system," 2005. [Online]. Available: http://arita.cc.sagau.
ac.jp/opengate/preprint0703.pdf. [Accessed 26 May 2014].
[27] J. Wessels, "Applications of BAN-Logic," CMG Finance B.V., 2001.
[28] H. Xia and J. Brustoloni, "Detecting and Blocking Unauthorized Access
in Wi-Fi Networks," in Networking 2004, vol. 3042, Springer Berlin
Heidelberg, 2004, pp. 795-806.