Các câu hỏi liên quan đến Scyther để xử lý/tách các giá trị và xác minh giá trị băm

Trong khi triển khai một giao thức trong Scyther, tôi cần trợ giúp về các câu hỏi sau -

1. Làm cách nào để chia một thông báo/biến cụ thể thành hai phần trong Scyther? (Ví dụ: nếu tôi có giá trị R trong giao thức của mình mà tôi cần chia thành hai phần, chẳng hạn như K1 và K2, thì làm cách nào để thực hiện điều đó trong Scyther. Tôi đã thử R=CONCAT(K1, K2) trong đó tất cả R, K1 và K2 đều cùng loại nhưng tôi không biết liệu đó có phải là cách chính xác hay không)
2. Làm cách nào để xác minh giá trị băm mà cả hai thực thể nhận được? (Ví dụ: Có một tin nhắn M được tạo bởi người gửi S và anh ta/cô ta gửi M và Hash(M) đến người nhận R. Một bản sao của tin nhắn, M' đã được lưu trữ ở người nhận R, sau đó nếu chúng tôi muốn xác minh các giá trị Hash(M) với Hash(M'), làm cách nào để thực hiện điều đó? Tôi đã thử sử dụng trận đấu() chức năng nhưng nó hiển thị một số lỗi)
3. Làm cách nào để chúng tôi xử lý các giá trị được cho là sẽ được lưu trữ trong cơ sở dữ liệu của các thực thể? (Ví dụ: người gửi tự đăng ký với người nhận bằng cách gửi ID duy nhất của mình và người nhận lưu trữ ID nhận được trong cơ sở dữ liệu của nó để tham khảo sau này, làm cách nào để mô tả tình huống này trong Scyther?)