Completeness of a Deduction System for Relational Information between Ciphertexts Based on Probabilistic Computational Semantics

  • Shigeki Hagihara
  • Hiroaki Oguro
  • Naoki Yonezaki
Conference paper
Part of the Proceedings in Information and Communications Technology book series (PICT, volume 5)


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.


Encryption Scheme Relational Information Secret Message Deduction System Security Parameter 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abadi, M., Jürjens, J.: Formal Eavesdropping and Its Computational Interpretation. In: Kobayashi, N., Babu, C. S. (eds.) TACS 2001. LNCS, vol. 2215, pp. 82–94. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  2. 2.
    Abadi, M., Rogaway, P.: Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption). In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol. 1872, pp. 3–22. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  3. 3.
    Abadi, M., Rogaway, P.: Reconciling two views of cryptography (the computational soundness of formal encryption). Journal of Cryptology 15(2), 103–127 (2002)MathSciNetMATHGoogle Scholar
  4. 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. 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
  6. 6.
    Bana, G., Mohassel, P., Stegers, T.: Computational Soundness of Formal Indistinguishability and Static Equivalence. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 182–196. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  7. 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. 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. 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
  10. 10.
    Bhery, A., Hagihara, S., Yonezaki, N.: A Formal System for Analysis of Cryptographic Encryption and Their Security Properties. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) ISSS 2003. LNCS, vol. 3233, pp. 87–112. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  11. 11.
    Canetti, R., Herzog, J.C.: Universally Composable Symbolic Analysis of Mutual Authentication and Key-Exchange Protocols. In: Halevi, S., Rabin, T. (eds.) TCC 2006. LNCS, vol. 3876, pp. 380–403. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  12. 12.
    Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983)MathSciNetMATHCrossRefGoogle Scholar
  13. 13.
    Herzog, J.: A computational interpretation of Dolev-Yao adversaries. Theoretical Computer Science 340(1), 57–81 (2005)MathSciNetMATHCrossRefGoogle Scholar
  14. 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

Copyright information

© Springer Tokyo 2012

Authors and Affiliations

  • Shigeki Hagihara
    • 1
  • Hiroaki Oguro
    • 1
    • 2
  • Naoki Yonezaki
    • 1
  1. 1.Department of Computer Science, Graduate School of Information Science and EngineeringTokyo Institute of TechnologyMeguro-kuJapan
  2. 2.SI Architecture Center, Research and Development HeadquartersNTT DATA CorporationJapan

Personalised recommendations