ns-pk-Lowe.py

# -*- generated by 1.0.9 -*-
import da
PatternExpr_176 = da.pat.TuplePattern([da.pat.ConstantPattern('msg1'), da.pat.TuplePattern([da.pat.FreePattern('A'), da.pat.FreePattern('B')])])
PatternExpr_186 = da.pat.FreePattern('A')
PatternExpr_219 = da.pat.TuplePattern([da.pat.ConstantPattern('msg4'), da.pat.TuplePattern([da.pat.FreePattern('B'), da.pat.FreePattern('A')])])
PatternExpr_229 = da.pat.FreePattern('B')
PatternExpr_285 = da.pat.TuplePattern([da.pat.ConstantPattern('msg2'), da.pat.FreePattern('sig_S')])
PatternExpr_292 = da.pat.FreePattern('S')
PatternExpr_346 = da.pat.TuplePattern([da.pat.ConstantPattern('msg6'), da.pat.FreePattern('enc_BA')])
PatternExpr_353 = da.pat.FreePattern('B')
PatternExpr_418 = da.pat.TuplePattern([da.pat.ConstantPattern('msg3'), da.pat.FreePattern('enc_AB')])
PatternExpr_425 = da.pat.FreePattern('A')
PatternExpr_458 = da.pat.TuplePattern([da.pat.ConstantPattern('msg5'), da.pat.FreePattern('sig_S')])
PatternExpr_465 = da.pat.FreePattern('S')
PatternExpr_520 = da.pat.TuplePattern([da.pat.ConstantPattern('msg7'), da.pat.FreePattern('enc_AB2')])
PatternExpr_527 = 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_186], destinations=None, timestamps=None, record_history=None, handlers=[self._roleS_handler_175]), da.pat.EventPattern(da.pat.ReceivedEvent, '_roleSReceivedEvent_1', PatternExpr_219, sources=[PatternExpr_229], destinations=None, timestamps=None, record_history=None, handlers=[self._roleS_handler_218])])

    def setup(self, skS, client_keys, **rest_633):
        super().setup(skS=skS, client_keys=client_keys, **rest_633)
        self._state.skS = skS
        self._state.client_keys = client_keys
        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):
        pkB = [x for (p, x) in self._state.client_keys if (p == B)].pop()
        self.send(('msg2', sign((B, pkB), self._state.skS)), to=A)
    _roleS_handler_175._labels = None
    _roleS_handler_175._notlabels = None

    def _roleS_handler_218(self, B, A):
        pkA = [x for (p, x) in self._state.client_keys if (p == A)].pop()
        self.send(('msg5', sign((A, pkA), self._state.skS)), to=B)
    _roleS_handler_218._labels = None
    _roleS_handler_218._notlabels = None

