SSH-Frank.py

# -*- generated by 1.0.12 -*-
import da
PatternExpr_278 = da.pat.TuplePattern([da.pat.BoundPattern('_BoundPattern279_'), da.pat.FreePattern('cookie_server'), da.pat.FreePattern('server_list'), da.pat.FreePattern('guess_server'), da.pat.FreePattern('reserved_server')])
PatternExpr_290 = da.pat.FreePattern('server')
PatternExpr_405 = da.pat.TuplePattern([da.pat.BoundPattern('_BoundPattern406_'), da.pat.FreePattern('K_S'), da.pat.FreePattern('f'), da.pat.FreePattern('sign_H')])
PatternExpr_415 = da.pat.FreePattern('server')
PatternExpr_483 = da.pat.BoundPattern('_BoundPattern484_')
PatternExpr_486 = da.pat.FreePattern('server')
PatternExpr_534 = da.pat.TuplePattern([da.pat.BoundPattern('_BoundPattern535_'), da.pat.TuplePattern([da.pat.FreePattern('cookie_client'), da.pat.FreePattern('client_list'), da.pat.FreePattern('guess_client'), da.pat.FreePattern('reserved_client')])])
PatternExpr_547 = da.pat.FreePattern('client')
PatternExpr_637 = da.pat.TuplePattern([da.pat.BoundPattern('_BoundPattern638_'), da.pat.FreePattern('e')])
PatternExpr_643 = da.pat.FreePattern('server')
PatternExpr_741 = da.pat.BoundPattern('_BoundPattern742_')
PatternExpr_744 = da.pat.FreePattern('client')
_config_object = {}
from sa.secalgo import *
from sa.sec_algo_pycrypto import *
from Crypto.Hash import SHA256
configure(verify_returns='bool')
configure(benchmark=True)
SSH_MSG_KEXINIT = 20
SSH_MSG_KexDH_INIT = 30
SSH_MSG_KexDH_REPLY = 31
SSH_MSG_NEWKEYS = 32

def iterate_protocol(client_list, server_list):
    for protocol_client in client_list:
        if (protocol_client in server_list):
            return protocol_client
    return None

