Difference of Function on Vector Space over F

Kenichi Arai; Ken Wakabayashi; Hiroyuki Okazaki

Formalized Mathematics (2014)

  • Volume: 22, Issue: 3, page 269-275
  • ISSN: 1426-2630

Abstract

top
In [11], the definitions of forward difference, backward difference, and central difference as difference operations for functions on R were formalized. However, the definitions of forward difference, backward difference, and central difference for functions on vector spaces over F have not been formalized. In cryptology, these definitions are very important in evaluating the security of cryptographic systems [3], [10]. Differential cryptanalysis [4] that undertakes a general purpose attack against block ciphers [13] can be formalized using these definitions. In this article, we formalize the definitions of forward difference, backward difference, and central difference for functions on vector spaces over F. Moreover, we formalize some facts about these definitions.

How to cite

top

Kenichi Arai, Ken Wakabayashi, and Hiroyuki Okazaki. "Difference of Function on Vector Space over F." Formalized Mathematics 22.3 (2014): 269-275. <http://eudml.org/doc/271080>.

@article{KenichiArai2014,
abstract = {In [11], the definitions of forward difference, backward difference, and central difference as difference operations for functions on R were formalized. However, the definitions of forward difference, backward difference, and central difference for functions on vector spaces over F have not been formalized. In cryptology, these definitions are very important in evaluating the security of cryptographic systems [3], [10]. Differential cryptanalysis [4] that undertakes a general purpose attack against block ciphers [13] can be formalized using these definitions. In this article, we formalize the definitions of forward difference, backward difference, and central difference for functions on vector spaces over F. Moreover, we formalize some facts about these definitions.},
author = {Kenichi Arai, Ken Wakabayashi, Hiroyuki Okazaki},
journal = {Formalized Mathematics},
keywords = {Mizar formalization; difference of function on vector space over F; difference of function on vector space over },
language = {eng},
number = {3},
pages = {269-275},
title = {Difference of Function on Vector Space over F},
url = {http://eudml.org/doc/271080},
volume = {22},
year = {2014},
}

TY - JOUR
AU - Kenichi Arai
AU - Ken Wakabayashi
AU - Hiroyuki Okazaki
TI - Difference of Function on Vector Space over F
JO - Formalized Mathematics
PY - 2014
VL - 22
IS - 3
SP - 269
EP - 275
AB - In [11], the definitions of forward difference, backward difference, and central difference as difference operations for functions on R were formalized. However, the definitions of forward difference, backward difference, and central difference for functions on vector spaces over F have not been formalized. In cryptology, these definitions are very important in evaluating the security of cryptographic systems [3], [10]. Differential cryptanalysis [4] that undertakes a general purpose attack against block ciphers [13] can be formalized using these definitions. In this article, we formalize the definitions of forward difference, backward difference, and central difference for functions on vector spaces over F. Moreover, we formalize some facts about these definitions.
LA - eng
KW - Mizar formalization; difference of function on vector space over F; difference of function on vector space over
UR - http://eudml.org/doc/271080
ER -

References

top
  1. [1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990. Zbl06213858
  2. [2] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990. 
  3. [3] E. Biham and A. Shamir. Differential cryptanalysis of DES-like cryptosystems. Lecture Notes in Computer Science, 537:2-21, 1991. Zbl0787.94014
  4. [4] E. Biham and A. Shamir. Differential cryptanalysis of the full 16-round DES. Lecture Notes in Computer Science, 740:487-496, 1993. Zbl0809.94017
  5. [5] Czesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990. 
  6. [6] Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990. 
  7. [7] Czesław Bylinski. Partial functions. Formalized Mathematics, 1(2):357-367, 1990. 
  8. [8] Czesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990. 
  9. [9] Eugeniusz Kusak, Wojciech Leonczuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335-342, 1990. 
  10. [10] X. Lai. Higher order derivatives and differential cryptoanalysis. Communications and Cryptography, pages 227-233, 1994. Zbl0840.94017
  11. [11] Bo Li, Yan Zhang, and Xiquan Liang. Difference and difference quotient. Formalized Mathematics, 14(3):115-119, 2006. doi:10.2478/v10037-006-0014-z.[Crossref] 
  12. [12] Michał Muzalewski and Wojciech Skaba. From loops to Abelian multiplicative groups with zero. Formalized Mathematics, 1(5):833-840, 1990. 
  13. [13] Hiroyuki Okazaki and Yasunari Shidama. Formalization of the data encryption standard. Formalized Mathematics, 20(2):125-146, 2012. doi:10.2478/v10037-012-0016-y.[Crossref] Zbl1288.94079
  14. [14] Beata Perkowska. Functional sequence from a domain to a domain. Formalized Mathematics, 3(1):17-21, 1992. 
  15. [15] Christoph Schwarzweller. The binomial theorem for algebraic structures. Formalized Mathematics, 9(3):559-564, 2001. 
  16. [16] Wojciech A. Trybulec. Groups. Formalized Mathematics, 1(5):821-827, 1990. 
  17. [17] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291-296, 1990. 
  18. [18] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990. 
  19. [19] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990. 
  20. [20] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181-186, 1990. 
  21. [21] Hiroshi Yamazaki and Yasunari Shidama. Algebra of vector functions. Formalized Mathematics, 3(2):171-175, 1992. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.