ns-sk-amended.py

# -*- generated by 1.0.9 -*-
import da
PatternExpr_176 = da.pat.TuplePattern([da.pat.ConstantPattern('m3'), da.pat.TuplePattern([da.pat.FreePattern('A'), da.pat.FreePattern('B'), da.pat.FreePattern('Na'), da.pat.FreePattern('enc_BA')])])
PatternExpr_190 = da.pat.FreePattern('A')
PatternExpr_268 = da.pat.TuplePattern([da.pat.ConstantPattern('m2'), da.pat.FreePattern('enc_BA')])
PatternExpr_275 = da.pat.FreePattern('B')
PatternExpr_314 = da.pat.TuplePattern([da.pat.ConstantPattern('m4'), da.pat.FreePattern('enc_SA')])
PatternExpr_321 = da.pat.FreePattern('S')
PatternExpr_385 = da.pat.TuplePattern([da.pat.ConstantPattern('m6'), da.pat.FreePattern('enc_BA')])
PatternExpr_391 = da.pat.FreePattern('B')
PatternExpr_447 = da.pat.TuplePattern([da.pat.ConstantPattern('m1'), da.pat.FreePattern('A')])
PatternExpr_454 = da.pat.FreePattern('A')
PatternExpr_481 = da.pat.TuplePattern([da.pat.ConstantPattern('m5'), da.pat.FreePattern('enc_SB')])
PatternExpr_488 = da.pat.FreePattern('A')
PatternExpr_542 = da.pat.TuplePattern([da.pat.ConstantPattern('m7'), da.pat.FreePattern('enc_AB')])
PatternExpr_549 = da.pat.FreePattern('A')
_config_object = {}
from sa.secalgo import *

class RoleS(da.DistProcess):

    def __init__(self, procimpl, props):
        super().__init__(procimpl, props)
        self._events.extend([da.pat.EventPattern(da.pat.ReceivedEvent, '_RoleSReceivedEvent_0', PatternExpr_176, sources=[PatternExpr_190], destinations=None, timestamps=None, record_history=None, handlers=[self._RoleS_handler_175])])

    def setup(self, Kas, Kbs, **rest_624):
        super().setup(Kas=Kas, Kbs=Kbs, **rest_624)
        self._state.Kas = Kas
        self._state.Kbs = Kbs
        pass

    def run(self):
        super()._label('_st_label_168', block=False)
        _st_label_168 = 0
        self._timer_start()
        while (_st_label_168 == 0):
            _st_label_168 += 1
            if False:
                pass
                _st_label_168 += 1
            elif self._timer_expired:
                pass
                _st_label_168 += 1
            else:
                super()._label('_st_label_168', block=True, timeout=10)
                _st_label_168 -= 1

    def _RoleS_handler_175(self, A, B, Na, enc_BA):
        print('4')
        if (A == decrypt(enc_BA, key=self._state.Kbs)[0]):
            Nb = decrypt(enc_BA, key=self._state.Kbs)[1]
            Kab = keygen('shared')
            self.send(('m4', encrypt((Na, B, Kab, encrypt((Kab, Nb, A), self._state.Kbs)), self._state.Kas)), to=A)
    _RoleS_handler_175._labels = None
    _RoleS_handler_175._notlabels = None

class RoleA(da.DistProcess):

    def __init__(self, procimpl, props):
        super().__init__(procimpl, props)
        self._RoleAReceivedEvent_0 = []
        self._RoleAReceivedEvent_1 = []
        self._RoleAReceivedEvent_2 = []
        self._events.extend([da.pat.EventPattern(da.pat.ReceivedEvent, '_RoleAReceivedEvent_0', PatternExpr_268, sources=[PatternExpr_275], destinations=None, timestamps=None, record_history=True, handlers=[]), da.pat.EventPattern(da.pat.ReceivedEvent, '_RoleAReceivedEvent_1', PatternExpr_314, sources=[PatternExpr_321], destinations=None, timestamps=None, record_history=True, handlers=[]), da.pat.EventPattern(da.pat.ReceivedEvent, '_RoleAReceivedEvent_2', PatternExpr_385, sources=[PatternExpr_391], destinations=None, timestamps=None, record_history=True, handlers=[])])

    def setup(self, B, Kas, S, **rest_624):
        super().setup(B=B, Kas=Kas, S=S, **rest_624)
        self._state.B = B
        self._state.Kas = Kas
        self._state.S = S
        pass

    def run(self):
        print('1')
        self.send(('m1', self._id), to=self._state.B)
        super()._label('_st_label_265', block=False)
        B = enc_BA = None

        def ExistentialOpExpr_266():
            nonlocal B, enc_BA
            for (_, (_, _, self._state.B), (_ConstantPattern285_, enc_BA)) in self._RoleAReceivedEvent_0:
                if (_ConstantPattern285_ == 'm2'):
                    if True:
                        return True
            return False
        _st_label_265 = 0
        while (_st_label_265 == 0):
            _st_label_265 += 1
            if ExistentialOpExpr_266():
                _st_label_265 += 1
            else:
                super()._label('_st_label_265', block=True)
                _st_label_265 -= 1
        print('3')
        Na = nonce()
        self.send(('m3', (self._id, self._state.B, Na, enc_BA)), to=self._state.S)
        super()._label('_st_label_311', block=False)
        S = enc_SA = None

        def ExistentialOpExpr_312():
            nonlocal S, enc_SA
            for (_, (_, _, self._state.S), (_ConstantPattern331_, enc_SA)) in self._RoleAReceivedEvent_1:
                if (_ConstantPattern331_ == 'm4'):
                    if ((decrypt(enc_SA, key=self._state.Kas)[0] == Na) and (decrypt(enc_SA, key=self._state.Kas)[1] == self._state.B)):
                        return True
            return False
        _st_label_311 = 0
        while (_st_label_311 == 0):
            _st_label_311 += 1
            if ExistentialOpExpr_312():
                _st_label_311 += 1
            else:
                super()._label('_st_label_311', block=True)
                _st_label_311 -= 1
        print('5')
        Kab = decrypt(enc_SA, key=self._state.Kas)[2]
        enc_SB = decrypt(enc_SA, key=self._state.Kas)[3]
        self.send(('m5', enc_SB), to=self._state.B)
        super()._label('_st_label_382', block=False)
        B = enc_BA = None

        def ExistentialOpExpr_383():
            nonlocal B, enc_BA
            for (_, (_, _, self._state.B), (_ConstantPattern401_, enc_BA)) in self._RoleAReceivedEvent_2:
                if (_ConstantPattern401_ == 'm6'):
                    if True:
                        return True
            return False
        _st_label_382 = 0
        while (_st_label_382 == 0):
            _st_label_382 += 1
            if ExistentialOpExpr_383():
                _st_label_382 += 1
            else:
                super()._label('_st_label_382', block=True)
                _st_label_382 -= 1
        Nb = decrypt(enc_BA, key=Kab)
        self.send(('m7', encrypt((Nb - 1), key=Kab)), to=self._state.B)
        self.output('A - Key Exchange Complete')

