xDAuth là giao thức kiểm soát truy cập liên miền, hỗ trợ bảo mật và ủy quyền giữa các tổ chức trong liên minh.  

• Tác giả sử dụng High-Level Petri Nets (HLPN) để mô hình hóa luồng thông tin và hành vi của giao thức trong môi trường phân tán.  
• - Các quy tắc chuyển tiếp được xác định bằng ngôn ngữ Z và được xác minh bằng công cụ Z3 SMT solver.  
• - Năm thuộc tính bảo mật được kiểm chứng: xác thực khóa bí mật, chính sách Chinese Wall, tính bảo mật, toàn vẹn và xác thực.  
• - Kết quả xác minh cho thấy giao thức đáp ứng đầy đủ các thuộc tính bảo mật đã định, với thời gian xử lý dưới 0.04 giây cho mỗi thuộc tính.  
• - Tài liệu cũng chỉ ra điểm yếu tiềm tàng: khóa bí mật giữa DS và các miền có thể là điểm lỗi duy nhất, cần bổ sung cơ chế ghi nhật ký để tăng độ tin cậy.