class ssh_client(da.DistProcess):

    def __init__(self, procimpl, props):
        super().__init__(procimpl, props)
        self._ssh_clientReceivedEvent_0 = []
        self._ssh_clientReceivedEvent_1 = []
        self._ssh_clientReceivedEvent_2 = []
        self._events.extend([da.pat.EventPattern(da.pat.ReceivedEvent, '_ssh_clientReceivedEvent_0', PatternExpr_278, sources=[PatternExpr_290], destinations=None, timestamps=None, record_history=True, handlers=[]), da.pat.EventPattern(da.pat.ReceivedEvent, '_ssh_clientReceivedEvent_1', PatternExpr_405, sources=[PatternExpr_415], destinations=None, timestamps=None, record_history=True, handlers=[]), da.pat.EventPattern(da.pat.ReceivedEvent, '_ssh_clientReceivedEvent_2', PatternExpr_483, sources=[PatternExpr_486], destinations=None, timestamps=None, record_history=True, handlers=[])])

    def setup(self, kex_algo_client, server_host_key_algo_client, encryption_ctos_client, encryption_stoc_client, mac_ctos_client, compression_ctos_client, conpression_stoc_client, languages_ctos_client, language_stoc_client, guess_client, host_key_server_public, server, **rest_925):
        super().setup(kex_algo_client=kex_algo_client, server_host_key_algo_client=server_host_key_algo_client, encryption_ctos_client=encryption_ctos_client, encryption_stoc_client=encryption_stoc_client, mac_ctos_client=mac_ctos_client, compression_ctos_client=compression_ctos_client, conpression_stoc_client=conpression_stoc_client, languages_ctos_client=languages_ctos_client, language_stoc_client=language_stoc_client, guess_client=guess_client, host_key_server_public=host_key_server_public, server=server, **rest_925)
        self._state.kex_algo_client = kex_algo_client
        self._state.server_host_key_algo_client = server_host_key_algo_client
        self._state.encryption_ctos_client = encryption_ctos_client
        self._state.encryption_stoc_client = encryption_stoc_client
        self._state.mac_ctos_client = mac_ctos_client
        self._state.compression_ctos_client = compression_ctos_client
        self._state.conpression_stoc_client = conpression_stoc_client
        self._state.languages_ctos_client = languages_ctos_client
        self._state.language_stoc_client = language_stoc_client
        self._state.guess_client = guess_client
        self._state.host_key_server_public = host_key_server_public
        self._state.server = server
        pass

    def run(self):
        cookie_client = keygen('random', 16)
        client_list = (self._state.kex_algo_client, self._state.server_host_key_algo_client, self._state.encryption_ctos_client, self._state.encryption_stoc_client, self._state.mac_ctos_client, self._state.compression_ctos_client, self._state.conpression_stoc_client, self._state.languages_ctos_client, self._state.language_stoc_client, self._state.host_key_server_public)
        I_C = (SSH_MSG_KEXINIT, cookie_client, client_list, self._state.guess_client, 0)
        print('SSH starts')
        self.send((SSH_MSG_KEXINIT, (cookie_client, client_list, self._state.guess_client, 0)), to=self._state.server)
        print('Client: Sends the first message(SSH_MSG_KEXINIT)')
        super()._label('_st_label_275', block=False)
        reserved_server = guess_server = server_list = cookie_server = server = None

        def ExistentialOpExpr_276():
            nonlocal reserved_server, guess_server, server_list, cookie_server, server
            for (_, (_, _, self._state.server), (_BoundPattern300_, cookie_server, server_list, guess_server, reserved_server)) in self._ssh_clientReceivedEvent_0:
                if (_BoundPattern300_ == SSH_MSG_KEXINIT):
                    if True:
                        return True
            return False
        _st_label_275 = 0
        while (_st_label_275 == 0):
            _st_label_275 += 1
            if ExistentialOpExpr_276():
                _st_label_275 += 1
            else:
                super()._label('_st_label_275', block=True)
                _st_label_275 -= 1
        print('Client: Recevied the second message from the server')
        if (guess_server & self._state.guess_client):
            print('Client: Guess Attempt not implemented. Start iterating name-lists...')
        else:
            print('Client: No Guess attempt made. Start iterating name-lists...')
        agreed_algorithms = []
        both_lists = zip(client_list, server_list)
        for pair in both_lists:
            agreed_algorithms.append(iterate_protocol(pair[0], pair[1]))
        print('Client: Done iterating protocols. Agreed algorithms saved for late use')
        x = int.from_bytes(keygen('random', 16), byteorder='little')
        g = modp_groups[5]['g']
        p = modp_groups[5]['p']
        e = pow(g, x, p)
        self.send((SSH_MSG_KexDH_INIT, e), to=self._state.server)
        print('Client: Sends the third message to the server')
        super()._label('_st_label_402', block=False)
        sign_H = f = K_S = server = None

        def ExistentialOpExpr_403():
            nonlocal sign_H, f, K_S, server
            for (_, (_, _, self._state.server), (_BoundPattern425_, K_S, f, sign_H)) in self._ssh_clientReceivedEvent_1:
                if (_BoundPattern425_ == SSH_MSG_KexDH_REPLY):
                    if True:
                        return True
            return False
        _st_label_402 = 0
        while (_st_label_402 == 0):
            _st_label_402 += 1
            if ExistentialOpExpr_403():
                _st_label_402 += 1
            else:
                super()._label('_st_label_402', block=True)
                _st_label_402 -= 1
        print('Client: Received the fourth message from the server')
        I_S = (SSH_MSG_KEXINIT, cookie_server, server_list, guess_server, reserved_server)
        k = pow(f, x, p)
        hash = (self._id, self._state.server, I_C, I_S, K_S, e, f, k)
        if verify((hash, sign_H), K_S):
            self.send(SSH_MSG_NEWKEYS, to=self._state.server)
            print('Client: Sends the fifth message to the server')
            super()._label('_st_label_480', block=False)
            server = None

            def ExistentialOpExpr_481():
                nonlocal server
                for (_, (_, _, self._state.server), _BoundPattern495_) in self._ssh_clientReceivedEvent_2:
                    if (_BoundPattern495_ == SSH_MSG_NEWKEYS):
                        if True:
                            return True
                return False
            _st_label_480 = 0
            while (_st_label_480 == 0):
                _st_label_480 += 1
                if ExistentialOpExpr_481():
                    _st_label_480 += 1
                else:
                    super()._label('_st_label_480', block=True)
                    _st_label_480 -= 1
            print('Client: Key exchange and algorithm negotiation completed. New key will be used from now on. ')
        else:
            print('Verification failed. Client and Server disconnected')

