Group based Authentication:

xercise 4.3.4 after visiting Canada. She arrives at the US border with her passport in hand. Sam is a citizen and resident of the United States, returning home a. The act of driving her car to the border agent's station can be interpreted as a request to enter the United States. Express this request in the access-control logic. b. Sam's passport can be interpreted as a certificate (i.e., a signed statement) from the U.S. State Department that associates Sam's face with her name. It also identifies Sam as belonging to the group of U.S. citizens. Formalize Sam's passport as an expression in the access-control logic. c. The standard policy is that US citizens with proof of citizenship may enter the country, provided the border agent deems them not to be a threat (i.e., the border agent may exercise discretion). Formalize this policy in the access-control logic. d. Suppose that the border agent deems Sam not to be a threat. Identify any other necessary assumptions (expressed as formulas in the access control logic) about certificates, jurisdiction, et cetera to justify letting Sam enter the United States. e. Using only those expressions given in the previous parts of the question, give a formal proof justifying Sam's entry into the United States