Вопросы, связанные с Scyther, для обработки/разделения значений и проверки хэшей

При реализации протокола в Scyther мне нужна помощь в следующих вопросах:

1. Как в Scyther разделить конкретное сообщение/переменную на две части? (Например, если у меня есть значение R в моем протоколе, которое мне нужно разделить на две части, скажем, K1 и K2, как мне сделать это в Scyther. Я пробовал R = СЦЕП (К1, К2) где все R, K1 и K2 одного типа, но я не знаю, правильно ли это)
2. Как проверить хэши, полученные обоими объектами? (Например, существует сообщение M, которое генерируется отправителем S, и он/она отправляет M и Hash(M) получателю R. Копия сообщения M' уже хранится у получателя R, тогда, если мы хотим проверить значения Hash(M) с помощью Hash(M'), как нам это сделать? Я пытался использовать соответствовать() функция, но она показывает какую-то ошибку)
3. Как мы обрабатываем значения, которые, как утверждается, хранятся в базе данных сущностей? (Например, отправитель регистрируется у получателя, отправляя свой уникальный идентификатор, а получатель сохраняет полученный идентификатор в своей базе данных для дальнейшего использования, как мы изобразим этот сценарий в Scyther?)