Completeness of a Deduction System for Relational Information between Ciphertexts Based on Probabilistic Computational Semantics
We proposed a system called JD-system for deducing relational information between contents or keys of two ciphertexts, such as “the contents of two ciphertexts are equal” or “the keys of two ciphertexts are different”. JD-system can be used as a symbolical analysis method, which is simple and easy to understand since it is regarded as abstract-level analysis by discarding a phenomenon of which probability is negligible. However, it is not clear whether JD-system is correct in the computational model where encrypted information is deciphered by computation of probabilistic polynomial-time Turing machines. In this paper, we introduce JD-system and give computational semantics to it. We also show its soundness and completeness, which are the property that we cannot deduce relational information by JD-system, if and only if it is impossible to obtain its evidence except with negligible probability by the computation.
KeywordsEncryption Scheme Relational Information Secret Message Deduction System Security Parameter
Unable to display preview. Download preview PDF.
- 4.Adao, P., Bana, G., Scedrov, A.: Computational and information-theoretic soundness and completeness of formal encryption. In: Proceedings of the 18th IEEE Computer Security Foundations Workshop (CSFW 2005), pp. 170–184. IEEE Computer Society (2005)Google Scholar
- 5.Backes, M., Pfitzmann, B.: Symmetric encryption in a simulatable dolev-yao style cryptographic library. In: Proceedings of the 17th IEEE Computer Security Foundations Workshop (CSFW), pp. 204–218 (2004)Google Scholar
- 7.Bhery, A., Hagihara, S., Yonezaki, N.: The characterization of cryptographic primitives and their security properties. In: Proceedings of the Ninth International Conference on Distributed Multimedia Systems, pp. 636–642 (2003) Google Scholar
- 8.Bhery, A., Hagihara, S., Yonezaki, N.: A formal analysis of symmetric encryption and keyed and keyed hash function. In: The 46th IEEE International Midwest Symposium on Circuits & Systems 2003 (2003)Google Scholar
- 9.Bhery, A., Hagihara, S., Yonezaki, N.: Judgment deduction system of asymmetric encryption scheme (JDE-system). In: Pre-Proceeding of WISA 2003, The 4th International Workshop on Information Security Applications, pp. 639–649 (2003)Google Scholar
- 14.Micciancio, D., Warinschi, B.: Completeness theorems for the abadi-rogaway language of encrypted expressions. Journal of Computer Security 12(1), 99–130 (2004)Google Scholar