{'fraction_non_alphanumeric': 0.01642710472279261, 'fraction_numerical': 0.0, 'mean_word_length': 5.543624161073826, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Formal Verification of Security Properties of Privacy Enhanced Mail

Abstract : The increased use of networked and distributed computing makes security a major concern. The capability to verify that a system meets its security requirements will continue to grow in importance. In particular, the capability to assign security properties to engineering structures is crucial. This work focuses on verifying the security properties of Privacy Enhanced Mail (PEM). Security properties such as non-repudiation, privacy, authentication, and integrity are defined independently of any implementation structure. PEM message structures and operations on those structures are shown to have the desired security properties. All formal definitions and proofs of security properties are done using the Higher Order Logic theorem prover. This work on PEM shows the feasibility of using formal logic and computer assisted reasoning tools to describe and verify relatively complex systems.