Masoud Koleini

Photograph of Masoud Koleini

Role: Research Student

I am a PhD student here at the School of Computer Science at The University of Birmingham under the supervision of Prof. Mark Ryan. I am a Microsoft PhD scholar and my research is funded by Microsoft.

Research area

Formal verification of dynamic (state-based) access control systems

I am working on the verification of state-based access control systems, using formal verification methods to verify temporal and epistemic properties over access control systems in order to find vulnerabilities related to policy design. My research also involves adopting abstraction mechanisms to reduce the size of the state space in order to make verification of systems with a large number of objects feasible.

I have worked in Microsoft Research Cambridge from August to October 2010. I worked with Moritz Becker, my supervisor in Microsoft Research. Our project was verification of information flow properties over credential-based access control policies. We worked on an algorithm that is able to find out if a system property is opaque from the point of view of an attacker with a specific security level. The designed algorithm is sound and complete, and implemented using Microsoft F# functional programming language.

I am the developer of PoliVer, an open source access control verification tool. I appreciate any collaboration related to my PhD research area and also my research interests.






Other research interests:

  • Formal verification, research and development of security protocols (in particular, access control systems)
  • Abstraction and refinement mechanisms
  • Interpreted systems
  • Network security and penetration testing, operating system and application security
  • Microprocessors and microcontrollers ( RISC microprocessors , AVR and ARM)
  • Software and hardware programming; interested in programming languages C++, C#, F#, Verilog
  • Analog and digital electronic circuit design

Publications

  1. Moritz Y. Becker and Masoud Koleini, Opacity Analysis in Trust Management Systems, In Proceedings of 14th Information Security Conference (ISC 2011), October 2011.
  2. Masoud Koleini and Mark Ryan, A knowledge-based verification method for dynamic access control policies, In Proceedings of 13th International Conference on Formal Engineering Methods (ICFEM 2011), October 2011.
  3. Masoud Koleini, Hasan Qunoo and Mark Ryan, Towards Modelling and Verifying Dynamic Access Control Policies for Web-based Collaborative Systems, W3C Workshop on Access Control Application Scenarios , November 2009.
  4. M. Koleini, M. Berenjkoub, M. Dakhil Alian, A New Protocol for Credit Card Transaction Systems, International Symposium on Telecommunications , September 10-12 2005, Iran.
  5. M. Koleini, M. Berenjkoub, M. Dakhil Alian, Security Analysis of 3D Secure Payment Protocol, 3rd Society of Cryptography conference , 6-7 September 2005, Isfahan, Iran (in Persian).

Teaching

I am a teaching assistant in following modules:



Educational and employment history

My CV is accessible from here.



Phone: (+44 (0)121 4143736)
Email:
Room: (218 Computer Science Building)