class RoleB(da.DistProcess):

    def __init__(self, procimpl, props):
        super().__init__(procimpl, props)
        self._RoleBReceivedEvent_1 = []
        self._RoleBReceivedEvent_2 = []
        self._events.extend([da.pat.EventPattern(da.pat.ReceivedEvent, '_RoleBReceivedEvent_0', PatternExpr_447, sources=[PatternExpr_454], destinations=None, timestamps=None, record_history=None, handlers=[self._RoleB_handler_446]), da.pat.EventPattern(da.pat.ReceivedEvent, '_RoleBReceivedEvent_1', PatternExpr_481, sources=[PatternExpr_488], destinations=None, timestamps=None, record_history=True, handlers=[]), da.pat.EventPattern(da.pat.ReceivedEvent, '_RoleBReceivedEvent_2', PatternExpr_542, sources=[PatternExpr_549], destinations=None, timestamps=None, record_history=True, handlers=[])])

    def setup(self, Kbs, **rest_624):
        super().setup(Kbs=Kbs, **rest_624)
        self._state.Kbs = Kbs
        pass

    def run(self):
        super()._label('_st_label_439', block=False)
        _st_label_439 = 0
        self._timer_start()
        while (_st_label_439 == 0):
            _st_label_439 += 1
            if False:
                pass
                _st_label_439 += 1
            elif self._timer_expired:
                pass
                _st_label_439 += 1
            else:
                super()._label('_st_label_439', block=True, timeout=10)
                _st_label_439 -= 1

    def _RoleB_handler_446(self, A):
        print('2')
        Nb = nonce()
        self.send(('m2', encrypt((A, Nb), self._state.Kbs)), to=A)
        super()._label('_st_label_478', block=False)
        A = enc_SB = None

        def ExistentialOpExpr_479():
            nonlocal A, enc_SB
            for (_, (_, _, A), (_ConstantPattern498_, enc_SB)) in self._RoleBReceivedEvent_1:
                if (_ConstantPattern498_ == 'm5'):
                    if ((decrypt(enc_SB, key=self._state.Kbs)[1] == Nb) and (decrypt(enc_SB, key=self._state.Kbs)[2] == A)):
                        return True
            return False
        _st_label_478 = 0
        while (_st_label_478 == 0):
            _st_label_478 += 1
            if ExistentialOpExpr_479():
                _st_label_478 += 1
            else:
                super()._label('_st_label_478', block=True)
                _st_label_478 -= 1
        Kab = decrypt(enc_SB, key=self._state.Kbs)[0]
        self.send(('m6', encrypt(Nb, Kab)), to=A)
        super()._label('_st_label_539', block=False)
        A = enc_AB = None

        def ExistentialOpExpr_540():
            nonlocal A, enc_AB
            for (_, (_, _, A), (_ConstantPattern559_, enc_AB)) in self._RoleBReceivedEvent_2:
                if (_ConstantPattern559_ == 'm7'):
                    if ((Nb - 1) == decrypt(enc_AB, key=Kab)):
                        return True
            return False
        _st_label_539 = 0
        while (_st_label_539 == 0):
            _st_label_539 += 1
            if ExistentialOpExpr_540():
                _st_label_539 += 1
            else:
                super()._label('_st_label_539', block=True)
                _st_label_539 -= 1
        self.output('B - Key Exchange Complete')
    _RoleB_handler_446._labels = None
    _RoleB_handler_446._notlabels = None

class Node_(da.NodeProcess):

    def __init__(self, procimpl, props):
        super().__init__(procimpl, props)
        self._events.extend([])

    def run(self):
        Kas = keygen('shared')
        Kbs = keygen('shared')
        S = self.new(RoleS, (Kas, Kbs))
        B = self.new(RoleB, (Kbs,))
        A = self.new(RoleA, (B, Kas, S))
        self._start(A)
        self._start(B)
        self._start(S)