class ssh_server(da.DistProcess):

    def __init__(self, procimpl, props):
        super().__init__(procimpl, props)
        self._ssh_serverReceivedEvent_1 = []
        self._ssh_serverReceivedEvent_2 = []
        self._events.extend([da.pat.EventPattern(da.pat.ReceivedEvent, '_ssh_serverReceivedEvent_0', PatternExpr_534, sources=[PatternExpr_547], destinations=None, timestamps=None, record_history=None, handlers=[self._ssh_server_handler_533]), da.pat.EventPattern(da.pat.ReceivedEvent, '_ssh_serverReceivedEvent_1', PatternExpr_637, sources=[PatternExpr_643], destinations=None, timestamps=None, record_history=True, handlers=[]), da.pat.EventPattern(da.pat.ReceivedEvent, '_ssh_serverReceivedEvent_2', PatternExpr_741, sources=[PatternExpr_744], destinations=None, timestamps=None, record_history=True, handlers=[])])

    def setup(self, kex_algo_server, server_host_key_algo_server, encryption_ctos_server, encryption_stoc_server, mac_ctos_server, compression_ctos_server, conpression_stoc_server, languages_ctos_server, language_stoc_server, guess_server, host_key_server_private, host_key_server_public, **rest_925):
        super().setup(kex_algo_server=kex_algo_server, server_host_key_algo_server=server_host_key_algo_server, encryption_ctos_server=encryption_ctos_server, encryption_stoc_server=encryption_stoc_server, mac_ctos_server=mac_ctos_server, compression_ctos_server=compression_ctos_server, conpression_stoc_server=conpression_stoc_server, languages_ctos_server=languages_ctos_server, language_stoc_server=language_stoc_server, guess_server=guess_server, host_key_server_private=host_key_server_private, host_key_server_public=host_key_server_public, **rest_925)
        self._state.kex_algo_server = kex_algo_server
        self._state.server_host_key_algo_server = server_host_key_algo_server
        self._state.encryption_ctos_server = encryption_ctos_server
        self._state.encryption_stoc_server = encryption_stoc_server
        self._state.mac_ctos_server = mac_ctos_server
        self._state.compression_ctos_server = compression_ctos_server
        self._state.conpression_stoc_server = conpression_stoc_server
        self._state.languages_ctos_server = languages_ctos_server
        self._state.language_stoc_server = language_stoc_server
        self._state.guess_server = guess_server
        self._state.host_key_server_private = host_key_server_private
        self._state.host_key_server_public = host_key_server_public
        pass

    def run(self):
        super()._label('_st_label_529', block=False)
        _st_label_529 = 0
        while (_st_label_529 == 0):
            _st_label_529 += 1
            if False:
                _st_label_529 += 1
            else:
                super()._label('_st_label_529', block=True)
                _st_label_529 -= 1

    def _ssh_server_handler_533(self, cookie_client, client_list, guess_client, reserved_client, client):
        print('Server: Received the first message from client')
        cookie_server = keygen('random', 16)
        I_C = (SSH_MSG_KEXINIT, cookie_client, client_list, guess_client, reserved_client)
        server_list = (self._state.kex_algo_server, self._state.server_host_key_algo_server, self._state.encryption_ctos_server, self._state.encryption_stoc_server, self._state.mac_ctos_server, self._state.compression_ctos_server, self._state.conpression_stoc_server, self._state.languages_ctos_server, self._state.language_stoc_server)
        print('Server: Sends the second message to the client')
        self.send((SSH_MSG_KEXINIT, cookie_server, server_list, self._state.guess_server, 0), to=client)
        I_S = (SSH_MSG_KEXINIT, cookie_server, server_list, self._state.guess_server, 0)
        agreed_algorithms = []
        both_lists = zip(client_list, server_list)
        for pair in both_lists:
            agreed_algorithms.append(iterate_protocol(pair[0], pair[1]))
        super()._label('_st_label_634', block=False)
        e = server = None

        def ExistentialOpExpr_635():
            nonlocal e, server
            for (_, (_, _, server), (_BoundPattern654_, e)) in self._ssh_serverReceivedEvent_1:
                if (_BoundPattern654_ == SSH_MSG_KexDH_INIT):
                    if True:
                        return True
            return False
        _st_label_634 = 0
        while (_st_label_634 == 0):
            _st_label_634 += 1
            if ExistentialOpExpr_635():
                _st_label_634 += 1
            else:
                super()._label('_st_label_634', block=True)
                _st_label_634 -= 1
        print('Server: Received third message from the client')
        y = int.from_bytes(keygen('random', 16), byteorder='little')
        g = modp_groups[5]['g']
        p = modp_groups[5]['p']
        f = pow(g, y, p)
        k = pow(e, y, p)
        hash = (client, self._id, I_C, I_S, self._state.host_key_server_public, e, f, k)
        s = sign(hash, key=self._state.host_key_server_private)
        self.send((SSH_MSG_KexDH_REPLY, self._state.host_key_server_public, f, s), to=client)
        print('Server: Sends fourth message to the clinet')
        super()._label('_st_label_738', block=False)
        client = None

        def ExistentialOpExpr_739():
            nonlocal client
            for (_, (_, _, client), _BoundPattern753_) in self._ssh_serverReceivedEvent_2:
                if (_BoundPattern753_ == SSH_MSG_NEWKEYS):
                    if True:
                        return True
            return False
        _st_label_738 = 0
        while (_st_label_738 == 0):
            _st_label_738 += 1
            if ExistentialOpExpr_739():
                _st_label_738 += 1
            else:
                super()._label('_st_label_738', block=True)
                _st_label_738 -= 1
        print('Server: Received the fifth message from the client')
        self.send(SSH_MSG_NEWKEYS, to=client)
        print('Server: Key exchange and algorithm negotiation completed. New key will be used from now on. ')
    _ssh_server_handler_533._labels = None
    _ssh_server_handler_533._notlabels = None

