Este trabalho analisa a influência de mecanismos de segurança, incluindo autenticação de assinante, confidencialidade e integridade de dados, sobre o desempenho do sistema celular de terceira geração Universal Mobile Communication System (UMTS). Em função do serviço e do tamanho das chaves utilizadas foram medidos, através de simulação, o nível de potência gasto pelos equipamentos de usuário (UE) e o tempo de resposta em aplicações do tipo Web. Verificou-se que os efeitos negativos produzidos pelos mecanismos de segurança são pequenos em relação à proteção maior que é obtida nos sistemas UMTS Terrestrial Radio Access Network (UTRAN) e Core Network (CN). / This work is aimed at analyzing the influence of security mechanisms, including user authentication, data confidentiality and integrity, related to system cellular performance of third generation named Universal Mobile Telecommunication System (UMTS). By the service and the size of the used keys, there has been measured through simulation, the power level spent by the user equipments and the response time at web applications usage. It is seen that negative results produced by security mechanisms are small related to the greater protection that is get on UMTS Terrestrial Radio Access Network (UTRAN) systems and Core Network (CN).

Este trabalho analisa a influência de mecanismos de segurança, incluindo autenticação de assinante, confidencialidade e integridade de dados, sobre o desempenho do sistema celular de terceira geração Universal Mobile Communication System (UMTS). Em função do serviço e do tamanho das chaves utilizadas foram medidos, através de simulação, o nível de potência gasto pelos equipamentos de usuário (UE) e o tempo de resposta em aplicações do tipo Web. Verificou-se que os efeitos negativos produzidos pelos mecanismos de segurança são pequenos em relação à proteção maior que é obtida nos sistemas UMTS Terrestrial Radio Access Network (UTRAN) e Core Network (CN). / This work is aimed at analyzing the influence of security mechanisms, including user authentication, data confidentiality and integrity, related to system cellular performance of third generation named Universal Mobile Telecommunication System (UMTS). By the service and the size of the used keys, there has been measured through simulation, the power level spent by the user equipments and the response time at web applications usage. It is seen that negative results produced by security mechanisms are small related to the greater protection that is get on UMTS Terrestrial Radio Access Network (UTRAN) systems and Core Network (CN).

The purpose of this thesis is to explore the formal verification technique of completion functions and equivalence checking by verifying two pipelined cryptographic circuits, KASUMI and WG ciphers. Most of current methods of communications either involve a personal computer or a mobile phone. To ensure that the information is exchanged in a secure manner, encryption circuits are used to transform the information into an unintelligible form. To be highly secure, this type of circuits is generally designed such that it is hard to analyze. Due to this fact, it becomes hard to locate a design error in the verification of cryptographic circuits. Therefore, cryptographic circuits pose significant challenges in the area of formal verification. Formal verification use mathematics to formulate correctness criteria of designs, to develop mathematical models of designs, and to verify designs against their correctness criteria. The results of this work can extend the existing collection of verification methods as well as benefiting the area of cryptography. In this thesis, we implemented the KASUMI cipher in VHDL, and we applied the optimization technique of pipelining to create three additional implementations of KASUMI. We verified the three pipelined implementations of KASUMI with completion functions and equivalence checking. During the verification of KASUMI, we developed a methodology to handle the completion functions efficiently based on VHDL generic parameters. We implemented the WG cipher in VHDL, and we applied the optimization techniques of pipelining and hardware re-use to create an optimized implementation of WG. We verified the optimized implementation of WG with completion functions and equivalence checking. During the verification of WG, we developed the methodology of ``skipping" that can decrease the number of verification obligations required to verify the correctness of a circuit. During the verification of WG, we developed a way of applying the completion functions approach such that it can deal with a circuit that has been optimized with hardware re-use.

