Modeling and Verification Distance Fraud Attacks
Statistical model checking of distance fraud attacks on the Hancke-Kuhn family of protocols
Posts by Collection
projects
Resource-bounded Intruders in Denial of Service Attacks
A formal resource-bounded-intruders model for a wide range of denial of service attacks
Statistical Model Checking of RANDAO Against Attacks
Statistical model checking of RANDAO’s resilience against pre-computed reveal sstrategies
Verification of Algorand’s Safety Property
Modeling of the Algorand Consensus Protocol in the Coq proof assistant and verifying its safety guarantees
An executable model of the Beacon Chain protocol
An executable K model of Ethereum 2.0 Beacon Chain Phase 0 specification
Modeling and Verification of Gasper
Modeling Gasper and verifying its properties using the Coq proof assistant
Formal tooling for Algorand’s smart contract architecture
Building formal semantics of both L1 and L2 languages for Algorand’s smart contract architecture in the K framework
publications
Real-Time Rewriting Semantics of Orc
Principles and Practice of Declarative Programming, ACM, pp 131–142, 2007
Musab A. Alturki and José Meseguer
Reduction Semantics and Formal Analysis of Orc Programs
Automated Specification and Verification of Web Systems, ENTCS 200, pp 25–41, 2008
Musab A. Alturki and José Meseguer
PBES: A Policy Based Encryption System with Application to Data Sharing in the Power Grid
International Symposium on Information, Computer, and Communications Security, ACM, pp 262-275, 2009
Rakesh Bobba, Himanshu Khurana, Musab A. Alturki and Farhana Ashraf
Probabilistic Modeling and Analysis of DoS Protection for the ASV Protocol
Security and Rewriting Techniques, ENTCS 234, pp 3-18, 2009
Musab A. Alturki, José Meseguer and Carl A. Gunter
Formal Specification and Analysis of Timing Properties in Software Systems
Fundamental Approaches to Software Engineering, Springer, LNCS 5503, pp 262-277, 2009
Musab A. Alturki, Dinakar Dhurjati, Dachuan Yu, Ajay Chander and Hiroshi Inamura
Model-Checking DoS Amplification for VoIP Session Initiation
European Symposium on Research in Computer Security, Springer, LNCS 5789, pp 390-405, 2009
Ravinder Shankesi, Musab A. Alturki, Ralf Sasse, Carl A. Gunter and José Meseguer
Dist-Orc: A Rewriting-based Distributed Implementation of Orc with Formal Analysis
Rewriting Techniques for Real-Time Systems, EPTCS 36, pp 26-45, 2010
Musab A. Alturki and José Meseguer
PVeStA: A Parallel Statistical Model Checking and Quantitative Analysis Tool
Algebra and Coalgebra in Computer Science, Springer, LNCS 6859, pp 386-392, 2011
Musab A. Alturki and José Meseguer
Stable Availability under Denial of Service Attacks through Formal Patterns
Fundamental Approaches to Software Engineering, Springer, LNCS 7212, pp 78-93, 2012
Jonas Eckhardt, Tobias Mühlbauer, Musab A. Alturki, José Meseguer and Martin Wirsing
Sparse Single-Hidden Layer Feedforward Network for Mapping Natural Language Questions to SQL Queries
Artificial Neural Networks and Machine Learning, Springer, LNCS 8681, pp 241-248, 2014
Issam H. Laradji, Lahouari Ghouti, Faisal Saleh and Musab A. Alturki
Towards Formal Verification of Orchestration Computations Using the K Framework
Formal Methods, Springer, LNCS 9109, pp 40-56, 2015
Musab A. Alturki and Omar Alzuhaibi
Executable Rewriting Logic Semantics of Orc and Formal Analysis of Orc Programs
Journal of Logical and Algebraic Methods in Programming, Volume 84(4), pp 505–533, 2015
Musab A. Alturki and José Meseguer
Implementing the Observer Design Pattern as an Expressive Language Construct
Software Engineering Advances, pp 463-469, 2015
Taher A. Ghaleb, Khalid Aljasser and Musab A. Alturki
A Symbolic Rewriting Semantics of the COMPASS Modeling Language
Information Reuse and Integration, IEEE, pp 283-290, 2017
Musab A. Alturki
Statistical Model Checking of Distance Fraud Attacks on the Hancke-Kuhn Family of Protocols
Cyber-Physical Systems Security and Privacy, ACM, pp 60-71, 2018
Musab A. Alturki, Max Kanovich, Tajana Ban Kirigin, Vivek Nigam, Andre Scedrov and Carolyn Talcott
Program Comprehension through Reverse-engineered Sequence Diagrams: A Systematic Review
Journal of Software: Evolution and Process, Wiley, Volume 30(11), pp e1965, 2018
Taher A. Ghaleb, Musab A. Alturki and Khalid Aljasser
A Multiset Rewriting Model for Specifying and Verifying Timing Aspects of Security Protocols
Foundations of Security, Protocols, and Equational Reasoning, Springer, LNCS 11565, pp 192-213, 2019
Musab A. Alturki, Tajana Ban Kirigin, Max Kanovich, Vivek Nigam, Andre Scedrov and Carolyn Talcott
Resource-Bounded Intruders in Denial of Service Attacks
Computer Security Foundations Symposium, IEEE, pp 382-396, 2019
Abraão Aires Urquiza, Musab A. Alturki, Max Kanovich, Tajana Ban Kirigin, Vivek Nigam, Andre Scedrov and Carolyn Talcott
Towards a Verified Model of the Algorand Consensus Protocol in Coq
Proceedings of Formal Methods (FM) 2019 International Workshops, volume 12232 of LNCS, pages 362-367, 2020
Musab A. Alturki, Jing Chen, Victor Luchangco, Brandon Moore, Karl Palmskog, Lucas Peña and Grigore Roşu
Statistical Model Checking of RANDAO’s Resilience to Pre-computed Reveal Strategies
Formal Methods (FM) 2019 International Workshops, volume 12232 of LNCS, pages 337–349, 2020
Musab A. Alturki and Grigore Roşu
Enhanced Visualization of Method Invocations by Extending Reverse-engineered Sequence Diagrams
Proceedings of 2020 Working Conference on Software Visualization (VISSOFT), 2020, 2020
Taher A. Ghaleb, Khalid Aljasser, Musab A. Alturki
On Security Analysis of Periodic Systems: Expressiveness and Complexity
Proceedings of the 7th International Conference on Information Systems Security and Privacy, ICISSP 2021, 2021
Musab A. Alturki, Tajana Ban Kirigin, Max Kanovich, Vivek Nigam, Andre Scedrov and Carolyn Talcott
Resource and timing aspects of security protocols
Journal of Computer Security, 2021
Abraão Aires Urquiza, Musab A. Alturki, Tajana Ban Kirigin, Max Kanovich, Vivek Nigam, Andre Scedrov and Carolyn Talcott
An Extensible Compiler for Implementing Software Design Patterns as Concise Language Constructs
International Journal of Software Engineering and Knowledge Engineering, 2021
Taher A. Ghaleb, Khalid Aljasser, Musab A. Alturki
talks
Statistical Model Checking of Distance Fraud Attacks on the Hancke-Kuhn Family of Protocols
Published:
teaching
Introduction to Computing I and II - Lab
Undergraduate Course, King Fahd University of Petroleum and Minerals
Fall 2002, Spring 2003
Introduction to Computing I and II
Undergraduate Course, King Fahd University of Petroleum and Minerals
2011 – 2013
Formal Methods and Models in Software Engineering
Undergraduate Course, King Fahd University of Petroleum and Minerals
Fall 2011
Theory of Computation
Undergraduate Course, King Fahd University of Petroleum and Minerals
Spring 2012
Principles of Programming Languages
(Under)graduate Course, King Fahd University of Petroleum and Minerals
Fall 2012, Fall 2013
Theory and Design of Programming Languages
Graduate course, King Fahd University of Petroleum and Minerals
Fall 2014, Fall 2015, Fall 2016