class Node_(da.NodeProcess):

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

    def run(self):
        (host_key_server_private, host_key_server_public) = keygen('public')
        kex_algo_client = ['DF']
        server_host_key_algo_client = ['DSA']
        encryption_ctos_client = ['AES']
        encryption_stoc_client = ['AES']
        mac_ctos_client = ['SHA-1']
        compression_ctos_client = ['none']
        conpression_stoc_client = ['none']
        languages_ctos_client = []
        language_stoc_client = []
        guess_client = False
        kex_algo_server = ['DF']
        server_host_key_algo_server = ['DSA']
        encryption_ctos_server = ['AES']
        encryption_stoc_server = ['AES']
        mac_ctos_server = ['SHA-1']
        compression_ctos_server = ['none']
        conpression_stoc_server = ['none']
        languages_ctos_server = []
        language_stoc_server = []
        guess_server = False
        client = self.new(ssh_client)
        server = self.new(ssh_server)
        self._setup(client, (kex_algo_client, server_host_key_algo_client, encryption_ctos_client, encryption_stoc_client, mac_ctos_client, compression_ctos_client, conpression_stoc_client, languages_ctos_client, language_stoc_client, guess_client, host_key_server_public, server))
        self._setup(server, (kex_algo_server, server_host_key_algo_server, encryption_ctos_server, encryption_stoc_server, mac_ctos_server, compression_ctos_server, conpression_stoc_server, languages_ctos_server, language_stoc_server, guess_server, host_key_server_private, host_key_server_public))
        self._start(server)
        self._start(client)