class roleA(da.DistProcess):

    def __init__(self, procimpl, props):
        super().__init__(procimpl, props)
        self._roleAReceivedEvent_0 = []
        self._roleAReceivedEvent_1 = []
        self._events.extend([da.pat.EventPattern(da.pat.ReceivedEvent, '_roleAReceivedEvent_0', PatternExpr_285, sources=[PatternExpr_292], destinations=None, timestamps=None, record_history=True, handlers=[]), da.pat.EventPattern(da.pat.ReceivedEvent, '_roleAReceivedEvent_1', PatternExpr_346, sources=[PatternExpr_353], destinations=None, timestamps=None, record_history=True, handlers=[])])

    def setup(self, skA, pkS, S, B, **rest_633):
        super().setup(skA=skA, pkS=pkS, S=S, B=B, **rest_633)
        self._state.skA = skA
        self._state.pkS = pkS
        self._state.S = S
        self._state.B = B
        pass

    def run(self):
        self.send(('msg1', (self._id, self._state.B)), to=self._state.S)
        super()._label('_st_label_282', block=False)
        sig_S = S = None

        def ExistentialOpExpr_283():
            nonlocal sig_S, S
            for (_, (_, _, self._state.S), (_ConstantPattern302_, sig_S)) in self._roleAReceivedEvent_0:
                if (_ConstantPattern302_ == 'msg2'):
                    if (verify(sig_S, key=self._state.pkS)[0] == self._state.B):
                        return True
            return False
        _st_label_282 = 0
        while (_st_label_282 == 0):
            _st_label_282 += 1
            if ExistentialOpExpr_283():
                _st_label_282 += 1
            else:
                super()._label('_st_label_282', block=True)
                _st_label_282 -= 1
        pkB = verify(sig_S, key=self._state.pkS)[1]
        nA = nonce()
        self.send(('msg3', encrypt((nA, self._id), key=pkB)), to=self._state.B)
        super()._label('_st_label_343', block=False)
        enc_BA = B = None

        def ExistentialOpExpr_344():
            nonlocal enc_BA, B
            for (_, (_, _, self._state.B), (_ConstantPattern363_, enc_BA)) in self._roleAReceivedEvent_1:
                if (_ConstantPattern363_ == 'msg6'):
                    if (decrypt(enc_BA, key=self._state.skA)[0] == nA):
                        return True
            return False
        _st_label_343 = 0
        while (_st_label_343 == 0):
            _st_label_343 += 1
            if ExistentialOpExpr_344():
                _st_label_343 += 1
            else:
                super()._label('_st_label_343', block=True)
                _st_label_343 -= 1
        nB = decrypt(enc_BA, key=self._state.skA)[1]
        self.send(('msg7', encrypt(nB, key=pkB)), to=self._state.B)
        self.output('A authenticated B')

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_418, sources=[PatternExpr_425], destinations=None, timestamps=None, record_history=None, handlers=[self._roleB_handler_417]), da.pat.EventPattern(da.pat.ReceivedEvent, '_roleBReceivedEvent_1', PatternExpr_458, sources=[PatternExpr_465], destinations=None, timestamps=None, record_history=True, handlers=[]), da.pat.EventPattern(da.pat.ReceivedEvent, '_roleBReceivedEvent_2', PatternExpr_520, sources=[PatternExpr_527], destinations=None, timestamps=None, record_history=True, handlers=[])])

    def setup(self, skB, pkS, S, **rest_633):
        super().setup(skB=skB, pkS=pkS, S=S, **rest_633)
        self._state.skB = skB
        self._state.pkS = pkS
        self._state.S = S
        pass

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

    def _roleB_handler_417(self, enc_AB, A):
        (A == decrypt(enc_AB, key=self._state.skB)[1])
        nA = decrypt(enc_AB, key=self._state.skB)[0]
        self.send(('msg4', (self._id, A)), to=self._state.S)
        super()._label('_st_label_455', block=False)
        S = sig_S = None

        def ExistentialOpExpr_456():
            nonlocal S, sig_S
            for (_, (_, _, self._state.S), (_ConstantPattern475_, sig_S)) in self._roleBReceivedEvent_1:
                if (_ConstantPattern475_ == 'msg5'):
                    if (verify(sig_S, key=self._state.pkS)[0] == A):
                        return True
            return False
        _st_label_455 = 0
        while (_st_label_455 == 0):
            _st_label_455 += 1
            if ExistentialOpExpr_456():
                _st_label_455 += 1
            else:
                super()._label('_st_label_455', block=True)
                _st_label_455 -= 1
        pkA = verify(sig_S, key=self._state.pkS)[1]
        nB = nonce()
        self.send(('msg6', encrypt((nA, nB, self._id), key=pkA)), to=A)
        super()._label('_st_label_517', block=False)
        enc_AB2 = A = None

        def ExistentialOpExpr_518():
            nonlocal enc_AB2, A
            for (_, (_, _, A), (_ConstantPattern537_, enc_AB2)) in self._roleBReceivedEvent_2:
                if (_ConstantPattern537_ == 'msg7'):
                    if (decrypt(enc_AB2, key=self._state.skB) == nB):
                        return True
            return False
        _st_label_517 = 0
        while (_st_label_517 == 0):
            _st_label_517 += 1
            if ExistentialOpExpr_518():
                _st_label_517 += 1
            else:
                super()._label('_st_label_517', block=True)
                _st_label_517 -= 1
        self.output('B authenticated A')
    _roleB_handler_417._labels = None
    _roleB_handler_417._notlabels = None

class Node_(da.NodeProcess):

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

    def run(self):
        (skS, pkS) = keygen('public')
        (skA, pkA) = keygen('public')
        (skB, pkB) = keygen('public')
        A = self.new(roleA)
        B = self.new(roleB)
        S = self.new(roleS)
        self._setup(S, (skS, [(A, pkA), (B, pkB)]))
        self._setup(A, (skA, pkS, S, B))
        self._setup(B, (skB, pkS, S))
        self._start(S)
        self._start(B)
        self._start(A)