Gergei Bana, Ph.D.

Postdoctoral Researcher

MSR-INRIA Joint Centre

Address:

MSR-INRIA

École Polytechnique, Bat. Alan Turing

1 rue Honoré d'Estienne d'Orves

91120 Palaiseau, France

INRIA E-mail:

GergelydotBanaatinriadotfr

E-mail:

banaatmathdotupenndotedu

Working Papers

Gergei Bana, Koji Hasebe, Mitsuhiro Okada: Secrecy-Oriented First-Order Logical Analysis of Cryptographic Protocols (BPL 2.0)

Protocol Proofs with Computationally Complete Symbolic Attackers

Needham Schroeder Lowe (honest players play one role only, either Initiator or Responder)

Protocol Proofs with BPL 2.0

Needham Schroeder Lowe (honest players allowed to play both roles, even against themselves)

Amended Needham Schroeder shared-key (honest players play one role only)

Otway-Rees (honest players allowed to play both Initiator, Responder, even against themselves; there is only 1 trusted server playing only the Sever role)

Publications

12. バナ・ゲルゲイ，ウベール・コモン-ルンド，櫻田 英樹．「計算論的に完全な記号的攻撃者とセキュリティ・プロトコルの計算論的に健全な検証」

11. Gergei Bana, Pedro Adão, Hideki Sakurada: Computationally Complete Symbolic Attacker in Action

10. Gergei Bana, Hubert Comon-Lundh: Towards Unconditional Soundness: Computationally Complete Symbolic Attacker

9. 長谷部浩二，バナ・ゲルゲイ，岡田光弘．「セキュリティプロトコルの論理的検証法」

8. Gergei Bana, Koji Hasebe, Mitsuhiro Okada: Computational Semantics for First-Order Logical Analysis of Cryptographic Protocols

7. Pedro Adão, Gergei Bana, Jonathan Herzog, Andre Scedrov: Soundness and Completeness of Formal Encryption: The Cases of Key Cycles and Partial Information Leakage

6. Gergei Bana, Koji Hasebe, Mitsuhiro Okada: Computational Semantics for Basic Protocol Logic - A Stochastic Approach

5. Gergei Bana, Payman Mohassel, Till Stegers: Computational Soundness of Formal Indistinguishability and Static Equivalence

4. Gergei Bana: A Note on Portfolios with Risk-Free Internal Gains

3. Pedro Adão, Gergei Bana, Jonathan Herzog, Andre Scedrov: Soundness of Formal Encryptions in the Presence of Key-Cycles

2. Pedro Adão, Gergei Bana, Andre Scedrov: Computational and Information-Theoretic Soundness and Completeness of Formal Encryption

1. Gergely Bana: Proof of Kolmogorovian Censorship

Ph.D. Thesis

2004, University of Pennsylvania

Soundness and Completeness of Formal Logics of Symmetric Encryptions

   This is about the relationship between formal and computational methods of cryptography

    For improved notations and proofs, see Publication 7.

Masters Paper

2003, Wharton School of the University of Pennsylvania

Risk-Free Internal Gains  -  Black and Scholes Re-examined

   This is about why the derivation of the Black-Scholes formula is correct even though it is mathematically erroneous

Hobbies

Piano

Photography