A practical and formal analysis of distributed private key generation for identity based cryptography

Abstract

Temelleri gizlilik paylaşımı yöntemlerine dayanan dağıtık gizli anahtar üretimi(DGAÜ) kriptografide gizli anahtarların dağıtık olarak güvenli bir şekilde üretilmesiamacıyla kullanılmaktadır. DGAÜ kullanımına en uygun olan kriptografik sistemlerdenbir tanesi kimlik tabanlı kriptografik sistemdir. DGAÜ kullanımı, kimliktabanlı kriptografik sistemlerde var olan ve sistemin pratik olarak kullanımındaengel teşkil eden anahtar emaneti probleminin bir çözümü olarak bilinmektedir. Her ne kadar bilinen matematikselproblemler üzerine oturmuş olsa da, öngörülmeyen açıklar içerebileceği için protokolün doğrulanması çok önemlidir. Bu tezde, DGAÜ protokolünün hem işlevsel hem de biçimsel açıdan analizi hedeflenmiştir. Bu amaçla öncelikle DGAÜ protokolü, endüstriyel kontrol sistemleri üzerinde büyük ölçüde kullanılmakta olanSCADA protokolünde eksik olan kimlik denetimi sağlanarak güvenli hale getirilmesi için uygulanmıştır ve işlevsel analiz bu uygulama üzerinde yapılmıştır. Biçimsel (formal)analiz için ise protokol basit Petri ağları kullanılarak modellenmiştir. Daha sonra bu model üzerinde yapısal ve davranışsal analizler yapılarak protokolünbiçimsel olarak doğrulanması için gerekli güvenlik özellikleriispatlanmıştır.

The basis of distributed private key generation (DPKG) scheme lies on secret sharing and it has been used in cryptography for generating keys distributively and securely. One of the most suitable cryptographic system for DPKG is identity based cryptographic system. DPKG is enormously used for generating private keys for the clients of an identity based cryptographic system. The scheme is claimed to be a solution for the key escrow problem which exists in the identity based cryptography and leads to impractical cryptographic systems. It is highly important to verify the protocol even though the protocol lies on well known mathematical problems. Clearly, the protocol might always preserve some unforeseen flaws.In this thesis, we aimed to analyze DPKG protocol in both practical and formal manners. For this aim, we implemented the protocol on industrial control systems (ICS) in order to secure the widely used ICS protocol SCADA by providing it with authentication and performed a practical analysis on the implementation. In order to perform formal analysis, we first modeled the DPKG protocol by using elementary Petri nets then we performed structural and behavioral analysis on the model for proving essential security properties of the protocol with the eventual aim of formal verification.