The purpose of this thesis is to explore the formal verification technique of completion functions and equivalence checking by verifying two pipelined cryptographic circuits, KASUMI and WG ciphers. Most of current methods of communications either involve a personal computer or a mobile phone. To ensure that the information is exchanged in a secure manner, encryption circuits are used to transform the information into an unintelligible form. To be highly secure, this type of circuits is generally designed such that it is hard to analyze. Due to this fact, it becomes hard to locate a design error in the verification of cryptographic circuits. Therefore, cryptographic circuits pose significant challenges in the area of formal verification. Formal verification use mathematics to formulate correctness criteria of designs, to develop mathematical models of designs, and to verify designs against their correctness criteria. The results of this work can extend the existing collection of verification methods as well as benefiting the area of cryptography. In this thesis, we implemented the KASUMI cipher in VHDL, and we applied the optimization technique of pipelining to create three additional implementations of KASUMI. We verified the three pipelined implementations of KASUMI with completion functions and equivalence checking. During the verification of KASUMI, we developed a methodology to handle the completion functions efficiently based on VHDL generic parameters. We implemented the WG cipher in VHDL, and we applied the optimization techniques of pipelining and hardware re-use to create an optimized implementation of WG. We verified the optimized implementation of WG with completion functions and equivalence checking. During the verification of WG, we developed the methodology of ``skipping" that can decrease the number of verification obligations required to verify the correctness of a circuit. During the verification of WG, we developed a way of applying the completion functions approach such that it can deal with a circuit that has been optimized with hardware re-use.

Θέμα της παρούσας διπλωματικής εργασίας ήταν ο σχεδιασμός των αλγορίθμων εμπιστευτικής και ακέραιης επικοινωνίας του πρωτοκόλλου UMTS. Απώτερος στόχος υπήρξε η ενσωμάτωση τους σε φορητές συσκευές και γι’ αυτό σχεδιάστηκαν με τέτοιο τρόπο ώστε διατηρώντας μία ικανοποιητική απόδοση να μπορούν να καταλαμβάνουν όσο το δυνατόν μικρότερη επιφάνεια ολοκλήρωσης και ταυτόχρονα να καταναλώνουν όσο το δυνατόν λιγότερη ενέργεια. Οι τεχνικές που χρησιμοποιήθηκαν για να επιτευχθεί ο στόχος αυτός ήταν η βελτίωση του αλγορίθμου μαζί με την τεχνική της διοχέτευσης και τα ισορροπημένα δέντρα από πύλες XOR. / -

This master's thesis deals with the issue of the security of GSM and UMTS mobile communication systems. In the thesis the principles of the authentication and encryption of both the mobile systems are described. Further, the constituent algorithms used for identity verification, key generation and encryption are mentioned. The commonly used algorithms are described along with their weaknesses. In the following part of this thesis, well-known attacks on GSM system are mentioned. In the part where UMTS system is dealt with one can find the algorithms used in this system to increase the security of transmitted data and authentication in comparison with GSM system. Therefore the whole process of authentication and encryption is described separately. In the last part the creation of programming models of authentication and encryption in GSM and encryption in UMTS is described. These models are created in the environment of Matlab version 2009b.

The Global System for Mobile (GSM) Communication is the most widely used cellular technology. The privacy has been protected using some version of stream ciphers until the 3rd Generation of GSM. KASUMI, a block cipher, has been chosen as a standard algorithm in order to be used in 3rd Generation. In this thesis, s-boxes of KASUMI, MISTY1 (former version of KASUMI) and RIJNDAEL (the Advanced Encryption Standard) are evaluated according to their linear approximation tables, XOR table distributions and satisfaction of the strict avalanche criterion (SAC). Then, the nonlinear part, FI function, of KASUMI and MISTY1 are investigated for SAC. A new FI function is defined by replacing both s-boxes of KASUMI by RIJNDAEL&rsquo / s s-box. Calling this new version KASUMI-R, it is found to have an FI function significantly better than others. Finally, the randomness characteristics of the overall KASUMI-R for different rounds are compared to those of MISTY1 and KASUMI, in terms of avalanche weight distribution (AWD) and some statistical tests. The overall performance of the three ciphers is found to be same, although there is a significant difference in their FI functions.