This case study concerns the non-repudiation protocol of Markowitch & Roggeman [MR99].

The models here are partially observable probabilistic timed automata (POPTAs),
as described in [NPZ17]. These extend the the probabilistic timed automaton (PTA)
version from [NPS13], the files for which can be found in ../../ptas/repudiation.
Both are extensions of the PTA model developed in [LMST04].

For more information, see: http://www.prismmodelchecker.org/casestudies/nonrepudiation.php

=====================================================================================

PARAMETERS:

K: the originator randomly selects an integer over the range 1,...,K

=====================================================================================

[LMST04]
R. Lanotte, A. Maggiolo-Schettini and A. Troina
Automatic Analysis of a Non-Repudiation Protocol
In Proc. 2nd International Workshop on Quantitative Aspects of Programming Languages (QAPL'04), 2004
(available as ENTCS, vol. 112, pp. 113–129, 2005)

[MR99]
O. Markowitch and Y. Roggeman
Probabilistic non-repudiation without trusted third party
In Proc. 2nd Workshop on Security in Communication Networks, 1999

[NPS13]
Gethin Norman, David Parker and Jeremy Sproston
Model Checking for Probabilistic Timed Automata
Formal Methods in System Design, 43(2), pages 164-190, Springer, 2013

[NPZ17]
Gethin Norman, David Parker and Xueyi Zou
Verification and Control of Partially Observable Probabilistic Systems
Real-Time Systems, 53(3), pages 354-402, Springer, 2017