Bojan Nokovic, McMaster University, Canada

A probabilistic model checker is a software tool for formal modeling and analysis of systems that exhibit random or probabilistic behaviour. Over probabilistic models, we analyze an innovative online authentication process based on image recognition. For true positive identification, the user needs to recognize the relationship between identified objects on distinct images which we call an outer relation, and the relation between objects in the same image which we call an inner relation. We use probabilistic computational tree logic formulas (PCTL) to quantify false-negative detection and analyze the proposed authentication process. That helps to tune up the process and make it more convenient for the user while maintaining the integrity of the authentication process.

Hierarchical State Machines; Probabilistic Model Checker; Costs/rewards; Verification.