Formal definition of probability on finite and discrete sample space for proving security of cryptographic systems using Mizar

Hiroyuki Okazaki, Yuichi Futa, Yasunari Shidama


Security proofs for cryptographic systems are very important. The ultimate objective of our study is to prove the security of cryptographic systems using the Mizar proof checker. In this study, we formalize the probability on a finite and discrete sample space to achieve our aim. Therefore, we introduce a formalization of the probability distribution and prove the correctness of the formalization using the Mizar proof checking system as a formal verification tool.

Full Text: PDF DOI: 10.5430/air.v2n4p37


  • There are currently no refbacks.

Creative Commons License
This work is licensed under a Creative Commons Attribution 3.0 License.

Artificial Intelligence Research

ISSN 1927-6974 (Print)   ISSN 1927-6982 (Online)

Copyright © Sciedu Press 
To make sure that you can receive messages from us, please add the '' domain to your e-mail 'safe list'. If you do not receive e-mail in your 'inbox', check your 'bulk mail' or 'junk mail' folders.